diff --git a/iset-discouraged b/iset-discouraged index cd4b2a941e..6aa1b9e3ce 100644 --- a/iset-discouraged +++ b/iset-discouraged @@ -385,6 +385,7 @@ New usage of "cnm" is discouraged (2 uses). New usage of "condcOLD" is discouraged (0 uses). New usage of "conventions" is discouraged (0 uses). New usage of "csbco" is discouraged (5 uses). +New usage of "dcan2" is discouraged (0 uses). New usage of "dcapnconstALT" is discouraged (0 uses). New usage of "dcnnOLD" is discouraged (0 uses). New usage of "demoivreALT" is discouraged (0 uses). diff --git a/iset.mm b/iset.mm index 46febfd198..6563a61b7f 100644 --- a/iset.mm +++ b/iset.mm @@ -7500,17 +7500,27 @@ converse also holds (see ~ pm5.6dc ). (Contributed by Jim Kingdon, ( wa simpl nsyl ) ABBCEDBCFG $. $} + ${ + dcand.1 $e |- ( ph -> DECID ps ) $. + dcand.2 $e |- ( ph -> DECID ch ) $. + $( A conjunction of two decidable propositions is decidable. (Contributed + by Jim Kingdon, 12-Apr-2018.) (Revised by BJ, 14-Nov-2024.) $) + dcand $p |- ( ph -> DECID ( ps /\ ch ) ) $= + ( wa wn wo wdc df-dc id intnanrd orim2i sylbi syl intnand sylanbrc sylibr + ordir ) ABCFZTGZHZTIABUAHZCUAHZUBABIZUCDUEBBGZHUCBJUFUABUFBCUFKLMNOACIZUD + EUGCCGZHUDCJUHUACUHCBUHKPMNOBCUASQTJR $. + $} + $( A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.) $) dcan $p |- ( ( DECID ph /\ DECID ps ) -> DECID ( ph /\ ps ) ) $= - ( wa wn wo simpl intnanrd orim2i simpr intnand olcd jaoi df-dc anbi12i andi - wdc andir orbi1i 3bitri 3imtr4i ) ABCZADZBCZEZAUBEZBDZCZEZUAUADZEZAPZBPZCZU - APUDUJUGUCUIUAUCABUBBFGHUGUIUAUGBAUEUFIJKLUMUEBUFEZCUEBCZUGEUHUKUEULUNAMBMN - UEBUFOUOUDUGAUBBQRSUAMT $. + ( wdc wa simpl simpr dcand ) ACZBCZDABHIEHIFG $. $( A conjunction of two decidable propositions is decidable, expressed in a - curried form as compared to ~ dcan . (Contributed by Jim Kingdon, - 12-Apr-2018.) $) + curried form as compared to ~ dcan . This is deprecated; it's trivial to + recreate with ~ ex , but it's here in case someone is using this older + form. (Contributed by Jim Kingdon, 12-Apr-2018.) + (New usage is discouraged.) $) dcan2 $p |- ( DECID ph -> ( DECID ps -> DECID ( ph /\ ps ) ) ) $= ( wdc wa dcan ex ) ACBCABDCABEF $. @@ -7525,8 +7535,8 @@ converse also holds (see ~ pm5.6dc ). (Contributed by Jim Kingdon, $( An equivalence of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.) $) dcbi $p |- ( DECID ph -> ( DECID ps -> DECID ( ph <-> ps ) ) ) $= - ( wdc wi wa wb dcim com12 dcan2 syl6c dfbi2 dcbii syl6ibr ) ACZBCZABDZBADZE - ZCZABFZCNOPCQCZSABGONUABAGHPQIJTRABKLM $. + ( wdc wi wa wb dcim com12 dcan ex syl6c dfbi2 dcbii syl6ibr ) ACZBCZABDZBAD + ZEZCZABFZCOPQCZRCZTABGPOUCBAGHUBUCTQRIJKUASABLMN $. $( Express conjunction in terms of implication. The forward direction, ~ annimim , is valid for all propositions, but as an equivalence, it @@ -7534,27 +7544,26 @@ converse also holds (see ~ pm5.6dc ). (Contributed by Jim Kingdon, 25-Apr-2018.) $) annimdc $p |- ( DECID ph -> ( DECID ps -> ( ( ph /\ -. ps ) <-> -. ( ph -> ps ) ) ) ) $= - ( wdc wn wa wi wb imandc adantl dcim imp dcn dcan2 syl5 con2bidc sylc mpbid - ex ) ACZBCZABDZEZABFZDGZSTEZUCUBDGZUDTUFSABHIUEUCCZUBCZUFUDGSTUGABJKSTUHTUA - CSUHBLAUAMNKUCUBOPQR $. + ( wdc wn wa wi wb imandc adantl dcim imp dcan sylan2 con2bidc sylc mpbid ex + dcn ) ACZBCZABDZEZABFZDGZSTEZUCUBDGZUDTUFSABHIUEUCCZUBCZUFUDGSTUGABJKTSUACU + HBRAUALMUCUBNOPQ $. $( Theorem *4.55 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 2-May-2018.) $) pm4.55dc $p |- ( DECID ph -> ( DECID ps -> ( -. ( -. ph /\ ps ) <-> ( ph \/ -. ps ) ) ) ) $= - ( wdc wn wa wo wb pm4.54dc imp dcn anim2i syl wi dcan2 jca con2bidc biimprd - dcor mpd bicomd ex ) ACZBCZADZBEZDZABDZFZGUBUCEZUHUFUIUEUHDGZUHUFGZUBUCUJAB - HIUIUKUJUIUHCZUECZEUKUJGZUIULUMUIUBUGCZEULUCUOUBBJKUBUOULAUGRILUBUCUMUBUDCU - CUMMAJUDBNLIOULUMUNUHUEPILQSTUA $. + ( wdc wn wa wo wb pm4.54dc imp dcor impel dcan sylan con2bidc sylc 3bitr2rd + dcn mpbird ex ) ACZBCZADZBEZDZABDZFZGTUAEZUFUDUFUDUGUFUDGZUCUFDGZTUAUIABHIU + GUFCZUCCZUHUIGTUECUJUAAUEJBQKTUBCUAUKAQUBBLMUFUCNORZULULPS $. $( Disjunction in terms of conjunction (De Morgan's law), for decidable propositions. Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by Jim Kingdon, 13-Dec-2021.) $) orandc $p |- ( ( DECID ph /\ DECID ps ) -> ( ( ph \/ ps ) <-> -. ( -. ph /\ -. ps ) ) ) $= - ( wdc wa wn wo pm4.56 dcn adantr adantl dcan2 sylc dcor imp con2bidc mpbii - wb ) ACZBCZDZAEZBEZDZABFZEQZUDUCEQZABGTUCCZUDCZUEUFQTUACZUBCZUGRUISAHISUJRB - HJUAUBKLRSUHABMNUCUDOLP $. + ( wdc wa wn wo wb pm4.56 dcn dcan syl2an dcor imp con2bidc sylc mpbii ) ACZ + BCZDZAEZBEZDZABFZEGZUCUBEGZABHSUBCZUCCZUDUEGQTCUACUFRAIBITUAJKQRUGABLMUBUCN + OP $. ${ mpbiran.1 $e |- ps $. @@ -7690,8 +7699,8 @@ converse also holds (see ~ pm5.6dc ). (Contributed by Jim Kingdon, 21-Apr-2018.) $) anordc $p |- ( DECID ph -> ( DECID ps -> ( ( ph /\ ps ) <-> -. ( -. ph \/ -. ps ) ) ) ) $= - ( wdc wa wn wo wb dcan2 ianordc bicomd a1d con2biddc syld ) ACZBCABDZCZOAEB - EFZEGABHNQONQOEZGPNRQABIJKLM $. + ( wdc wa wn wo wb dcan ex ianordc 3bitr2rd a1d con2biddc syld ) ACZBCZABDZC + ZQAEBEFZEGOPRABHIOSQOSQEZGROTSTSABJZUAUAKLMN $. $( Theorem *3.11 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, ~ pm3.1 , holds for all propositions, not @@ -10673,10 +10682,10 @@ The classical version (without the decidability conditions) is an axiom of ( ( ph /\ ( ps \/_ ch ) ) <-> ( ( ph /\ ps ) \/_ ( ph /\ ch ) ) ) ) ) ) $= ( wdc wxo wa wb wn dcbi imp wi annimdc pm5.32 notbii bitrdi sylan2 xornbidc - adantl anbi2d dcan2 adantrr adantrl sylc 3bitr4d exp32 ) ADZBDZCDZABCEZFZAB - FZACFZEZGUFUGUHFZFZABCGZHZFZUKULGZHZUJUMUNUFUPDZURUTGUGUHVABCIJUFVAFURAUPKZ - HZUTUFVAURVCGAUPLJVBUSABCMNOPUOUIUQAUNUIUQGZUFUGUHVDBCQJRSUOUKDZULDZUMUTGUF - UGVEUHUFUGVEABTJUAUFUHVFUGUFUHVFACTJUBUKULQUCUDUE $. + adantl anbi2d dcan adantrr adantrl sylc 3bitr4d exp32 ) ADZBDZCDZABCEZFZABF + ZACFZEZGUFUGUHFZFZABCGZHZFZUKULGZHZUJUMUNUFUPDZURUTGUGUHVABCIJUFVAFURAUPKZH + ZUTUFVAURVCGAUPLJVBUSABCMNOPUOUIUQAUNUIUQGZUFUGUHVDBCQJRSUOUKDZULDZUMUTGUFU + GVEUHABTUAUFUHVFUGACTUBUKULQUCUDUE $. $( Conjunction distributes over exclusive-or. (Contributed by Mario Carneiro and Jim Kingdon, 7-Oct-2018.) $) @@ -67978,15 +67987,15 @@ intersections of elements of the argument (see ~ elfi2 ). (Contributed $( Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.) $) dcfi $p |- ( ( A e. Fin /\ A. x e. A DECID ph ) -> DECID A. x e. A ph ) $= - ( vw vy vz cfn wcel wdc wral wa cv csn wceq raleq dcbid sylc dcbii sylibr - c0 cun wn wo ral0 orci df-dc mpbir a1i cdif simpr simplrr eldifad simp-4r - wss wsbc nfsbc1v nfdc sbceq1a wb cvv ralsnsg elv dcan2 ralunb findcard2sd - rspc ex simpl ) CGHZAIZBCJZKZABDLZJZIABTJZIZABELZJZIZABVQFLZMZUAZJZIZABCJ - ZIDEFCVMTNVNVOABVMTOPVMVQNVNVRABVMVQOPVMWBNVNWCABVMWBOPVMCNVNWEABVMCOPVPV - LVPVOVOUBZUCVOWFABUDUEVOUFUGUHVLVQGHZKZVQCUNZVTCVQUIHZKZKZVSWDWLVSKZVRABW - AJZKZIZWDWMVSWNIZWPWLVSUJWMABVTUOZIZWQWMVTCHVKWSWMVTCVQWHWIWJVSUKULVIVKWG - WKVSUMVJWSBVTCWRBABVTUPUQBLVTNAWRABVTURPVFQWNWRWNWRUSFABVTUTVAVBRSVRWNVCQ - WCWOABVQWAVDRSVGVIVKVHVE $. + ( vw vy vz cfn wcel wdc wral wa cv csn cun wceq raleq dcbid dcbii sylibr + c0 wn wo ral0 orci df-dc mpbir a1i wss cdif simpr simplrr eldifad simp-4r + wsbc nfsbc1v nfdc sbceq1a rspc wb cvv ralsns elv dcand ralunb findcard2sd + sylc ex simpl ) CGHZAIZBCJZKZABDLZJZIABTJZIZABELZJZIZABVQFLZMZNZJZIZABCJZ + IDEFCVMTOVNVOABVMTPQVMVQOVNVRABVMVQPQVMWBOVNWCABVMWBPQVMCOVNWEABVMCPQVPVL + VPVOVOUAZUBVOWFABUCUDVOUEUFUGVLVQGHZKZVQCUHZVTCVQUIHZKZKZVSWDWLVSKZVRABWA + JZKZIWDWMVRWNWLVSUJWMABVTUNZIZWNIWMVTCHVKWQWMVTCVQWHWIWJVSUKULVIVKWGWKVSU + MVJWQBVTCWPBABVTUOUPBLVTOAWPABVTUQQURVFWNWPWNWPUSFABVTUTVAVBRSVCWCWOABVQW + AVDRSVGVIVKVHVE $. $} @@ -94898,15 +94907,14 @@ nonnegative integers (cont.)". $) $( A nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by Alexander van der Vekens, 17-Jan-2018.) $) nn0n0n1ge2b $p |- ( N e. NN0 -> ( ( N =/= 0 /\ N =/= 1 ) <-> 2 <_ N ) ) $= - ( wcel cc0 wne c1 wa c2 wbr wdc wn wi wceq zdceq sylancl dcned sylc syl clt - cz wb cn0 nn0n0n1ge2 3expib nn0z 0z 1z dcan2 wo ianordc nnedc orbi12d bitrd - cle 2pos breq1 mpbiri a1d 1lt2 jaoi impcom 2z zltnle adantr mpbid ex sylbid - condc impbid ) AUABZACDZAEDZFZGAUMHZVIVJVKVMAUBUCVIVLIZVLJZVMJZKVMVLKVIVJIZ - VKIVNVIACVIASBZCSBACLZIZAUDZUEACMNZOZVIAEVIVRESBAELZIZWAUFAEMNZOVJVKUGPVIVO - VSWDUHZVPVIVOVJJZVKJZUHZWGVIVQVOWJTWCVJVKUIQVIWHVSWIWDVIVTWHVSTWBACUJQVIWEW - IWDTWFAEUJQUKULVIWGVPVIWGFAGRHZVPWGVIWKVSVIWKKWDVSWKVIVSWKCGRHUNACGRUOUPUQW - DWKVIWDWKEGRHURAEGRUOUPUQUSUTVIWKVPTZWGVIVRGSBWLWAVAAGVBNVCVDVEVFVLVMVGPVH - $. + ( wcel cc0 wne c1 wa c2 wbr wdc wn wi cz wceq zdceq sylancl dcned wo wb syl + clt cn0 nn0n0n1ge2 3expib nn0z 0z 1z dcand ianordc nnedc orbi12d bitrd 2pos + cle breq1 mpbiri a1d 1lt2 jaoi impcom 2z zltnle adantr mpbid ex sylbid sylc + condc impbid ) AUABZACDZAEDZFZGAUMHZVIVJVKVMAUBUCVIVLIVLJZVMJZKVMVLKVIVJVKV + IACVIALBZCLBACMZIZAUDZUEACNOZPZVIAEVIVPELBAEMZIZVSUFAENOZPUGVIVNVQWBQZVOVIV + NVJJZVKJZQZWEVIVJIVNWHRWAVJVKUHSVIWFVQWGWBVIVRWFVQRVTACUISVIWCWGWBRWDAEUISU + JUKVIWEVOVIWEFAGTHZVOWEVIWIVQVIWIKWBVQWIVIVQWICGTHULACGTUNUOUPWBWIVIWBWIEGT + HUQAEGTUNUOUPURUSVIWIVORZWEVIVPGLBWJVSUTAGVAOVBVCVDVEVLVMVGVFVH $. $( A nonnegative integer less than ` 1 ` is ` 0 ` . (Contributed by Paul Chapman, 22-Jun-2011.) $) @@ -130662,8 +130670,8 @@ equal to the half of the predecessor of the odd number (which is an even $( Decidablity lemma used in various proofs related to ` gcd ` . (Contributed by Jim Kingdon, 12-Dec-2021.) $) gcdmndc $p |- ( ( M e. ZZ /\ N e. ZZ ) -> DECID ( M = 0 /\ N = 0 ) ) $= - ( cz wcel wa cc0 wceq wdc 0z zdceq mpan2 adantr adantl dcan2 sylc ) ACDZBCD - ZEAFGZHZBFGZHZRTEHPSQPFCDZSIAFJKLQUAPQUBUAIBFJKMRTNO $. + ( cz wcel cc0 wceq wdc wa 0z zdceq mpan2 dcan syl2an ) ACDZAEFZGZBEFZGZOQHG + BCDZNECDZPIAEJKSTRIBEJKOQLM $. ${ $d K n x y z $. $d M n y $. $d n ph y $. $d ps x y z $. @@ -131002,18 +131010,17 @@ which defines the set we are taking the supremum of must (a) be true at A. y e. RR ( y < x -> E. z e. { n e. ZZ | ( n || X /\ n || Y ) } y < z ) ) ) $= ( vj cz wcel wa cc0 wceq wn cdvds wbr c1 wdc cn wral wrex cv 1zzd anbi12d - breq1 1dvds anim12i adantr cuz elnnuz biimpri simpll dvdsdc syl2an2 dcan2 - cfv simplr sylc adantlr wne simplll dvdsbnd nnuz rexeqi sylib id intnanrd - ralimi reximi syl sylancom simpllr intnand wo simpr wb 0z sylancl ianordc - zdceq mpbid df-ne orbi12i sylibr mpjaodan zsupcllemex ) EHIZFHIZJZEKLZFKL - ZJMZJZDUAZENOZWMFNOZJZPENOZPFNOZJZABCGDPWLUBWMPLWNWQWOWRWMPENUDWMPFNUDUCW - HWSWKWFWQWGWREUEFUEUFUGWHWMPUHUOZIZWPQZWKWHXAJWNQZWOQZXBXAWMRIZWHWFXCXEXA - WMUIUJZWFWGXAUKWMEULUMXAXEWHWGXDXFWFWGXAUPWMFULUMWNWOUNUQURWLEKUSZWPMZDGU - AUHUOZSZGWTTZFKUSZWLXGWFXKWFWGWKXGUTWFXGJZWNMZDXISZGWTTZXKXMXOGRTXPEDGVAX - OGRWTVBVCVDXOXJGWTXNXHDXIXNWNWOXNVEVFVGVHVIVJWLXLWGXKWFWGWKXLVKWGXLJZWOMZ - DXISZGWTTZXKXQXSGRTXTFDGVAXSGRWTVBVCVDXSXJGWTXRXHDXIXRWOWNXRVEVLVGVHVIVJW - LWIMZWJMZVMZXGXLVMWLWKYCWHWKVNWLWIQZWKYCVOWLWFKHIYDWFWGWKUKVPEKVSVQWIWJVR - VIVTXGYAXLYBEKWAFKWAWBWCWDWE $. + breq1 1dvds anim12i adantr cuz elnnuz biimpri simpll dvdsdc syl2an2 dcand + cfv simplr adantlr wne dvdsbnd rexeqi sylib id intnanrd ralimi reximi syl + nnuz ad4ant14 intnand ad4ant24 wo simpr wb 0z zdceq sylancl ianordc mpbid + df-ne orbi12i sylibr mpjaodan zsupcllemex ) EHIZFHIZJZEKLZFKLZJMZJZDUAZEN + OZWKFNOZJZPENOZPFNOZJZABCGDPWJUBWKPLWLWOWMWPWKPENUDWKPFNUDUCWFWQWIWDWOWEW + PEUEFUEUFUGWFWKPUHUOZIZWNQWIWFWSJWLWMWSWKRIZWFWDWLQWTWSWKUIUJZWDWEWSUKWKE + ULUMWSWTWFWEWMQXAWDWEWSUPWKFULUMUNUQWJEKURZWNMZDGUAUHUOZSZGWRTZFKURZWDXBX + FWEWIWDXBJZWLMZDXDSZGWRTZXFXHXJGRTXKEDGUSXJGRWRVGUTVAXJXEGWRXIXCDXDXIWLWM + XIVBVCVDVEVFVHWEXGXFWDWIWEXGJZWMMZDXDSZGWRTZXFXLXNGRTXOFDGUSXNGRWRVGUTVAX + NXEGWRXMXCDXDXMWMWLXMVBVIVDVEVFVJWJWGMZWHMZVKZXBXGVKWJWIXRWFWIVLWJWGQZWIX + RVMWJWDKHIXSWDWEWIUKVNEKVOVPWGWHVQVFVRXBXPXGXQEKVSFKVSVTWAWBWC $. $} ${ @@ -131024,17 +131031,17 @@ which defines the set we are taking the supremum of must (a) be true at sup ( { n e. ZZ | ( n || X /\ n || Y ) } , RR , < ) e. NN ) $= ( vj cz wcel wa cc0 wceq wn cv cdvds wbr c1 cn wdc wral wrex nnuz syl clt crab csup cuz cfv 1zzd breq1 anbi12d anim12i adantr elnnuz biimpri simpll - 1dvds dvdsdc syl2an2 simplr dcan2 sylc adantlr wne simplll dvdsbnd rexeqi - cr sylib id intnanrd ralimi sylancom simpllr intnand wo simpr wb 0z zdceq - reximi sylancl ianordc mpbid orbi12i sylibr mpjaodan zsupcl eleqtrrdi - df-ne ) BEFZCEFZGZBHIZCHIZGJZGZAKZBLMZWOCLMZGZAEUBVEUAUCNUDUEZOWNWRNBLMZN - CLMZGZDANWNUFWONIWPWTWQXAWONBLUGWONCLUGUHWJXBWMWHWTWIXABUNCUNUIUJWJWOWSFZ - WRPZWMWJXCGWPPZWQPZXDXCWOOFZWJWHXEXGXCWOUKULZWHWIXCUMWOBUOUPXCXGWJWIXFXHW - HWIXCUQWOCUOUPWPWQURUSUTWNBHVAZWRJZADKUDUEZQZDWSRZCHVAZWNXIWHXMWHWIWMXIVB - WHXIGZWPJZAXKQZDWSRZXMXOXQDORXRBADVCXQDOWSSVDVFXQXLDWSXPXJAXKXPWPWQXPVGVH - VIVRTVJWNXNWIXMWHWIWMXNVKWIXNGZWQJZAXKQZDWSRZXMXSYADORYBCADVCYADOWSSVDVFY - AXLDWSXTXJAXKXTWQWPXTVGVLVIVRTVJWNWKJZWLJZVMZXIXNVMWNWMYEWJWMVNWNWKPZWMYE - VOWNWHHEFYFWHWIWMUMVPBHVQVSWKWLVTTWAXIYCXNYDBHWGCHWGWBWCWDWESWF $. + cr 1dvds dvdsdc syl2an2 simplr dcand adantlr wne rexeqi sylib id intnanrd + dvdsbnd ralimi reximi ad4ant14 intnand ad4ant24 wo simpr wb zdceq sylancl + 0z ianordc mpbid df-ne orbi12i sylibr mpjaodan zsupcl eleqtrrdi ) BEFZCEF + ZGZBHIZCHIZGJZGZAKZBLMZWMCLMZGZAEUBUNUAUCNUDUEZOWLWPNBLMZNCLMZGZDANWLUFWM + NIWNWRWOWSWMNBLUGWMNCLUGUHWHWTWKWFWRWGWSBUOCUOUIUJWHWMWQFZWPPWKWHXAGWNWOX + AWMOFZWHWFWNPXBXAWMUKULZWFWGXAUMWMBUPUQXAXBWHWGWOPXCWFWGXAURWMCUPUQUSUTWL + BHVAZWPJZADKUDUEZQZDWQRZCHVAZWFXDXHWGWKWFXDGZWNJZAXFQZDWQRZXHXJXLDORXMBAD + VFXLDOWQSVBVCXLXGDWQXKXEAXFXKWNWOXKVDVEVGVHTVIWGXIXHWFWKWGXIGZWOJZAXFQZDW + QRZXHXNXPDORXQCADVFXPDOWQSVBVCXPXGDWQXOXEAXFXOWOWNXOVDVJVGVHTVKWLWIJZWJJZ + VLZXDXIVLWLWKXTWHWKVMWLWIPZWKXTVNWLWFHEFYAWFWGWKUMVQBHVOVPWIWJVRTVSXDXRXI + XSBHVTCHVTWAWBWCWDSWE $. $} ${ @@ -131310,27 +131317,26 @@ which defines the set we are taking the supremum of must (a) be true at wdc w3a cle gcddvds 3adant1 simpld simp1 1zzd cn0 gcdcl nn0zd simp2 dvds2ln simp3 syl23anc mpd mulid2d oveq2d breqtrd zmulcld zaddcld dvdslegcd syl3anc wn jca ex mpid znegcld gcdcld mulneg1d oveq12d mulcld negcld addcomd negidd - eqtr3d oveq1d addassd addid2d 3eqtr3d anim12d nn0red letri3d sylibrd wo 0zd - cneg wb zdceq dcan2 sylc orandc mul01d adantr eqeq1d pm5.32da oveq12 adantl - simpr syl6bir imp eqtr4d sylbid jaod sylbird dcn syl exmiddc mpjaod ) ADEZB - DEZCDEZUAZBCFGZBABHGZCIGZFGZBCXNIGZFGXLBJKZXOJKZLZVCZXRCJKZLZVCZLZXMXPKZYEV - CZXLYEXMXPUBMZXPXMUBMZLYFXLYAYHYDYIXLYAXMBNMZXMXONMZLZYHXLYJYKXLYJXMCNMZXJX - KYJYMLZXIBCUCUDZUEXLXMXNOCHGZIGZXONXLYNXMYQNMZYOXLXIODEZXMDEZXJXKYNYRPXIXJX - KUFZXLUGZXLXMXJXKXMUHEXIBCUIUDZUJZXIXJXKUKZXIXJXKUMZAOXMBCULUNUOXLYPCXNIXLC - XLCUUFQZUPUQURVDXLYTXJXODEZYAYLYHPZPUUDUUEXLXNCXLABUUAUUEUSUUFUTZYTXJUUHUAY - AUUIXMBXOVAVEVBVFXLYDXPBNMZXPCNMZLZYIXLUUKUULXLUUKXPXONMZXLXJUUHUUKUUNLZUUE - UUJBXOUCRZUEXLXPAWFZBHGZOXOHGZIGZCNXLUUOXPUUTNMZUUPXLUUQDEYSXPDEZXJUUHUUOUV - APXLAUUAVGUUBXLXPXLBXOUUEUUJVHZUJZUUEUUJUUQOXPBXOULUNUOXLUUTXNWFZXOIGZCXLUU - RUVEUUSXOIXLABXLAUUAQZXLBUUEQZVIXLXOXLXOUUJQUPVJXLUVEXNIGZCIGJCIGZUVFCXLUVI - JCIXLXNUVEIGUVIJXLXNUVEXLABUVGUVHVKZXLXNUVKVLZVMXLXNUVKVNVOVPXLUVEXNCUVLUVK - UUGVQXLCUUGVRZVSSURVDXLUVBXJXKYDUUMYIPZPUVDUUEUUFUVBXJXKUAYDUVNXPBCVAVEVBVF - VTXLXMXPXLXMUUCWAXLXPUVCWAWBWCXLYGXTYCWDZYFXLXTTZYCTZUVOYGWGXLXRTZXSTZUVPXL - XJJDEZUVRUUEXLWEZBJWHRZXLUUHUVTUVSUUJUWAXOJWHRXRXSWIWJZXLUVRYBTZUVQUWBXLXKU - VTUWDUUFUWACJWHRXRYBWIWJZXTYCWKRXLXTYFYCXLXTYCYFXLXRXSYBXLXRLZXOCJUWFXOUVJC - UWFXNJCIUWFXNAJHGZJUWFBJAHXLXRWRUQXLUWGJKXRXLAUVGWLWMSVPXLUVJCKXRUVMWMSWNWO - ZXLYCYFXLYCLXMJJFGZXPYCXMUWIKXLBJCJFWPWQXLYCXPUWIKZXLYCXTUWJUWHBJXOJFWPWSWT - XAVEZXBUWKXCXDXLYETZYEYGWDXLYATZYDTZUWLXLUVPUWMUWCXTXEXFXLUVQUWNUWEYCXEXFYA - YDWIWJYEXGXFXHXLXOXQBFXLXNCUVKUUGVMUQS $. + cneg eqtr3d oveq1d addassd addid2d 3eqtr3d syld3an1 anim12d letri3d sylibrd + nn0red wo 0zd zdceq dcand orandc simpr mul01d adantr eqeq1d pm5.32da oveq12 + wb adantl syl6bir imp eqtr4d sylbid jaod sylbird dcn syl exmiddc mpjaod ) A + DEZBDEZCDEZUAZBCFGZBABHGZCIGZFGZBCXNIGZFGXLBJKZXOJKZLZVCZXRCJKZLZVCZLZXMXPK + ZYEVCZXLYEXMXPUBMZXPXMUBMZLYFXLYAYHYDYIXLYAXMBNMZXMXONMZLZYHXLYJYKXLYJXMCNM + ZXJXKYJYMLZXIBCUCUDZUEXLXMXNOCHGZIGZXONXLYNXMYQNMZYOXLXIODEZXMDEZXJXKYNYRPX + IXJXKUFZXLUGZXLXMXJXKXMUHEXIBCUIUDZUJZXIXJXKUKZXIXJXKUMZAOXMBCULUNUOXLYPCXN + IXLCXLCUUFQZUPUQURVDXLYTXJXODEZYAYLYHPZPUUDUUEXLXNCXLABUUAUUEUSUUFUTZYTXJUU + HUAYAUUIXMBXOVAVEVBVFXLYDXPBNMZXPCNMZLZYIXLUUKUULXLUUKXPXONMZXLXJUUHUUKUUNL + ZUUEUUJBXOUCRZUEXLXPAVOZBHGZOXOHGZIGZCNXLUUOXPUUTNMZUUPXLUUQDEYSXPDEZXJUUHU + UOUVAPXLAUUAVGUUBXLXPXLBXOUUEUUJVHZUJZUUEUUJUUQOXPBXOULUNUOXLUUTXNVOZXOIGZC + XLUURUVEUUSXOIXLABXLAUUAQZXLBUUEQZVIXLXOXLXOUUJQUPVJXLUVEXNIGZCIGJCIGZUVFCX + LUVIJCIXLXNUVEIGUVIJXLXNUVEXLABUVGUVHVKZXLXNUVKVLZVMXLXNUVKVNVPVQXLUVEXNCUV + LUVKUUGVRXLCUUGVSZVTSURVDUVBXJXIXKYDUUMYIPZPUVDUVBXJXKUAYDUVNXPBCVAVEWAVFWB + XLXMXPXLXMUUCWEXLXPUVCWEWCWDXLYGXTYCWFZYFXLXTTZYCTZUVOYGWQXLXRXSXLXJJDEZXRT + UUEXLWGZBJWHRZXLUUHUVRXSTUUJUVSXOJWHRWIZXLXRYBUVTXLXKUVRYBTUUFUVSCJWHRWIZXT + YCWJRXLXTYFYCXLXTYCYFXLXRXSYBXLXRLZXOCJUWCXOUVJCUWCXNJCIUWCXNAJHGZJUWCBJAHX + LXRWKUQXLUWDJKXRXLAUVGWLWMSVQXLUVJCKXRUVMWMSWNWOZXLYCYFXLYCLXMJJFGZXPYCXMUW + FKXLBJCJFWPWRXLYCXPUWFKZXLYCXTUWGUWEBJXOJFWPWSWTXAVEZXBUWHXCXDXLYETYEYGWFXL + YAYDXLUVPYATUWAXTXEXFXLUVQYDTUWBYCXEXFWIYEXGXFXHXLXOXQBFXLXNCUVKUUGVMUQS $. $( The GCD of two numbers is the same as the GCD of the left and their sum. (Contributed by Scott Fenton, 20-Apr-2014.) $) @@ -132436,18 +132442,33 @@ integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 25-Oct-2024.) $) nnwosdc $p |- ( ( E. x e. NN ph /\ A. x e. NN DECID ph ) -> E. x e. NN ( ph /\ A. y e. NN ( ps -> x <_ y ) ) ) $= - ( vw vj cn wrex wdc wral wa cv wcel wex wi sylibr nfcv wal df-rex wss w3a - crab cle wbr rabn0m ssrab2 biantrur sylbb1 wsb wn wo animorrl df-dc nfs1v - nfdc weq sbequ12 dcbid rspc impcom dcan2 sylc elrabf dcbii anim12i df-3an - nfrab1 nnwofdc rabid df-ral elrab imbi1i impexp bitri albii anbi12i exbii - ralrimiva anbi2i anass bitr3i bitr4i 3bitri sylib syl ) ACHIZAJZCHKZLZACH - UCZHUAZFMWKNFOZGMZWKNZJZGHKZUBZABCMZDMZUDUEZPZDHKZLZCHIZWJWLWMLZWQLWRWGXF - WIWQWMWGXFACFHUFWLWMACHUGUHUIWIWPGHWIWNHNZLZXGACGUJZLZJZWPXHXGJZXIJZXKXHX - GXGUKZULXLWIXGXNUMXGUNQXGWIXMWHXMCWNHXICACGUOZUPCGUQAXIACGURZUSUTVAXGXIVB - VCWOXJAXICWNHCWNRCHRXOXPVDVEQVSVFWLWMWQVGQWRXADWKKZCWKIZXECDFWKGACHVHDWKR - VIXRWSWKNZXQLZCOWSHNZALZWTHNZXBPZDSZLZCOZXEXQCWKTXTYFCXSYBXQYEACHVJXQWTWK - NZXAPZDSYEXADWKVKYIYDDYIYCBLZXAPYDYHYJXAABCWTHEVLVMYCBXAVNVOVPVOVQVRYGYAX - DLZCOXEYFYKCYFYBXCLYKXCYEYBXBDHVKVTYAAXCWAWBVRXDCHTWCWDWEWF $. + ( vw vj cn wrex wdc wral wa cv wcel wex wi sylibr weq nfcv 3bitr2d rabn0m + crab wss w3a cle wbr ssrab2 biantrur sylbb1 wsb wn wo animorrl df-dc nfdc + nfs1v sbequ12 dcbid rspc impcom dcand elrabf dcbii anim12i df-3an nnwofdc + ralrimiva nfrab1 wal df-rex rabid df-ral elrab imbi1i bitri albii anbi12i + impexp exbii anbi2i anass bitr3i bitr4i 3bitri sylib syl ) ACHIZAJZCHKZLZ + ACHUBZHUCZFMWKNFOZGMZWKNZJZGHKZUDZABCMZDMZUEUFZPZDHKZLZCHIZWJWLWMLZWQLWRW + GXFWIWQWMWGXFACFHUAWLWMACHUGUHUIWIWPGHWIWNHNZLZXGACGUJZLZJWPXHXGXIXHXGXGU + KZULXGJWIXGXKUMXGUNQXGWIXIJZWHXLCWNHXICACGUPZUOCGRAXIACGUQZURUSUTVAWOXJAX + ICWNHCWNSCHSXMXNVBVCQVGVDWLWMWQVEQWRXADWKKZCWKIZXECDFWKGACHVHDWKSVFXPWSWK + NZXOLZCOWSHNZALZWTHNZXBPZDVIZLZCOZXEXOCWKVJXRYDCXQXTXOYCACHVKXOWTWKNZXAPZ + DVIYCXADWKVLYGYBDYGYABLZXAPYBYFYHXAABCWTHCDRZABABEEYIABABEEYIABABEEYIABAB + EEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABE + EYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEE + YIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEY + IABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYI + ABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIA + BABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIAB + ABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABA + BEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABAB + EEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABE + EYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEE + YIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEY + IABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYIABABEEYI + ABABEEYIABABEEYIABABEEYIABABEEETTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTT + TTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTT + TTVMVNYABXAVRVOVPVOVQVSYEXSXDLZCOXEYDYJCYDXTXCLYJXCYCXTXBDHVLVTXSAXCWAWBV + SXDCHVJWCWDWEWF $. $} @@ -132897,26 +132918,25 @@ According to Wikipedia ("Least common multiple", 27-Aug-2020, lcmval $p |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) = if ( ( M = 0 \/ N = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) ) $= - ( vx vy cz wcel wa cv cc0 wceq cdvds wbr cn crab cr clt cfv c1 syl2anc wo + ( vx vy cz wcel wa cv cc0 wceq wo cdvds wbr cn cr clt cfv c1 syl2anc crab cinf cif clcm cvv cmpo df-lcm eqeq1 orbi1d breq1 rabbidv infeq1d ifbieq2d a1i anbi1d orbi2d anbi2d sylan9eq adantl simpl simpr c0ex wn cmul co cabs - 1zzd cuz nnuz rabeq ax-mp dvdsmul1 adantr wb simpll simplr dvdsabsb mpbid - zmulcld dvdsmul2 zcnd absmuld ioran simpld neqned nnabscl simprd nnmulcld - wne sylib eqeltrd anbi12d elrab3 syl mpbir2and cfz elfzelz zdvdsdc syl2an - breq2 wdc dcan2 sylc infssuzcldc elexd lcmmndc ifcldadc ovmpod ) BFGZCFGZ - HZDEBCFFDIZJKZEIZJKZUAZJXLAIZLMZXNXQLMZHZANOZPQUBZUCZBJKZCJKZUAZJBXQLMZCX - QLMZHZANOZPQUBZUCZUDUEUDDEFFYCUFKXKDEAUGUNXLBKZXNCKZHYCYLKXKYMYNYCYDXOUAZ - JYGXSHZANOZPQUBZUCYLYMXPYOYBYRJYMXMYDXOXLBJUHUIYMPYAYQQYMXTYPANYMXRYGXSXL - BXQLUJUOUKULUMYNYOYFYRYKJYNXOYEYDXNCJUHUPYNPYQYJQYNYPYIANYNXSYHYGXNCXQLUJ - UQUKULUMURUSXIXJUTXIXJVAXKYFJYKUEJUEGXKYFHVBUNXKYFVCZHZYKYJYTYIBCVDVEZVFR - ZYJASYTVGNSVHRZKYJYIAUUCOKVIYIANUUCVJVKYTUUBYJGZBUUBLMZCUUBLMZYTBUUALMZUU - EXKUUGYSBCVLVMYTXIUUAFGZUUGUUEVNXIXJYSVOZYTBCUUIXIXJYSVPZVSZBUUAVQTVRYTCU - UALMZUUFXKUULYSBCVTVMYTXJUUHUULUUFVNUUJUUKCUUAVQTVRYTUUBNGUUDUUEUUFHZVNYT - UUBBVFRZCVFRZVDVENYTBCYTBUUIWAYTCUUJWAWBYTUUNUUOYTXIBJWIUUNNGUUIYTBJYTYDV - CZYEVCZYTYSUUPUUQHXKYSVAYDYEWCWJZWDWEBWFTYTXJCJWIUUONGUUJYTCJYTUUPUUQUURW - GWECWFTWHWKYIUUMAUUBNXQUUBKYGUUEYHUUFXQUUBBLWTXQUUBCLWTWLWMWNWOYTXQSUUBWP - VEGZHYGXAZYHXAZYIXAYTXIXQFGZUUTUUSUUIXQSUUBWQZBXQWRWSYTXJUVBUVAUUSUUJUVCC - XQWRWSYGYHXBXCXDXEBCXFXGXH $. + 1zzd cuz nnuz rabeqi dvdsmul1 adantr simpll simplr zmulcld dvdsabsb mpbid + wb dvdsmul2 zcnd absmuld wne ioran simpld neneqad nnabscl simprd nnmulcld + sylib eqeltrd anbi12d elrab3 syl mpbir2and cfz wdc elfzelz zdvdsdc syl2an + breq2 dcand infssuzcldc elexd lcmmndc ifcldadc ovmpod ) BFGZCFGZHZDEBCFFD + IZJKZEIZJKZLZJXJAIZMNZXLXOMNZHZAOUAZPQUBZUCZBJKZCJKZLZJBXOMNZCXOMNZHZAOUA + ZPQUBZUCZUDUEUDDEFFYAUFKXIDEAUGUNXJBKZXLCKZHYAYJKXIYKYLYAYBXMLZJYEXQHZAOU + AZPQUBZUCYJYKXNYMXTYPJYKXKYBXMXJBJUHUIYKPXSYOQYKXRYNAOYKXPYEXQXJBXOMUJUOU + KULUMYLYMYDYPYIJYLXMYCYBXLCJUHUPYLPYOYHQYLYNYGAOYLXQYFYEXLCXOMUJUQUKULUMU + RUSXGXHUTXGXHVAXIYDJYIUEJUEGXIYDHVBUNXIYDVCZHZYIYHYRYGBCVDVEZVFRZYHASYRVG + YGAOSVHRVIVJYRYTYHGZBYTMNZCYTMNZYRBYSMNZUUBXIUUDYQBCVKVLYRXGYSFGZUUDUUBVR + XGXHYQVMZYRBCUUFXGXHYQVNZVOZBYSVPTVQYRCYSMNZUUCXIUUIYQBCVSVLYRXHUUEUUIUUC + VRUUGUUHCYSVPTVQYRYTOGUUAUUBUUCHZVRYRYTBVFRZCVFRZVDVEOYRBCYRBUUFVTYRCUUGV + TWAYRUUKUULYRXGBJWBUUKOGUUFYRBJYRYBVCZYCVCZYRYQUUMUUNHXIYQVAYBYCWCWIZWDWE + BWFTYRXHCJWBUULOGUUGYRCJYRUUMUUNUUOWGWECWFTWHWJYGUUJAYTOXOYTKYEUUBYFUUCXO + YTBMWTXOYTCMWTWKWLWMWNYRXOSYTWOVEGZHYEYFYRXGXOFGZYEWPUUPUUFXOSYTWQZBXOWRW + SYRXHUUQYFWPUUPUUGUURCXOWRWSXAXBXCBCXDXEXF $. $} ${ @@ -132951,20 +132971,19 @@ According to Wikipedia ("Least common multiple", 27-Aug-2020, lcmcllem $p |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) e. { n e. NN | ( M || n /\ N || n ) } ) $= ( cz wcel wa cc0 wceq wn co cdvds wbr cn c1 wne cap zapne syl2anc mpbid - wb wo clcm cv crab cr clt cinf lcmn0val cmul cabs cfv 1zzd cuz nnuz rabeq - ax-mp simpll simplr zmulcld zcnd ioran biimpi adantl simpld neqned mpbird - 0zd simprd mulap0d nnabscl dvdsmul1 zmulcl dvdsabsb syldan sylan2 anabss7 - dvdsmul2 jca breq2 anbi12d elrab sylanbrc cfz wdc simplll elfzelz zdvdsdc - adantr simpllr dcan2 sylc infssuzcldc eqeltrd ) BDEZCDEZFZBGHZCGHZUAIZFZB - CUBJBAUCZKLZCXAKLZFZAMUDZUEUFUGXEABCUHWTXDBCUIJZUJUKZXEANWTULMNUMUKZHXEXD - AXHUDHUNXDAMXHUOUPWTXGMEZBXGKLZCXGKLZFZXGXEEWTXFDEZXFGOZXIWTBCWNWOWSUQZWN - WOWSURZUSZWTXFGPLZXNWTBCWTBXOUTWTCXPUTWTBGPLZBGOZWTBGWTWQIZWRIZWSYAYBFZWP - WSYCWQWRVAVBVCZVDVEWTWNGDEZXSXTTXOWTVGZBGQRVFWTCGPLZCGOZWTCGWTYAYBYDVHVEW - TWOYEYGYHTXPYFCGQRVFVIWTXMYEXRXNTXQYFXFGQRSXFVJRWPXLWSWPXJXKWPBXFKLZXJBCV - KWNWOXMYIXJTBCVLZBXFVMVNSWPCXFKLZXKBCVQWNWOYKXKTZWPWOXMYLYJCXFVMVOVPSVRWH - XDXLAXGMXAXGHXBXJXCXKXAXGBKVSXAXGCKVSVTWAWBWTXANXGWCJEZFZXBWDZXCWDZXDWDYN - WNXADEZYOWNWOWSYMWEYMYQWTXANXGWFVCZBXAWGRYNWOYQYPWNWOWSYMWIYRCXAWGRXBXCWJ - WKWLWM $. + wb wo clcm cv crab cr clt cinf lcmn0val cmul cabs cfv 1zzd cuz nnuz breq2 + rabeqi anbi12d simpll simplr zmulcld zcnd ioran biimpi adantl neneqad 0zd + simpld mpbird simprd mulap0d dvdsmul1 zmulcl dvdsabsb syldan dvdsmul2 jca + nnabscl sylan2 anabss7 adantr cfz wdc simplll elfzelz zdvdsdc infssuzcldc + elrabd simpllr dcand eqeltrd ) BDEZCDEZFZBGHZCGHZUAIZFZBCUBJBAUCZKLZCWRKL + ZFZAMUDZUEUFUGXBABCUHWQXABCUIJZUJUKZXBANWQULXAAMNUMUKUNUPWQXABXDKLZCXDKLZ + FZAXDMWRXDHWSXEWTXFWRXDBKUOWRXDCKUOUQWQXCDEZXCGOZXDMEWQBCWKWLWPURZWKWLWPU + SZUTZWQXCGPLZXIWQBCWQBXJVAWQCXKVAWQBGPLZBGOZWQBGWQWNIZWOIZWPXPXQFZWMWPXRW + NWOVBVCVDZVGVEWQWKGDEZXNXOTXJWQVFZBGQRVHWQCGPLZCGOZWQCGWQXPXQXSVIVEWQWLXT + YBYCTXKYACGQRVHVJWQXHXTXMXITXLYAXCGQRSXCVQRWMXGWPWMXEXFWMBXCKLZXEBCVKWKWL + XHYDXETBCVLZBXCVMVNSWMCXCKLZXFBCVOWKWLYFXFTZWMWLXHYGYECXCVMVRVSSVPVTWGWQW + RNXDWAJEZFZWSWTYIWKWRDEZWSWBWKWLWPYHWCYHYJWQWRNXDWDVDZBWRWERYIWLYJWTWBWKW + LWPYHWHYKCWRWERWIWFWJ $. $( Closure of the ` lcm ` operator. (Contributed by Steve Rodriguez, 20-Jan-2020.) $) @@ -132992,15 +133011,14 @@ According to Wikipedia ("Least common multiple", 27-Aug-2020, lcmledvds $p |- ( ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) <_ K ) ) $= - ( vn cn wcel cz cc0 wceq wa cdvds wbr co cle c1 breq2 wdc zdvdsdc syl2anc - crab w3a wo wn clcm cv cr clt cinf lcmn0val 3adantl1 adantr 1zzd cuz nnuz - cfv rabeq ax-mp simpll1 simpr anbi12d sylanbrc cfz simpll2 elfzelz adantl - elrab simpll3 dcan2 sylc adantlr infssuzledc eqbrtrd ex ) AEFZBGFZCGFZUAB - HICHIUBUCZJZBAKLZCAKLZJZBCUDMZANLVRWAJZWBBDUEZKLZCWDKLZJZDETZUFUGUHZANVRW - BWIIZWAVOVPVQWJVNDBCUIUJUKWCWGAWHDOWCULEOUMUOZIWHWGDWKTIUNWGDEWKUPUQWCVNW - AAWHFVNVOVPVQWAURVRWAUSWGWADAEWDAIWEVSWFVTWDABKPWDACKPUTVFVAVRWDOAVBMFZWG - QZWAVRWLJZWEQZWFQZWMWNVOWDGFZWOVNVOVPVQWLVCWLWQVRWDOAVDVEZBWDRSWNVPWQWPVN - VOVPVQWLVGWRCWDRSWEWFVHVIVJVKVLVM $. + ( vn cn wcel cz w3a cc0 wceq wa cdvds wbr co cle c1 breq2 zdvdsdc syl2anc + wdc wo wn clcm cv crab cr clt cinf lcmn0val 3adantl1 adantr 1zzd cuz nnuz + cfv rabeqi anbi12d simpll1 simpr elrabd cfz simpll2 elfzelz simpll3 dcand + adantl adantlr infssuzledc eqbrtrd ex ) AEFZBGFZCGFZHBIJCIJUAUBZKZBALMZCA + LMZKZBCUCNZAOMVOVRKZVSBDUDZLMZCWALMZKZDEUEZUFUGUHZAOVOVSWFJZVRVLVMVNWGVKD + BCUIUJUKVTWDAWEDPVTULWDDEPUMUOUNUPVTWDVRDAEWAAJWBVPWCVQWAABLQWAACLQUQVKVL + VMVNVRURVOVRUSUTVOWAPAVANFZWDTVRVOWHKZWBWCWIVLWAGFZWBTVKVLVMVNWHVBWHWJVOW + APAVCVFZBWARSWIVMWJWCTVKVLVMVNWHVDWKCWARSVEVGVHVIVJ $. $} $( The lcm of two integers is zero iff either is zero. (Contributed by Steve @@ -134194,13 +134212,12 @@ According to Wikipedia ("Least common multiple", 27-Aug-2020, ( vx cn wcel c2 cuz wbr wn c1 co wral wa wdc wo cz a1i syl adantl syl2anc cle cfv cv cdvds cmin cfz cprime wceq 1nuz2 mtbiri orim1i orcomd elnn1uz2 eleq1 df-dc 3imtr4i cfn 2z nnz peano2zm fzfigd elfzelz 1red 2re zred 1le2 - elfzle1 letrd elnnz1 sylanbrc adantr dvdsdc dcn ralrimiva dcfi dcan2 sylc - cr isprm3 dcbii sylibr ) ACDZAEFUAZDZBUBZAUCGZHZBEAIUDJZUEJZKZLZMZAUFDZMW - AWCMZWIMZWKAIUGZWCNZWCWCHZNWAWMWPWQWCWOWQWCWOWCIWBDUHAIWBUMUIUJUKAULWCUNU - OWAWHUPDWFMZBWHKWNWAEWGEODWAUQPWAAODZWGODAURZAUSQUTWAWRBWHWAWDWHDZLZWEMZW - RXBWDCDZWSXCXBWDODZIWDTGXDXAXEWAWDEWGVARZXBIEWDXBVBEVQDXBVCPXBWDXFVDIETGX - BVEPXAEWDTGWAWDEWGVFRVGWDVHVIWAWSXAWTVJWDAVKSWEVLQVMWFBWHVNSWCWIVOVPWLWJB - AVRVSVT $. + cr elfzle1 letrd elnnz1 sylanbrc adantr dvdsdc dcn ralrimiva dcand isprm3 + dcfi dcbii sylibr ) ACDZAEFUAZDZBUBZAUCGZHZBEAIUDJZUEJZKZLZMAUFDZMVTWBWHA + IUGZWBNZWBWBHZNVTWBMWLWMWBWKWMWBWKWBIWADUHAIWAUMUIUJUKAULWBUNUOVTWGUPDWEM + ZBWGKWHMVTEWFEODVTUQPVTAODZWFODAURZAUSQUTVTWNBWGVTWCWGDZLZWDMZWNWRWCCDZWO + WSWRWCODZIWCTGWTWQXAVTWCEWFVARZWRIEWCWRVBEVFDWRVCPWRWCXBVDIETGWRVEPWQEWCT + GVTWCEWFVGRVHWCVIVJVTWOWQWPVKWCAVLSWDVMQVNWEBWGVQSVOWJWIBAVPVRVS $. $} ${ @@ -137204,15 +137221,19 @@ given prime (or other positive integer) that divides the number. For Jim Kingdon, 8-Oct-2024.) $) pclemdc $p |- ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> A. x e. ZZ DECID x e. A ) $= - ( c2 wcel cz wa cv wdc cn0 wn cexp co cdvds wbr simpr sylibr cuz zexpcl - cfv cc0 wne elnn0dc ad2antlr eluzelz ad3antrrr syl2anc ad2antrr zdvdsdc - simprl dcan2 sylc oveq2 breq1d elrab2 dcbii intnanrd olcd df-dc exmiddc - weq wo syl adantl mpjaodan ralrimiva ) CGUAUCHZEIHZEUDUEZJZJZAKZBHZLZAI - VNVOIHZJZVOMHZVQVTNZVSVTJZVTCVOOPZEQRZJZLZVQWBVTLZWDLZWFVRWGVNVTVOUFZUG - WBWCIHZVKWHWBCIHZVTWJVJWKVMVRVTGCUHUIVSVTSCVOUBUJVNVKVRVTVJVKVLUMUKWCEU - LUJVTWDUNUOVPWECDKZOPZEQRWDDVOMBDAVDWMWCEQWLVOCOUPUQFURUSZTVSWAJZWFVQWO - WEWENZVEWFWOWPWEWOVTWDVSWASUTVAWEVBTWNTVRVTWAVEZVNVRWGWQWIVTVCVFVGVHVI - $. + ( c2 wcel cz wa cv wdc cn0 wn cexp co cdvds wbr sylibr 3eqtr2i ad2antlr + cuz cfv cc0 wne elnn0dc eluzelz zexpcl sylancom simprl ad2antrr zdvdsdc + ad3antrrr syl2anc dcand weq oveq2 breq1d elrab2 dcbii wo simpr intnanrd + olcd df-dc crab exmiddc syl adantl mpjaodan ralrimiva ) CGUBUCHZEIHZEUD + UEZJZJZAKZBHZLZAIVPVQIHZJZVQMHZVSWBNZWAWBJZWBCVQOPZEQRZJZLZVSWDWBWFVTWB + LZVPWBVQUFZUAWDWEIHZVMWFLWAWBCIHZWKVLWLVOVTWBGCUGUMCVQUHUIVPVMVTWBVLVMV + NUJUKWEEULUNUOVRWGCDKZOPZEQRZWFDVQMBDAUPWNWEEQWMVQCOUQURZFUSUTSWAWCJZWH + VSWQWGWGNZVAWHWQWRWGWQWBWFWAWCVBVCVDWGVESVRWGWOWFDVQMBWPBWODMVFZBWSFFBW + SBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFB + WSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFF + BWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSFFBWSBWSF + FBWSBWSFFFTTTTTTTTTTTTTTTTTTTTTTTTTTTTTUSUTSVTWBWCVAZVPVTWIWTWJWBVGVHVI + VJVK $. $} pclem.2 $e |- S = sup ( A , RR , < ) $. @@ -138390,23 +138411,30 @@ given prime (or other positive integer) that divides the number. For (Contributed by Mario Carneiro, 12-Mar-2014.) $) pcmptdvds $p |- ( ph -> ( seq 1 ( x. , F ) ` N ) || ( seq 1 ( x. , F ) ` M ) ) $= - ( vm c1 wbr cz wcel cc0 cle cprime cn0 cn vp cmul cseq cfv cdvds cdiv cpc - co cv wral wa wn csb cif wdc nfv nfcsb1v nfel1 weq csbeq1a eleq1d cbvralw - sylib csbeq1 rspcv mpan9 nn0ge0d 0le0 a1i prmz cuz eluzelz adantr syl2an2 - syl zdcle nnzd dcan2 sylc breq2 ifbothdc syl3anc cexp cmpt nfcv nfov nfif - dcn eleq1w id ifbieq1d cbvmpt eqtri simpr pcmpt2 breqtrrd ralrimiva cq wb - oveq12d wf pcmptcl simprd eluznn syl2anc ffvelrnd znq pcz mpbird dvdsval2 - wne nnne0d ) AFUBDLUCZUDZEXMUDZUEMZXOXNUFUHZNOZAXRPUAUIZXQUGUHZQMZUARUJZA - YAUARAXSROZUKZPXSEQMZXSFQMZULZUKZCXSBUMZPUNZXTQYDPYIQMZPPQMZYHUOZPYJQMZYD - YIACKUIZBUMZSOZKRUJZYCYISOZABSOZCRUJYRHYTYQCKRYTKUPCYPSCYOBUQZURCKUSZBYPS - CYOBUTZVAVBVCZYQYSKXSRKUAUSYPYISCYOXSBVDZVAVEVFVGYLYDVHVIYDYEUOZYGUOZYMYC - XSNOZAENOZUUFXSVJZAUUIYCAEFVKUDOZUUIJFEVLVOVMXSEVPVNYDYFUOZUUGYCUUHAFNOUU - LUUJYDFAFTOZYCIVMZVQXSFVPVNYFWHVOYEYGVRVSYHYKYLYNYIPYIYJPQVTPYJPQVTWAWBYD - YPYIXSKDEFDCTCUIZROZUUOBWCUHZLUNZWDKTYOROZYOYPWCUHZLUNZWDGCKTUURUVAKUURWE - UUSCUUTLUUSCUPCYOYPWCCYOWECWCWEUUAWFCLWEWGUUBUUPUUSUUQUUTLCKRWIUUBUUOYOBY - PWCUUBWJUUCWTWKWLWMAYRYCUUDVMUUNAYCWNUUEAUUKYCJVMWOWPWQAXQWROZXRYBWSAXONO - ZXNTOUVBAXOATTEXMATTDXATTXMXAABCDGHXBXCZAUUMUUKETOIJEFXDXEXFVQZATTFXMUVDI - XFZXOXNXGXEXQUAXHVOXIAXNNOXNPXKUVCXPXRWSAXNUVFVQAXNUVFXLUVEXNXOXJWBXI $. + ( vm c1 wbr cz wcel cc0 cle cprime cn 3eqtr2i vp cmul cseq cfv cdvds cdiv + co cv cpc wral wa wn csb cif wdc cn0 nfv nfcsb1v nfel1 weq csbeq1a eleq1d + cbvral sylib csbeq1 rspcv mpan9 nn0ge0d 0le0 a1i prmz cuz eluzelz syl2anr + syl zdcle adantr nnzd syl2an2 dcand breq2 ifbothdc syl3anc cexp cmpt nfcv + nfov nfif eleq1 id oveq12d ifbieq1d cbvmpt eqtri simpr breqtrrd ralrimiva + dcn pcmpt2 cq wb wf pcmptcl simprd eluznn syl2anc ffvelrnd znq pcz mpbird + wne nnne0d dvdsval2 ) AFUBDLUCZUDZEXNUDZUEMZXPXOUFUGZNOZAXSPUAUHZXRUIUGZQ + MZUARUJZAYBUARAXTROZUKZPXTEQMZXTFQMZULZUKZCXTBUMZPUNZYAQYEPYJQMZPPQMZYIUO + PYKQMZYEYJACKUHZBUMZUPOZKRUJZYDYJUPOZABUPOZCRUJYRHYTYQCKRYTKUQCYPUPCYOBUR + ZUSCKUTZBYPUPCYOBVAZVBVCVDZYQYSKXTRKUAUTYPYJUPCYOXTBVEZVBVFVGVHYMYEVIVJYE + YFYHYDXTNOZENOZYFUOAXTVKZAEFVLUDOZUUGJFEVMVOXTEVPVNYEYGUOZYHUOYDUUFAFNOUU + JUUHYEFAFSOZYDIVQZVRXTFVPVSYGWRVOVTYIYLYMYNYJPYJYKPQWAPYKPQWAWBWCYEYPYJXT + KDEFDCSCUHZROZUUMBWDUGZLUNZWEZKSYOROZYOYPWDUGZLUNZWEGCKSUUPUUTKUUPWFUURCU + USLUURCUQCYOYPWDCYOWFCWDWFUUAWGCLWFWHUUBUUNUURUUOUUSLUUMYORWIUUBUUMYOBYPW + DUUBWJUUCWKWLWMWNAYRYDUUDVQUULAYDWOUUEAUUIYDJVQWSWPWQAXRWTOZXSYCXAAXPNOZX + OSOUVAAXPASSEXNASSDXBZSSXNXBZABCDGHXCXDZAUUKUUIESOIJEFXEXFZXGVRASSFXNUVEI + XGZXPXOXHXFXRUAXIVOXJAXONOXOPXKUVBXQXSXAAXOUVGVRAXOUVGXLAXPASSEXNAUVCUVDA + BCDDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGG + DUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUU + QDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDU + UQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQG + GDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDU + UQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGDUUQDUUQGGGTTTTTTTTTTTTTTTTTTTTTTTT + TTTTTTTTTTTTTTTTTHXCXDUVFXGVRXOXPXMWCXJ $. $} ${ @@ -138939,19 +138967,26 @@ given prime (or other positive integer) that divides the number. For 5-May-2005.) $) infpnlem2 $p |- ( N e. NN -> E. j e. NN ( N < j /\ A. k e. NN ( ( j / k ) e. NN -> ( k = 1 \/ k = j ) ) ) ) $= - ( cn wcel c1 cv clt wbr cdiv co wa wral wrex wceq wdc cz syl2anc wi caddc - cle wo cfa cfv nnnn0 faccld peano2nnd eqeltrid nnge1d wb nnleltp1 sylancr - 1nn mpbid breqtrrdi cc cc0 cap nncn nnap0 jca dividap 3syl eqeltrdi breq2 - oveq2 eleq1d anbi12d rspcev syl12anc 1zzd adantl zdclt cdvds simpr adantr - nnzd dvdsdc nndivdvds dcbid sylan dcan2 sylc ralrimiva infpnlem1 reximdva - nnz nnwosdc mpd ) DFGZHAIZJKZCWMLMZFGZNZHBIZJKZCWRLMZFGZNZWMWRUCKUABFONZA - FPZDWMJKWMWRLMFGWRHQWRWMQUDUABFONZAFPWLWQAFPZWQRZAFOXDWLCFGZHCJKZCCLMZFGZ - XFWLCDUEUFZHUBMZFEWLXLWLDDUGUHZUIUJZWLHXMCJWLHXLUCKZHXMJKZWLXLXNUKWLHFGXL - FGXPXQULUOXNHXLUMUNUPEUQWLXJHFWLXHCURGZCUSUTKZNXJHQXOXHXRXSCVACVBVCCVDVEU - OVFWQXIXKNACFWMCQZWNXIWPXKWMCHJVGXTWOXJFWMCCLVHVIVJVKVLWLXGAFWLWMFGZNZWNR - ZWPRZXGYBHSGWMSGZYCYBVMYAYEWLWMWIVNHWMVOTYBWMCVPKZRZYDYBYACSGYGWLYAVQYBCW - LXHYAXOVRVSWMCVTTWLXHYAYGYDULXOXHYANYFWPCWMWAWBWCUPWNWPWDWEWFWQXBABWMWRQZ - WNWSWPXAWMWRHJVGYHWOWTFWMWRCLVHVIVJWJTWLXCXEAFBCWMDEWGWHWK $. + ( cn wcel c1 clt wbr cdiv co wa wral wrex wceq wdc cz syl2anc 3eqtr2i cle + cv wi wo cfa cfv caddc nnnn0 faccld peano2nnd eqeltrid nnge1d wb nnleltp1 + 1nn sylancr mpbid breqtrrdi cc0 cap nncn nnap0 jca dividap eqeltrdi breq2 + cc 3syl oveq2 eleq1d anbi12d rspcev syl12anc nnz adantl zdclt cdvds simpr + 1zzd adantr nnzd dvdsdc nndivdvds dcbid sylan ralrimiva nnwosdc infpnlem1 + dcand reximdva mpd ) DFGZHAUBZIJZCWMKLZFGZMZHBUBZIJZCWRKLZFGZMZWMWRUAJUCB + FNMZAFOZDWMIJWMWRKLFGWRHPWRWMPUDUCBFNMZAFOWLWQAFOZWQQZAFNXDWLCFGZHCIJZCCK + LZFGZXFWLCDUEUFZHUGLZFEWLXLWLDDUHUIZUJUKZWLHXMCIWLHXLUAJZHXMIJZWLXLXNULWL + HFGXLFGXPXQUMUOXNHXLUNUPUQEURWLXJHFWLXHCVGGZCUSUTJZMXJHPXOXHXRXSCVACVBVCC + VDVHUOVEWQXIXKMACFWMCPZWNXIWPXKWMCHIVFXTWOXJFWMCCKVIVJVKVLVMWLXGAFWLWMFGZ + MZWNWPYBHRGWMRGZWNQYBVSYAYCWLWMVNVOHWMVPSYBWMCVQJZQZWPQZYBYACRGYEWLYAVRYB + CWLXHYAXOVTWAWMCWBSWLXHYAYEYFUMXOXHYAMYDWPCWMWCWDWEUQWIWFWQXBABWMWRPZWNWS + WPXAWMWRHIVFYGWOWTFWMWRCKVIVJVKWGSWLXCXEAFBCWMDCXMCXMEECXMCXMEECXMCXMEECX + MCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXM + CXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMC + XMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCX + MEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXM + EECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXME + ECXMCXMEECXMCXMEECXMCXMEECXMCXMEECXMCXMEEETTTTTTTTTTTTTTTTTTTTTTTTTTTTTTT + TTTTTTTTTTTTTTTTTTTTTTTWHWJWK $. $} ${ @@ -139047,51 +139082,80 @@ given prime (or other positive integer) that divides the number. For ` R ` . (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 30-May-2014.) $) 1arith $p |- M : NN -1-1-onto-> R $= - ( vx vy vq cn cv cfv wceq wral wcel cprime cn0 wa wb vj vf wf1o wf1 wfo - vk vg wf weq wi wfn cpc co cmpt prmex mptex fnmpti cmap ccnv 1arithlem3 - cima cfn nn0ex elmap sylibr c1 cfz wss wdc 1zzd nnz fzfigd ffn elpreima - 3syl 1arithlem2 eleq1d cdvds wbr cle cz id dvdsle syl2anr pcelnn ancoms - prmz cuz prmnn nnuz eleqtrdi elfz5 3imtr4d sylbid expimpd elfznn adantl - ssrdv wn prmdc syl adantr ad2antrr simpr ffvelrnd nn0zd elnndc dcan2 wo - sylc intnanrd olcd df-dc exmiddc mpjaodan dcbid mpbird ralrimiva ssfidc - syl3anc cnveq imaeq1d elrab2 sylanbrc mpbir2an adantlr adantll ralbidva - rgen ffnfv eqeq12d eqfnfv syl2an nnnn0 sylib nnred cr ad2antrl syl2anc - wrex pc11 3bitr4d biimpd rgen2 dff13 cexp cif caddc eqid simplbi simplr - peano2nnd cc0 peano2re ltp1d simprr ltletrd nnzd zltnle mpbid biantrurd - clt simprl ad3antrrr bitr4d breq1 rspccv ad2antlr mtod elnn0 1arithlem4 - ord mpd cdm cnvimass fdmd prmssnn eqsstrdi sstrid simprbi r19.29a dffo3 - fiubnn df-f1o ) KADUCKADUDZKADUEZUWEKADUHZHLZDMZILZDMZNZHIUIZUJZIKOHKOU - WGDKUKUWIAPZHKOCKEQELCLULUMZUNDEQUWPUOUPFUQUWOHKUWHKPZUWIRQURUMZPZUWIUS - ZKVAZVBPZUWOUWQQRUWIUHZUWSCDUWHEFUTZRQUWIVCUOVDVEUWQVFUWHVGUMZVBPUXAUXE - VHUALZUXAPZVIZUAUXEOUXBUWQVFUWHUWQVJUWHVKZVLUWQJUXAUXEUWQJLZUXAPZUXJQPZ - UXJUWIMZKPZSZUXJUXEPZUWQUXCUWIQUKZUXKUXOTUXDQRUWIVMZQUXJKUWIVNVOUWQUXLU - XNUXPUWQUXLSZUXNUXJUWHULUMZKPZUXPUXSUXMUXTKUXJCDUWHEFVPZVQUXSUXJUWHVRVS - ZUXJUWHVTVSZUYAUXPUXLUXJWAPZUWQUYCUYDUJUWQUXJWGZUWQWBUXJUWHWCWDUXLUWQUY - AUYCTUXJUWHWEWFUXLUXJVFWHMZPUWHWAPUXPUYDTUWQUXLUXJKUYGUXJWIZWJWKUXIUXJV - FUWHWLWDWMWNWOWNWRUWQUXHUAUXEUWQUXFUXEPZSZUXHUXFQPZUXFUWIMZKPZSZVIZUYJU - YKUYOUYKWSZUYJUYKSZUYKVIZUYMVIZUYOUYJUYRUYKUYJUXFKPZUYRUYIUYTUWQUXFUWHW - PWQUXFWTXAZXBUYQUYLWAPUYSUYQUYLUYQQRUXFUWIUWQUXCUYIUYKUXDXCUYJUYKXDXEXF - UYLXGXAUYKUYMXHXJUYJUYPSZUYNUYNWSZXIUYOVUBVUCUYNVUBUYKUYMUYJUYPXDXKXLUY - NXMVEUYJUYRUYKUYPXIVUAUYKXNXAXOUWQUXHUYOTUYIUWQUXGUYNUWQUXCUXQUXGUYNTUX - DUXRQUXFKUWIVNVOXPXBXQXRUAUXEUXAXSXTBLZUSZKVAZVBPZUXBBUWIUWRAVUDUWINZVU - FUXAVBVUHVUEUWTKVUDUWIYAYBVQGYCYDYIHKADYJYEZUWNHIKKUWQUWJKPZSZUWLUWMVUK - UXMUXJUWKMZNZJQOZUXTUXJUWJULUMZNZJQOZUWLUWMVUKVUMVUPJQVUKUXLSUXMUXTVULV - UOUWQUXLUXMUXTNVUJUYBYFVUJUXLVULVUONUWQUXJCDUWJEFVPYGYKYHUWQUXCQRUWKUHZ - UWLVUNTZVUJUXDCDUWJEFUTUXCUXQUWKQUKVUSVURUXRQRUWKVMJQUWIUWKYLYMYMUWQUWH - RPUWJRPUWMVUQTVUJUWHYNUWJYNUWHUWJJUUAYMUUBUUCUUDHIKADUUEYEUWFUWGUBLZUWI - NHKYTZUBAOVUIVVAUBAVUTAPZUFLZUWJVTVSZUFVUTUSZKVAZOZVVAIKVVBVUJSZVVGSZHU - GCVUTUGKUGLZQPVVJVVJVUTMUUFUMVFUUGUNZDUWJVFUUHUMZJEFVVKUUIVVBQRVUTUHZVU - JVVGVVBVUTUWRPZVVMVVBVVNVVFVBPZVUGVVOBVUTUWRABUBUIZVUFVVFVBVVPVUEVVEKVU - DVUTYAYBVQGYCZUUJRQVUTVCUOVDYOZXCVVIUWJVVBVUJVVGUUKZUULVVIUXLVVLUXJVTVS - ZSZSZUXJVUTMZKPZWSVWCUUMNZVWBVWDUXJUWJVTVSZVWBUWJUXJUVBVSZVWFWSZVWBUWJV - VLUXJVWBUWJVVIVUJVWAVVSXBZYPZVWBUWJYQPVVLYQPVWJUWJUUNXAVWBUXJUXLUXJKPVV - IVVTUYHYRYPVWBUWJVWJUUOVVIUXLVVTUUPUUQVWBUWJWAPUYEVWGVWHTVWBUWJVWIUURUX - LUYEVVIVVTUYFYRUWJUXJUUSYSUUTVWBVWDUXJVVFPZVWFVWBVWDUXLVWDSZVWKVWBUXLVW - DVVIUXLVVTUVCZUVAVWBVVMVUTQUKVWKVWLTVVBVVMVUJVVGVWAVVRUVDZQRVUTVMQUXJKV - UTVNVOUVEVVGVWKVWFUJVVHVWAVVDVWFUFUXJVVFVVCUXJUWJVTUVFUVGUVHWNUVIVWBVWD - VWEVWBVWCRPVWDVWEXIVWBQRUXJVUTVWNVWMXEVWCUVJYOUVLUVMUVKVVBVVFKVHVVOVVGI - KYTVVBVVFVUTUVNZKVUTKUVOVVBVWOQKVVBQRVUTVVRUVPUVQUVRUVSVVBVVNVVOVVQUVTI - UFVVFUWCYSUWAYIHUBKADUWBYEKADUWDYE $. + ( vx vy vq cn cv cfv wceq wcel cprime cn0 wa wb 3eqtr2i vj vf vk vg wf1 + wf1o wfo wf weq wi wral wfn cpc co cmpt prmex fnmpti cmap ccnv cima cfn + mptex 1arithlem3 nn0ex elmap sylibr c1 cfz wss wdc 1zzd fzfigd elpreima + nnz ffn 3syl 1arithlem2 eleq1d cdvds wbr cle prmz dvdsle syl2anr pcelnn + cz id ancoms cuz prmnn nnuz eleqtrdi elfz5 3imtr4d sylbid expimpd ssrdv + wn elfznn adantl prmdc syl ad2antrr simpr ffvelrnd elnndc dcan syl2an2r + nn0zd wo intnanrd df-dc exmiddc mpjaodan adantr mpbird ralrimiva ssfidc + olcd dcbid syl3anc cnveq imaeq1d elrab2 sylanbrc ffnfv mpbir2an adantlr + rgen adantll eqeq12d ralbidva syl2an nnnn0 wrex sylib nnred cr ad2antrl + syl2anc eqfnfv pc11 3bitr4d biimpd rgen2 dff13 cif caddc simplbi simplr + cexp eqid peano2nnd cc0 clt simpllr peano2re simprr ltletrd nnzd zltnle + ltp1d mpbid simprl biantrurd ad3antrrr bitr4d breq1 ad2antlr mtod elnn0 + rspccv ord mpd 1arithlem4 cnvimass fdmd prmssnn eqsstrdi sstrid simprbi + cdm crab fiubnn r19.29a dffo3 df-f1o ) KADUFKADUEZKADUGZUWHKADUHZHLZDMZ + ILZDMZNZHIUIZUJZIKUKHKUKUWJDKULUWLAOZHKUKCKEPELCLUMUNZUODEPUWSUPVBFUQUW + RHKUWKKOZUWLQPURUNZOZUWLUSZKUTZVAOZUWRUWTPQUWLUHZUXBCDUWKEFVCZQPUWLVDUP + VEVFUWTVGUWKVHUNZVAOUXDUXHVIUALZUXDOZVJZUAUXHUKUXEUWTVGUWKUWTVKUWKVNZVL + UWTJUXDUXHUWTJLZUXDOZUXMPOZUXMUWLMZKOZRZUXMUXHOZUWTUXFUWLPULZUXNUXRSUXG + PQUWLVOZPUXMKUWLVMVPUWTUXOUXQUXSUWTUXORZUXQUXMUWKUMUNZKOZUXSUYBUXPUYCKU + XMCDUWKEFVQZVRUYBUXMUWKVSVTZUXMUWKWAVTZUYDUXSUXOUXMWFOZUWTUYFUYGUJUWTUX + MWBZUWTWGUXMUWKWCWDUXOUWTUYDUYFSUXMUWKWEWHUXOUXMVGWIMZOUWKWFOUXSUYGSUWT + UXOUXMKUYJUXMWJZWKWLUXLUXMVGUWKWMWDWNWOWPWOWQUWTUXKUAUXHUWTUXIUXHOZRZUX + KUXIPOZUXIUWLMZKOZRZVJZUYMUYNUYRUYNWRZUYMUYNVJZUYNUYPVJZUYRUYMUXIKOZUYT + UYLVUBUWTUXIUWKWSWTZUXIXAZXBUYMUYNRZUYOWFOVUAVUEUYOVUEPQUXIUWLUWTUXFUYL + UYNUXGXCUYMUYNXDXEXIUYOXFXBUYNUYPXGXHUYMUYSRZUYQUYQWRZXJUYRVUFVUGUYQVUF + UYNUYPUYMUYSXDXKXSUYQXLVFUYMVUBUYTUYNUYSXJVUCVUDUYNXMVPXNUWTUXKUYRSUYLU + WTUXJUYQUWTUXFUXTUXJUYQSUXGUYAPUXIKUWLVMVPXTXOXPXQUAUXHUXDXRYABLZUSZKUT + ZVAOZUXEBUWLUXAAVUHUWLNZVUJUXDVAVULVUIUXCKVUHUWLYBYCVRGYDYEYIHKADYFYGZU + WQHIKKUWTUWMKOZRZUWOUWPVUOUXPUXMUWNMZNZJPUKZUYCUXMUWMUMUNZNZJPUKZUWOUWP + VUOVUQVUTJPVUOUXORUXPUYCVUPVUSUWTUXOUXPUYCNVUNUYEYHVUNUXOVUPVUSNUWTUXMC + DUWMEFVQYJYKYLUWTUXFPQUWNUHZUWOVURSZVUNUXGCDUWMEFVCUXFUXTUWNPULVVCVVBUY + APQUWNVOJPUWLUWNUUAYMYMUWTUWKQOUWMQOUWPVVASVUNUWKYNUWMYNUWKUWMJUUBYMUUC + UUDUUEHIKADUUFYGUWIUWJUBLZUWLNHKYOZUBAUKVUMVVEUBAVVDAOZUCLZUWMWAVTZUCVV + DUSZKUTZUKZVVEIKVVFVUNRZVVKRZHUDCVVDUDKUDLZPOVVNVVNVVDMUUKUNVGUUGUOZDUW + MVGUUHUNZJEFVVOUULVVFPQVVDUHZVUNVVKVVFVVDUXAOZVVQVVFVVRVVJVAOZVUKVVSBVV + DUXAABUBUIZVUJVVJVAVVTVUIVVIKVUHVVDYBYCVRZGYDUUIQPVVDVDUPVEYPZXCVVMUWMV + VFVUNVVKUUJUUMVVMUXOVVPUXMWAVTZRZRZUXMVVDMZKOZWRVWFUUNNZVWEVWGUXMUWMWAV + TZVWEUWMUXMUUOVTZVWIWRZVWEUWMVVPUXMVWEUWMVVFVUNVVKVWDUUPZYQZVWEUWMYROVV + PYROVWMUWMUUQXBVWEUXMUXOUXMKOVVMVWCUYKYSYQVWEUWMVWMUVBVVMUXOVWCUURUUSVW + EUWMWFOUYHVWJVWKSVWEUWMVWLUUTUXOUYHVVMVWCUYIYSUWMUXMUVAYTUVCVWEVWGUXMVV + JOZVWIVWEVWGUXOVWGRZVWNVWEUXOVWGVVMUXOVWCUVDZUVEVWEVVQVVDPULVWNVWOSVVFV + VQVUNVVKVWDVWBUVFZPQVVDVOPUXMKVVDVMVPUVGVVKVWNVWIUJVVLVWDVVHVWIUCUXMVVJ + VVGUXMUWMWAUVHUVLUVIWOUVJVWEVWGVWHVWEVWFQOVWGVWHXJVWEPQUXMVVDVWQVWPXEVW + FUVKYPUVMUVNUVOVVFVVJKVIVVSVVKIKYOVVFVVJVVDUWBZKVVDKUVPVVFVWRPKVVFPQVVD + VWBUVQUVRUVSUVTVVFVVRVVSVUKVVSBVVDUXAAVWAAVUKBUXAUWCZAVWSGGAVWSAVWSGGAV + WSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVW + SAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWS + AVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSA + VWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAV + WSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVW + SGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWS + GGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSG + GAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGG + AVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGA + VWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAV + WSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVW + SAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWS + AVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSA + VWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAV + WSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVW + SGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWS + GGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSG + GAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGG + AVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGA + VWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAV + WSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVW + SAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWS + AVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSA + VWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAV + WSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVWSGGAVWSAVW + SGGAVWSAVWSGGGTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTT + TTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTT + TTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTYDUWAIUCVVJUWDYTUW + EYIHUBKADUWFYGKADUWGYG $. $} $( Fundamental theorem of arithmetic, where a prime factorization is @@ -140624,21 +140688,27 @@ then the Limited Principle of Omniscience (LPO) implies excluded middle. ctiunctlemudc $p |- ( ph -> A. n e. _om DECID n e. U ) $= ( vm cv wcel wdc com wral wa cfv c1st c2nd csb wn wceq eleq1 adantr cxp dcbid wf1o f1of syl simpr ffvelrnd xp1st rspcdva wfo ad2antrr ralrimiva - wf fof nfcv nfcsb1v nfcri nfdc nfralya csbeq1a eleq2d ralbidv rspc sylc - xp2nd dcan2 wo intnanrd olcd df-dc sylibr mpjaodan 2fveq3 eleq1d fveq2d - exmiddc csbeq1d eleq12d anbi12d elrab2 wb adantl bitr4id mpbird cbvralv - ibar sylib ) AUAUBZHUCZUDZUAUEUFIUBZHUCZUDZIUEUFAXEUAUEAXCUEUCZUGZXEXCL - UHZUIUHZFUCZXKUJUHZBXLJUHZGUKZUCZUGZUDZXJXMXSXMULZXJXMUGZXMUDZXQUDZXSXJ - YBXMXJXFFUCZUDZYBIUEXLXFXLUMYDXMXFXLFUNUQAYEIUEUFXINUOXJXKUEUEUPZUCZXLU - EUCXJUEYFXCLXJUEYFLURZUEYFLVHAYHXISUOUEYFLUSUTAXIVAVBZXKUEUEVCUTVDZUOYA - XFXPUCZUDZYCIUEXNXFXNUMYKXQXFXNXPUNUQYAXODUCXFGUCZUDZIUEUFZBDUFZYLIUEUF - ZYAFDXLJAFDJVHZXIXMAFDJVEYROFDJVIUTVFXJXMVAVBAYPXIXMAYOBDQVGVFYOYQBXODY - LBIUEBUEVJYKBBIXPBXOGVKVLVMVNBUBXOUMZYNYLIUEYSYMYKYSGXPXFBXOGVOVPUQVQVR - VSYAYGXNUEUCXJYGXMYIUOXKUEUEVTUTVDXMXQWAVSXJXTUGZXRXRULZWBXSYTUUAXRYTXM - XQXJXTVAWCWDXRWEWFXJYBXMXTWBYJXMWKUTWGXJXDXRXJXDXIXRUGZXRCUBZLUHZUIUHZF - UCZUUDUJUHZBUUEJUHZGUKZUCZUGXRCXCUEHUUCXCUMZUUFXMUUJXQUUKUUEXLFUUCXCUIL - WHZWIUUKUUGXNUUIXPUUCXCUJLWHUUKBUUHXOGUUKUUEXLJUULWJWLWMWNTWOXIXRUUBWPA - XIXRXAWQWRUQWSVGXEXHUAIUEXCXFUMXDXGXCXFHUNUQWTXB $. + wf fof nfcv nfcsb1v nfel2 nfdc nfralya csbeq1a eleq2d ralbidv rspc sylc + xp2nd dcan syl2an2r wo intnanrd olcd df-dc sylibr exmiddc 2fveq3 eleq1d + mpjaodan fveq2d csbeq1d eleq12d anbi12d crab 3eqtr2i elrab2 ibar adantl + wb bitr4id mpbird cbvralvw sylib ) AUAUBZHUCZUDZUAUEUFIUBZHUCZUDZIUEUFA + XHUAUEAXFUEUCZUGZXHXFLUHZUIUHZFUCZXNUJUHZBXOJUHZGUKZUCZUGZUDZXMXPYBXPUL + ZXMXPUDZXPXTUDZYBXMXIFUCZUDZYDIUEXOXIXOUMYFXPXIXOFUNUQAYGIUEUFXLNUOXMXN + UEUEUPZUCZXOUEUCXMUEYHXFLXMUEYHLURZUEYHLVHAYJXLSUOUEYHLUSUTAXLVAVBZXNUE + UEVCUTVDZXMXPUGZXIXSUCZUDZYEIUEXQXIXQUMYNXTXIXQXSUNUQYMXRDUCXIGUCZUDZIU + EUFZBDUFZYOIUEUFZYMFDXOJAFDJVHZXLXPAFDJVEUUAOFDJVIUTVFXMXPVAVBAYSXLXPAY + RBDQVGVFYRYTBXRDYOBIUEBUEVJYNBBXIXSBXRGVKVLVMVNBUBXRUMZYQYOIUEUUBYPYNUU + BGXSXIBXRGVOVPUQVQVRVSYMYIXQUEUCXMYIXPYKUOXNUEUEVTUTVDXPXTWAWBXMYCUGZYA + YAULZWCYBUUCUUDYAUUCXPXTXMYCVAWDWEYAWFWGXMYDXPYCWCYLXPWHUTWKXMXGYAXMXGX + LYAUGZYACUBZLUHZUIUHZFUCZUUGUJUHZBUUHJUHZGUKZUCZUGZYACXFUEHUUFXFUMZUUIX + PUUMXTUUOUUHXOFUUFXFUILWIZWJUUOUUJXQUULXSUUFXFUJLWIUUOBUUKXRGUUOUUHXOJU + UPWLWMWNWOHUUNCUEWPZHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQH + UUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHU + UQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUU + QTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQ + TTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTHUUQHUUQTTTWQWQWQWQWQWQWQWQWQWQWQWQWQWQ + WQWQWQWQWQWQWQWQWQWQWQWQWQWQWQWQWQWRXLYAUUEXAAXLYAWSWTXBUQXCVGXHXKUAIUE + XFXIUMXGXJXFXIHUNUQXDXE $. $} ctiunct.h $e |- H = ( n e. U |-> ( [_ ( F ` ( 1st ` ( J ` n ) ) ) / x ]_ G @@ -140894,23 +140964,23 @@ then the Limited Principle of Omniscience (LPO) implies excluded middle. $( Lemma for ~ nninfdc . (Contributed by Jim Kingdon, 25-Sep-2024.) $) nninfdclemcl $p |- ( ph -> ( P ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) Q ) e. A ) $= - ( vs cn cv clt wcel wceq vr vt c1 caddc co cuz cfv cin cinf cmpo sseldd - cr wss wdc wral wex inss1 sstrid eleq1w dcbid adantr simpr rspcdva nnzd - wa cz peano2zd eluzdc syl2anc dcan2 sylc dcbii sylibr ralrimiva cbvralv - elin sylib wbr wrex breq1 rexbidv cbvrexv simprl cle simprr wb nnltp1le - breq2 mpbid eluz2 syl3anbrc elind syl rexlimddv nnmindc syl3anc fvoveq1 - elex2 elin1d ineq2d infeq1d eqidd eqid ovmpog eqeltrd ) AFGCDPPECQZUCUD - UEUFUGZUHZULRUIZUJZUEZEFUCUDUEZUFUGZUHZULRUIZEAFPSZGPSXOESXKXOTAEPFJMUK - ZAEPGJNUKAEXMXOAXNPUMBQZXNSZUNZBPUOZUAQXNSUAUPZXOXNSAXNEPEXMUQJURAOQZXN - SZUNZOPUOYAAYEOPAYCPSZVEZYCESZYCXMSZVEZUNZYEYGYHUNZYIUNZYKYGXRESZUNZYLB - PYCXRYCTYNYHBOEUSUTAYOBPUOYFKVAAYFVBZVCYGXLVFSZYCVFSYMYGFYGFAXPYFXQVAVD - VGYGYCYPVDXLYCVHVIYHYIVJVKYDYJYCEXMVPVLVMVNYEXTOBPYCXRTYDXSOBXNUSUTVOVQ - AFUBQZRVRZYBUBEAFIQZRVRZIEVSZYSUBEVSAHQZYTRVRZIEVSUUBHPFUUCFTUUDUUAIEUU - CFYTRVTWALXQVCUUAYSIUBEYTYRFRWHWBVQAYRESZYSVEZVEZYRXNSYBUUGEXMYRAUUEYSW - CZUUGYQYRVFSXLYRWDVRZYRXMSAYQUUFAFAFXQVDVGVAUUGYRUUGEPYRAEPUMUUFJVAUUHU - KZVDUUGYSUUIAUUEYSWEUUGXPYRPSYSUUIWFAXPUUFXQVAUUJFYRWGVIWIXLYRWJWKWLUAY - RXNWRWMWNBUAXNWOWPWSZCDFGPPXIXOXJXOEXFFTZULXHXNRUULXGXMEXFFUCUFUDWQWTXA - DQGTXOXBXJXCXDWPUUKXE $. + ( cn cv clt wcel wceq wdc vr vs vt c1 caddc co cuz cfv cin cr cinf cmpo + sseldd wss wral wex inss1 sstrid wa eleq1 dcbid adantr simpr rspcdva cz + nnzd peano2zd eluzdc syl2anc dcand elin dcbii sylibr ralrimiva cbvralvw + sylib wrex breq1 rexbidv breq2 cbvrexvw simprl simprr nnltp1le syl2an2r + wbr cle mpbid eluz2 syl3anbrc elind elex2 syl rexlimddv nnmindc syl3anc + wb elin1d fvoveq1 ineq2d infeq1d eqidd eqid ovmpog eqeltrd ) AFGCDOOECP + ZUDUEUFUGUHZUIZUJQUKZULZUFZEFUDUEUFZUGUHZUIZUJQUKZEAFORZGORXOERXKXOSAEO + FJMUMZAEOGJNUMAEXMXOAXNOUNBPZXNRZTZBOUOZUAPXNRUAUPZXOXNRAXNEOEXMUQJURAU + BPZXNRZTZUBOUOYAAYEUBOAYCORZUSZYCERZYCXMRZUSZTYEYGYHYIYGXRERZTZYHTBOYCX + RYCSYKYHXRYCEUTVAAYLBOUOYFKVBAYFVCZVDYGXLVERZYCVERYITYGFYGFAXPYFXQVBVFV + GYGYCYMVFXLYCVHVIVJYDYJYCEXMVKVLVMVNYEXTUBBOYCXRSYDXSYCXRXNUTVAVOVPAFUC + PZQWFZYBUCEAFIPZQWFZIEVQZYPUCEVQAHPZYQQWFZIEVQYSHOFYTFSUUAYRIEYTFYQQVRV + SLXQVDYRYPIUCEYQYOFQVTWAVPAYOERZYPUSZUSZYOXNRYBUUDEXMYOAUUBYPWBZUUDYNYO + VERXLYOWGWFZYOXMRAYNUUCAFAFXQVFVGVBUUDYOUUDEOYOAEOUNUUCJVBUUEUMZVFUUDYP + UUFAUUBYPWCAXPUUCYOORYPUUFWQXQUUGFYOWDWEWHXLYOWIWJWKUAYOXNWLWMWNBUAXNWO + WPWRZCDFGOOXIXOXJXOEXFFSZUJXHXNQUUIXGXMEXFFUDUGUEWSWTXADPGSXOXBXJXCXDWP + UUHXE $. $} nninfdclemf.j $e |- ( ph -> ( J e. A /\ 1 < J ) ) $. @@ -140943,40 +141013,54 @@ then the Limited Principle of Omniscience (LPO) implies excluded middle. than the previous element. (Contributed by Jim Kingdon, 26-Sep-2024.) $) nninfdclemp1 $p |- ( ph -> ( F ` U ) < ( F ` ( U + 1 ) ) ) $= - ( cn cv wcel vr va vb vp vq vs cfv c1 caddc nninfdclemf ffvelrnd sseldd - co nnred nnzd peano2zd zred peano2nnd ltp1d cuz cin cr clt cinf cle wbr - wral wa simpr elin2d eluzle syl ralrimiva inss1 sstrid wdc eleq1w dcbid - weq adantr rspcdva cz eluzdc syl2an2r dcan2 sylc elin dcbii sylibr wrex - wex breq1 rexbidv breq2 cbvrexv sylib df-rex simprl wss simprr nnltp1le - wceq wb mpbid eluz2 syl3anbrc elind ex eximdv mpd nninfdcex infregelbex - nnssre sstrdi mpbird cmpo cmpt cseq fveq1i nnuz eleqtrdi elnnuz biimpri - eqid eqidd adantl simpld fvmptd3 eqeltrd nninfdclemcl seq3p1 syl5eq a1i - eqcomi oveq12d cbvralv nnmindc syl3anc elin1d fvoveq1 infeq1d breqtrrd - ineq2d ovmpog 3eqtrd ltletrd ) AFJUGZUUGUHUIUMZFUHUIUMZJUGZAUUGAERUUGLA - REFJABCDEGHIJKLMNOPUJZQUKULZUNZAUUHAUUGAUUGUULUOUPZUQZAUUJAERUUJLAREUUI - JUUKAFQURZUKULUNAUUGUUMUSAUUHEUUHUTUGZVAZVBVCVDZUUJVEAUUHUUSVEVFUUHUASZ - VEVFZUAUURVGAUVAUAUURAUUTUURTZVHZUUTUUQTUVAUVCEUUQUUTAUVBVIVJUUHUUTVKVL - VMAUBUCUAUURUUHAUBUCUAUURAUUREREUUQVNLVOZAUBSZUURTZVPZUBRAUVERTZVHZUVEE - TZUVEUUQTZVHZVPZUVGUVIUVJVPZUVKVPZUVMUVIBSZETZVPZUVNBRUVEBUBVSUVQUVJBUB - EVQVRAUVRBRVGZUVHMVTAUVHVIZWAAUUHWBTZUVHUVEWBTUVOUUNUVIUVEUVTUOUUHUVEWC - WDUVJUVKWEWFUVFUVLUVEEUUQWGWHWIVMAUCSZETZUUGUWBVCVFZVHZUCWKZUWBUURTZUCW - KZAUWDUCEWJZUWFAUUGISZVCVFZIEWJZUWIAHSZUWJVCVFZIEWJZUWLHRUUGUWMUUGXBUWN - UWKIEUWMUUGUWJVCWLWMNUULWAUWKUWDIUCEUWJUWBUUGVCWNWOWPUWDUCEWQWPAUWEUWGU - CAUWEUWGAUWEVHZEUUQUWBAUWCUWDWRZUWPUWAUWBWBTUUHUWBVEVFZUWBUUQTAUWAUWEUU - NVTUWPUWBUWPERUWBAERWSZUWELVTUWQULZUOUWPUWDUWRAUWCUWDWTAUUGRTZUWEUWBRTU - WDUWRXCUULUWTUUGUWBXAWDXDUUHUWBXEXFXGXHXIXJZXKAUURRVBUVDXMXNUUOXLXOAUUJ - FCDRRECSZUHUIUMUTUGZVAZVBVCVDZXPZGRKXQZUHXRZUGZUUIUXHUGZUXGUMZUUGKUXGUM - ZUUSAUUJUUIUXIUGUXLUUIJUXIPXSAUDUEUXGEUXHUHFAFRUHUTUGZQXTYAAUDSZUXNTZVH - ZUXOUXHUGKEUXQGUXOKKRUXHEUXHYDZGUDVSKYEUXPUXORTZAUXSUXPUXOYBYCYFAKETZUX - PAUXTUHKVCVFOYGZVTZYHUYBYIAUXOETZUESZETZVHZVHBCDEUXOUYDHIAUWSUYFLVTAUVS - UYFMVTAUWOHRVGUYFNVTAUYCUYEWRAUYCUYEWTYJYKYLAUXJUUGUXKKUXGUXJUUGXBAUUGU - XJFJUXIPXSYNYMAGUUIKKRUXHEUXRGSUUIXBKYEUUPUYAYHYOAUXAKRTUUSETUXMUUSXBUU - LAERKLUYAULAEUUQUUSAUURRWSUVPUURTZVPZBRVGZUWHUUSUURTUVDAUFSZUURTZVPZUFR - VGUYIAUYLUFRAUYJRTZVHZUYJETZUYJUUQTZVHZVPZUYLUYNUYOVPZUYPVPZUYRUYNUVRUY - SBRUYJBUFVSUVQUYOBUFEVQVRAUVSUYMMVTAUYMVIZWAAUWAUYMUYJWBTUYTUUNUYNUYJVU - AUOUUHUYJWCWDUYOUYPWEWFUYKUYQUYJEUUQWGWHWIVMUYLUYHUFBRUFBVSUYKUYGUFBUUR - VQVRYPWPUXBBUCUURYQYRYSCDUUGKRRUXFUUSUXGUUSEUXCUUGXBZVBUXEUURVCVUBUXDUU - QEUXCUUGUHUTUIYTUUCUUADSKXBUUSYEUXGYDUUDYRUUEUUBUUF $. + ( cn wcel 3eqtr2i vr va vb vp vq vs c1 caddc nninfdclemf ffvelrnd nnred + cfv co sseldd nnzd peano2zd zred peano2nnd ltp1d cuz cin cr clt cle wbr + cinf cv wa simpr elin2d eluzle syl ralrimiva inss1 sstrid wdc weq eleq1 + wral dcbid adantr rspcdva cz eluzdc syl2an2r dcand elin sylibr wex wrex + dcbii wceq breq1 breq2 cbvrexvw sylib df-rex simprl wss simprr nnltp1le + rexbidv wb mpbid eluz2 syl3anbrc elind eximdv mpd nninfdcex infregelbex + ex nnssre sstrdi mpbird cmpo cmpt cseq fveq1i nnuz eleqtrdi eqid elnnuz + eqidd biimpri adantl simpld fvmptd3 nninfdclemcl seq3p1 syl5eq 3eqtr2ri + eqeltrd a1i oveq12d cbvralvw nnmindc syl3anc elin1d fvoveq1 breqtrrd + ineq2d infeq1d ovmpog 3eqtrd ltletrd ) AFJULZUUGUGUHUMZFUGUHUMZJULZAUUG + AERUUGLAREFJABCDEGHIJKLMNOPUIZQUJUNZUKZAUUHAUUGAUUGUULUOUPZUQZAUUJAERUU + JLAREUUIJUUKAFQURZUJUNUKAUUGUUMUSAUUHEUUHUTULZVAZVBVCVFZUUJVDAUUHUUSVDV + EUUHUAVGZVDVEZUAUURVSAUVAUAUURAUUTUURSZVHZUUTUUQSUVAUVCEUUQUUTAUVBVIVJU + UHUUTVKVLVMAUBUCUAUURUUHAUBUCUAUURAUUREREUUQVNLVOZAUBVGZUURSZVPZUBRAUVE + RSZVHZUVEESZUVEUUQSZVHZVPUVGUVIUVJUVKUVIBVGZESZVPZUVJVPBRUVEBUBVQUVNUVJ + UVMUVEEVRVTAUVOBRVSZUVHMWAAUVHVIZWBAUUHWCSZUVHUVEWCSUVKVPUUNUVIUVEUVQUO + UUHUVEWDWEWFUVFUVLUVEEUUQWGWKWHVMAUCVGZESZUUGUVSVCVEZVHZUCWIZUVSUURSZUC + WIZAUWAUCEWJZUWCAUUGIVGZVCVEZIEWJZUWFAHVGZUWGVCVEZIEWJZUWIHRUUGUWJUUGWL + UWKUWHIEUWJUUGUWGVCWMXBNUULWBUWHUWAIUCEUWGUVSUUGVCWNWOWPUWAUCEWQWPZAUWB + UWDUCAUWBUWDAUWBVHZEUUQUVSAUVTUWAWRZUWNUVRUVSWCSZUUHUVSVDVEZUVSUUQSZAUV + RUWBUUNWAZUWNUVSUWNERUVSAERWSZUWBLWAUWOUNZUOZUWNUWAUWQAUVTUWAWTZAUUGRSZ + UWBUVSRSZUWAUWQXCZUULUXAUUGUVSXAZWEXDUUHUVSXEZXFXGXLXHXIXJAUURRVBUVDXMX + NUUOXKXOAUUJFCDRRECVGZUGUHUMUTULZVAZVBVCVFZXPZGRKXQZUGXRZULZUUIUXNULZUX + MUMZUUGKUXMUMZUUSAUUJUUIUXOULUXRUUIJUXOPXSAUDUEUXMEUXNUGFAFRUGUTULZQXTY + AAUDVGZUXTSZVHZUYAUXNULKEUYCGUYAKKRUXNEUXNYBZGUDVQKYDUYBUYARSZAUYEUYBUY + AYCYEYFAKESZUYBAUYFUGKVCVEOYGZWAZYHUYHYMAUYAESZUEVGZESZVHZVHBCDEUYAUYJH + IAUWTUYLLWAAUVPUYLMWAAUWLHRVSUYLNWAAUYIUYKWRAUYIUYKWTYIYJYKAUXPUUGUXQKU + XMUXPUUGWLAUUGUXPUUGUXPFJUXOPXSZUYMUYMYLYNAGUUIKKRUXNEUYDGVGUUIWLKYDUUP + UYGYHYOAUXDKRSUUSESUXSUUSWLUULAERKLUYGUNAEUUQUUSAUURRWSUVMUURSZVPZBRVSZ + UWEUUSUURSUVDAUFVGZUURSZVPZUFRVSUYPAUYSUFRAUYQRSZVHZUYQESZUYQUUQSZVHZVP + UYSVUAVUBVUCVUAUVOVUBVPBRUYQBUFVQUVNVUBUVMUYQEVRVTAUVPUYTMWAAUYTVIZWBAU + VRUYTUYQWCSVUCVPUUNVUAUYQVUEUOUUHUYQWDWEWFUYRVUDUYQEUUQWGWKWHVMUYSUYOUF + BRUFBVQUYRUYNUYQUVMUURVRVTYPWPAUWCUWEUWMAUWBUWDUCAUWBUWDUWNEUUQUVSUWOUW + NUVRUWPUWQUWRUWSUXBUWNUWAUWQUXCAUXDUWBUXEUXFAERUUGLAREFJABCDEGHIJKLMNOJ + UXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJU + XOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUX + OJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXO + JUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJ + UXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJU + XOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUX + OPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXO + PPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOP + PJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPP + JUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPJUXOJUXOPPP + TTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTT + UIQUJUNUXAUXGWEXDUXHXFXGXLXHXIBUCUURYQYRYSCDUUGKRRUXLUUSUXMUUSEUXIUUGWL + ZVBUXKUURVCVUFUXJUUQEUXIUUGUGUTUHYTUUBUUCDVGKWLUUSYDUXMYBUUDYRUUEUUAUUF + $. $} ${ @@ -156845,48 +156929,56 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is lgsval $p |- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) = if ( N = 0 , if ( ( A ^ 2 ) = 1 , 1 , 0 ) , ( if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , F ) ` ( abs ` N ) ) ) ) ) $= - ( cz wcel cc0 wceq c2 cexp co c1 cif wa cmul wdc cn cmo oveq1d vk clt wbr - vv va vm cneg cabs cfv cseq clgs 0zd zsqcl ad2antrr zdceq syl2anc ifcldcd - 1zzd wn neg1z a1i simpr zdclt syl2an2r simpl dcan2 sylc nnuz cprime cdvds - cv c8 c7 cpr cmin caddc cpc eleq1w eqeq1 oveq1 oveq2d id oveq12d ifbieq2d - cdiv ifbieq1d cn0 znegcld wo 8nn zmodcld nn0zd nnzi sylancl dcor wb elprg - 7nn syl dcbid mpbird ad5antr 2nn simp-5l dvdsdc prm2orodd orcomd ad2antlr - ecased prmnn nnnn0d nn0oddm1d2 mpbid zexpcl peano2zd zsubcld nnz ifcldadc - 2z wne simp-4r neqne ad3antlr pczcl syl12anc prmdc adantl fvmptd3 eqeltrd - zmulcl seqf simplr nnabscl ffvelrnd zmulcld eqeq1d ifbid breq1d anbi12d - cmpt breq2d eleq1d ifeq12d ifeq1d mpteq2dv eqtr4di seqeq3d fveq2d fveq12d - ifbieq12d df-lgs ovmpoga mpd3an3 ) AFGZDFGZDHIZAJKLZMIZMHNZDHUBUCZAHUBUCZ - OZMUGZMNZDUHUIZPCMUJZUIZPLZNZFGADUKLUVIIUUNUUOOZUUPUUSUVHFUVJUUPOZUURMHFU - VKURZUVKULUVKUUQFGZMFGZUURQUUNUVMUUOUUPAUMUNUVLUUQMUOUPUQUVJUUPUSZOZUVDUV - GUVPUVBUVCMFUVCFGUVPUTVAUVPURZUVPUUTQZUVAQZUVBQUVJUUOUVOHFGZUVRUUNUUOVBZU - VPULZDHVCVDUVJUUNUVOUVTUVSUUNUUOVEUWBAHVCVDUUTUVAVFVGUQUVPRFUVEUVFUVPUAUD - PFCMRVHUVQUVPUAVKZRGZOZUWCCUIUWCVIGZUWCJIZJAVJUCZHAVLSLZMVMVNZGZMUVCNZNZA - UWCMVOLZJWELZKLZMVPLZUWCSLZMVOLZNZUWCDVQLZKLZMNZFUWEBUWCBVKZVIGZUXDJIZUWM - AUXDMVOLZJWELZKLZMVPLZUXDSLZMVOLZNZUXDDVQLZKLZMNZUXCRCFEUXDUWCIZUXEUWFUXO - UXBMBUAVIVRUXQUXMUWTUXNUXAKUXQUXFUWGUXLUWSUWMUXDUWCJVSUXQUXKUWRMVOUXQUXJU - WQUXDUWCSUXQUXIUWPMVPUXQUXHUWOAKUXQUXGUWNJWEUXDUWCMVOVTTWATUXQWBWCTWDUXDU - WCDVQVTWCWFUVPUWDVBZUWEUWFUXBMFUWEUWFOZUWTFGUXAWGGZUXBFGUXSUWGUWMUWSFUXSU - WGOZUWHHUWLFUYAULUYAUWKMUVCFUYAURZUYAMUYBWHUUNUWKQZUUOUVOUWDUWFUWGUUNUYCU - WIMIZUWIVMIZWIZQZUUNUYDQZUYEQZUYGUUNUWIFGZUVNUYHUUNUWIUUNAVLUUNWBVLRGUUNW - JVAWKZWLZUUNURUWIMUOUPUUNUYJVMFGUYIUYLVMWRWMUWIVMUOWNUYDUYEWOVGUUNUWKUYFU - UNUWIWGGUWKUYFWPUYKUWIMVMWGWQWSWTXAXBUQUYAJRGZUUNUWHQUYMUYAXCVAUUNUUOUVOU - WDUWFUWGXDJAXEUPUQUXSUWGUSZOZUWRMUYOUWRUYOUWQUWCUYOUWPUYOUUNUWOWGGZUWPFGU - UNUUOUVOUWDUWFUYNXDUYOJUWCVJUCUSZUYPUYOUYQUWGUXSUYNVBUWFUYQUWGWIUWEUYNUWF - UWGUYQUWCXFXGXHXIUWFUYQUYPWPZUWEUYNUWFUWCWGGUYRUWFUWCUWCXJXKUWCXLWSXHXMAU - WOXNUPXOUWEUWDUWFUYNUXRUNWKWLUYOURXPUXSUWCFGZJFGUWGQUWDUYSUVPUWFUWCXQXHXS - UWCJUOWNXRUXSUWFUUODHXTZUXTUWEUWFVBUUNUUOUVOUWDUWFYAUVOUYTUVJUWDUWFDHYBZY - CUWCDYDYEUWTUXAXNUPUWEUWFUSOURUWDUWFQUVPUWCYFYGXRZYHVUBYIUYSUDVKZFGOUWCVU - CPLFGUVPUWCVUCYJYGYKUVPUUOUYTUVERGUUNUUOUVOYLUVOUYTUVJVUAYGDYMUPYNYOUVJUU - OUVTUUPQUWAUVJULDHUOUPXRUEUFADFFUFVKZHIZUEVKZJKLZMIZMHNZVUDHUBUCZVUFHUBUC - ZOZUVCMNZVUDUHUIZPBRUXEUXFJVUFVJUCZHVUFVLSLZUWJGZMUVCNZNZVUFUXHKLZMVPLZUX - DSLZMVOLZNZUXDVUDVQLZKLZMNZYTZMUJZUIZPLZNUVIUKFVUFAIZVUDDIZOZVUEUUPVUIVVK - UUSUVHVVNVUDDHVVLVVMVBZYPVVNVUHUURMHVVNVUGUUQMVVNVUFAJKVVLVVMVEZTYPYQVVNV - UMUVDVVJUVGPVVNVULUVBUVCMVVNVUJUUTVUKUVAVVNVUDDHUBVVOYRVVNVUFAHUBVVPYRYSY - QVVNVUNUVEVVIUVFVVNVVHCPMVVNVVHBRUXPYTCVVNBRVVGUXPVVNUXEVVFUXOMVVNVVDUXMV - VEUXNKVVNUXFVUSUWMVVCUXLVVNVUOUWHVURUWLHVVNVUFAJVJVVPUUAVVNVUQUWKMUVCVVNV - UPUWIUWJVVNVUFAVLSVVPTUUBYQWDVVNVVBUXKMVOVVNVVAUXJUXDSVVNVUTUXIMVPVVNVUFA - UXHKVVPTTTTUUCVVNVUDDUXDVQVVOWAWCUUDUUEEUUFUUGVVNVUDDUHVVOUUHUUIWCUUJBUFU - EUUKUULUUM $. + ( cz wcel cc0 wceq c2 cexp co c1 cif wa cmul wdc cn oveq1d 3eqtr2i vk clt + vv va wbr cneg cabs cfv cseq clgs 1zzd 0zd zsqcl ad2antrr syl2anc ifcldcd + vm zdceq wn neg1z a1i simpr zdclt syl2an2r simpl dcand cv cprime cdvds c8 + nnuz cmo c7 cpr cmin cdiv caddc eleq1 eqeq1 oveq1 oveq2d oveq12d ifbieq2d + cpc id ifbieq1d cn0 znegcld wo 8nn zmodcld nn0zd 7nn nnzi sylancl dcor wb + sylc elprg 3syl dcbid mpbird ad5antr 2nn simp-5l dvdsdc sylancr prm2orodd + orcomd ad2antlr ecased prmnn nnnn0d nn0oddm1d2 syl mpbid peano2zd simpllr + zexpcl zsubcld nnz 2z ifcldadc wne simp-4r neqne ad3antlr syl12anc adantl + pczcl prmdc fvmptd3 eqeltrd zmulcl seqf simplr cmpt eqeq1d ifbid breq1d + nnabscl ffvelrnd zmulcld anbi12d ifeq12d mpteq2dv eqtr4di seqeq3d fveq12d + breq2d eleq1d ifeq1d fveq2d ifbieq12d df-lgs ovmpoga mpd3an3 ) AFGZDFGZDH + IZAJKLZMIZMHNZDHUBUEZAHUBUEZOZMUFZMNZDUGUHZPCMUIZUHZPLZNZFGADUJLUVMIUURUU + SOZUUTUVCUVLFUVNUUTOZUVBMHFUVOUKZUVOULUVOUVAFGZMFGZUVBQUURUVQUUSUUTAUMUNU + VPUVAMURUOUPUVNUUTUSZOZUVHUVKUVTUVFUVGMFUVGFGUVTUTVAUVTUKZUVTUVDUVEUVNUUS + UVSHFGZUVDQUURUUSVBZUVTULZDHVCVDUVNUURUVSUWBUVEQUURUUSVEUWDAHVCVDVFUPUVTR + FUVIUVJUVTUAUCPFCMRVKUWAUVTUAVGZRGZOZUWECUHUWEVHGZUWEJIZJAVIUEZHAVJVLLZMV + MVNZGZMUVGNZNZAUWEMVOLZJVPLZKLZMVQLZUWEVLLZMVOLZNZUWEDWDLZKLZMNZFUWGBUWEB + VGZVHGZUXFJIZUWOAUXFMVOLZJVPLZKLZMVQLZUXFVLLZMVOLZNZUXFDWDLZKLZMNZUXERCFE + UXFUWEIZUXGUWHUXQUXDMUXFUWEVHVRUXSUXOUXBUXPUXCKUXSUXHUWIUXNUXAUWOUXFUWEJV + SUXSUXMUWTMVOUXSUXLUWSUXFUWEVLUXSUXKUWRMVQUXSUXJUWQAKUXSUXIUWPJVPUXFUWEMV + OVTSWASUXSWEWBSWCUXFUWEDWDVTWBWFUVTUWFVBUWGUWHUXDMFUWGUWHOZUXBFGUXCWGGZUX + DFGUXTUWIUWOUXAFUXTUWIOZUWJHUWNFUYBULUYBUWMMUVGFUYBUKZUYBMUYCWHUURUWMQZUU + SUVSUWFUWHUWIUURUYDUWKMIZUWKVMIZWIZQZUURUYEQZUYFQZUYHUURUWKFGZUVRUYIUURUW + KUURAVJUURWEZVJRGUURWJVAWKZWLZUURUKUWKMURUOUURUYKVMFGUYJUYNVMWMWNUWKVMURW + OUYEUYFWPWRUURUWMUYGUURUURUWKWGGUWMUYGWQUYLUYMUWKMVMWGWSWTXAXBXCUPUYBJRGU + URUWJQXDUURUUSUVSUWFUWHUWIXEJAXFXGUPUXTUWIUSZOZUWTMUYPUWTUYPUWSUWEUYPUWRU + YPUURUWQWGGZUWRFGUURUUSUVSUWFUWHUYOXEUYPJUWEVIUEUSZUYQUYPUYRUWIUXTUYOVBUW + HUYRUWIWIUWGUYOUWHUWIUYRUWEXHXIXJXKUWHUYRUYQWQZUWGUYOUWHUWEWGGUYSUWHUWEUW + EXLXMUWEXNXOXJXPAUWQXSUOXQUVTUWFUWHUYOXRWKWLUYPUKXTUXTUWEFGZJFGUWIQUWFUYT + UVTUWHUWEYAXJYBUWEJURWOYCUXTUWHUUSDHYDZUYAUWGUWHVBUURUUSUVSUWFUWHYEUVSVUA + UVNUWFUWHDHYFZYGUWEDYJYHUXBUXCXSUOUWGUWHUSOUKUWFUWHQUVTUWEYKYIYCZYLVUCYMU + YTUCVGZFGOUWEVUDPLFGUVTUWEVUDYNYIYOUVTUUSVUAUVIRGUURUUSUVSYPUVSVUAUVNVUBY + IDUUAUOUUBUUCUVNUUSUWBUUTQUWCUVNULDHURUOYCUDUQADFFUQVGZHIZUDVGZJKLZMIZMHN + ZVUEHUBUEZVUGHUBUEZOZUVGMNZVUEUGUHZPBRUXGUXHJVUGVIUEZHVUGVJVLLZUWLGZMUVGN + ZNZVUGUXJKLZMVQLZUXFVLLZMVOLZNZUXFVUEWDLZKLZMNZYQZMUIZUHZPLZNUVMUJFVUGAIZ + VUEDIZOZVUFUUTVUJVVLUVCUVLVVOVUEDHVVMVVNVBZYRVVOVUIUVBMHVVOVUHUVAMVVOVUGA + JKVVMVVNVEZSYRYSVVOVUNUVHVVKUVKPVVOVUMUVFUVGMVVOVUKUVDVULUVEVVOVUEDHUBVVP + YTVVOVUGAHUBVVQYTUUDYSVVOVUOUVIVVJUVJVVOVVICPMVVOVVIBRUXRYQZCVVOBRVVHUXRV + VOUXGVVGUXQMVVOVVEUXOVVFUXPKVVOUXHVUTUWOVVDUXNVVOVUPUWJVUSUWNHVVOVUGAJVIV + VQUUJVVOVURUWMMUVGVVOVUQUWKUWLVVOVUGAVJVLVVQSUUKYSWCVVOVVCUXMMVOVVOVVBUXL + UXFVLVVOVVAUXKMVQVVOVUGAUXJKVVQSSSSUUEVVOVUEDUXFWDVVPWAWBUULUUFCVVRCVVREE + CVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVV + RCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCV + VREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVRE + ECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECV + VRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRC + VVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVR + EECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREECVVRCVVREEC + VVRCVVREEETTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTTUUGUUHVVOV + UEDUGVVPUUMUUIWBUUNBUQUDUUOUUPUUQ $. $( Value of the function ` F ` which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by Jim @@ -156946,18 +157038,22 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is $( The Legendre symbol is an element of ` Z ` . (Contributed by Mario Carneiro, 4-Feb-2015.) $) lgscllem $p |- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. Z ) $= - ( cz wcel wa co cc0 c1 cif cmul a1i wdc syl2anc cn vy vz clgs wceq cexp - c2 clt wbr cneg cabs cseq lgsval lgslem2 simp3i simp2i zsqcl 1zzd zdceq - cfv syl2an2r ifcldcd adantr wn simp1i simpr 0zd zdclt syldan dcan2 sylc - nnuz cv wf df-ne lgsfcl2 3expa sylan2br ffvelrnda lgslem3 adantl simplr - wne seqf neqned nnabscl ffvelrnd ifcldadc eqeltrd ) BIJZEIJZKZBEUCLEMUD - ZBUFUELZNUDZNMOZEMUGUHZBMUGUHZKZNUIZNOZEUJUSZPDNUKZUSZPLZOFBCDEGULWKWLW - OXDFWKWOFJWLWKWNNMFNFJZWKWSFJZMFJZXEAFHUMZUNQZXGWKXFXGXEXHUOQWIWMIJWJNI - JWNRBUPWKUQWMNURUTVAVBWKWTFJWLVCZXCFJXDFJWKWRWSNFXFWKXFXGXEXHVDQXIWKWPR - ZWQRZWRRWKWJMIJZXKWIWJVEZWKVFZEMVGSWIWJXMXLXOBMVGVHWPWQVIVJVAWKXJKZTFXA - XBXPUAUBPFDNTVKXPUQXPTFUAVLZDXJWKEMWBZTFDVMZEMVNWIWJXRXSABCDEFGHVOVPVQV - RXQFJUBVLZFJKXQXTPLFJXPAXQXTFHVSVTWCXPWJXRXATJWIWJXJWAXPEMWKXJVEWDEWESW - FAWTXCFHVSUTWKWJXMWLRXNXOEMURSWGWH $. + ( cz wcel wa co cc0 c1 cif wbr cmul wdc cn 3eqtr2i vy vz clgs wceq cexp + c2 clt cneg cabs cfv cseq lgsval lgslem2 simp3i simp2i zsqcl 1zzd zdceq + a1i syl2an2r ifcldcd adantr simp1i simpr 0zd zdclt syl2anc syldan dcand + wn nnuz cv wne wf df-ne lgsfcl2 3expa sylan2br ffvelrnda lgslem3 adantl + seqf simplr neneqad nnabscl ffvelrnd cle crab ifcldadc eqeltrd ) BIJZEI + JZKZBEUCLEMUDZBUFUELZNUDZNMOZEMUGPZBMUGPZKZNUHZNOZEUIUJZQDNUKZUJZQLZOFB + CDEGULWMWNWQXFFWMWQFJWNWMWPNMFNFJZWMXAFJZMFJZXGAFHUMZUNUSZXIWMXHXIXGXJU + OUSWKWOIJWLNIJWPRBUPWMUQWONURUTVAVBWMXBFJWNVJZXEFJXFFJWMWTXANFXHWMXHXIX + GXJVCUSXKWMWRWSWMWLMIJZWRRWKWLVDZWMVEZEMVFVGWKWLXMWSRXOBMVFVHVIVAWMXLKZ + SFXCXDXPUAUBQFDNSVKXPUQXPSFUAVLZDXLWMEMVMZSFDVNZEMVOWKWLXRXSABCDEFGHVPV + QVRVSXQFJUBVLZFJKXQXTQLFJXPAXQXTFHVTWAWBXPWLXRXCSJWKWLXLWCXPEMWMXLVDWDE + WEVGWFAXBXEFFAVLUIUJNWGPAIWHZFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFY + AHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAF + YAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYA + FYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHFYAFYAHHHTTTTTTTTT + TTTTTTTTTTTTTTTTTTTTTTVTUTWMWLXMWNRXNXOEMURVGWIWJ $. $} $( Closure of the function ` F ` which defines the Legendre symbol at the @@ -157181,37 +157277,37 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is by Mario Carneiro, 4-Feb-2015.) $) lgsneg $p |- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( A /L -u N ) = ( if ( A < 0 , -u 1 , 1 ) x. ( A /L N ) ) ) $= - ( vn cz wcel cc0 wbr wa c1 cif cfv cmul cn co wceq adantl wdc 0z syl cc - vx vy wne w3a cneg clt cabs cv cprime clgs cpc cexp cmpt wn iftrue oveq1d - cseq simpl2 zdclt mpan2 oveq2 neg1mulneg1e1 eqtrdi ax-1cn mulm1i biantrud - ifsbdc simpr ifbid oveq2d cle simpl3 necomd zltlen sylancl mpbiran2d zred - wb le0neg1d cr renegcld lenlt sylancr 3bitrd znegcl ifnotdc eqtrd 3eqtr3d - 3eqtrd 1t1e1 iffalse intnand iffalsed oveq12d 3eqtr4a wo exmiddc mpjaodan - 0re simp1 eqcomd cq pcneg syl2anc adantlr ifeq1dadc mpteq2dva seqeq3d zcn - zq prmdc 3ad2ant2 absnegd fveq12d neg1cn a1i ifcldcd dcan2 sylc nnuz 1zzd - eqid lgsfcl3 ffvelrnda zmulcl seqf nnabscl 3adant1 ffvelrnd mulassd simp3 - zcnd negne0d lgsval4 syl3anc 3eqtr4d ) ADEZBDEZBFUCZUDZBUEZFUFGZAFUFGZHZI - UEZIJZUUAUGKZLCMCUHZUIEZAUUHUJNZUUHUUAUKNZULNZIJZUMZIUQZKZLNZUUCUUEIJZBFU - FGZUUCHZUUEIJZBUGKZLCMUUIUUJUUHBUKNZULNZIJZUMZIUQZKZLNZLNZAUUAUJNZUURABUJ - NZLNYTUUQUURUVALNZUVHLNUVJYTUUFUVMUUPUVHLYTUVMUUFYTUUCUVMUUFOUUCUNZYTUUCH - ZUVMUUEUVALNZUUBUUEIJZUUFUVOUURUUEUVALUUCUURUUEOYTUUCUUEIUOPUPUVOUUEUUSUU - EIJZLNZUUSIUUEJZUVPUVQUVOYRUVSUVTOZYQYRYSUUCURZYRUUSQZUWAYRFDEZUWCRBFUSUT - ZUUSUUEIUVSIUUEUVRUUEOUVSUUEUUELNIUVRUUEUUELVAVBVCUVRIOUVSUUEILNUUEUVRIUU - ELVAIVDVEVCVGSSUVOUVRUVAUUELUVOUUSUUTUUEIUVOUUCUUSYTUUCVHZVFVIVJUVOUVTUUB - UNZIUUEJZUVQUVOUUSUWGIUUEUVOUUSBFVKGZFUUAVKGZUWGUVOUUSUWIFBUCZUVOBFYQYRYS - UUCVLVMUVOYRUWDUUSUWIUWKHVRUWBRBFVNVOVPUVOBUVOBUWBVQZVSUVOFVTEUUAVTEUWJUW - GVRWSUVOBUWLWAFUUAWBWCWDVIUVOYRUWHUVQOZUWBYRUUBQZUWMYRUUADEZUWDUWNBWEZRUU - AFUSVOUUBIUUEWFSSWGWHUVOUUBUUDUUEIUVOUUCUUBUWFVFVIWIYTUVNHZIILNIUVMUUFWJU - WQUURIUVAILUVNUURIOYTUUCUUEIWKPUWQUUTUUEIUWQUUCUUSYTUVNVHZWLWMWNUWQUUDUUE - IUWQUUCUUBUWRWLWMWOYTUUCQZUUCUVNWPYTYQUWDUWSYQYRYSWTZRAFUSVOZUUCWQSWRXAYT - UUGUVBUUOUVGYTUUNUVFLIYTCMUUMUVEYTUUHMEZHUUIUULUVDIYTUUIUULUVDOUXBYTUUIHZ - UUKUVCUUJULUXCUUIBXBEZUUKUVCOYTUUIVHUXCYRUXDYQYRYSUUIURBXJSBUUHXCXDVJXEUX - BUUIQYTUUHXKPXFXGXHYTBYRYQBTEYSBXIXLZXMXNWNYTUURUVAUVHYTUUCUUEITUUETEYTXO - XPZITEYTVDXPZUXAXQYTUUTUUEITUXFUXGYTUWCUWSUUTQYRYQUWCYSUWEXLUXAUUSUUCXRXS - XQYTUVHYTMDUVBUVGYTUAUBLDUVFIMXTYTYAYTMDUAUHZUVFACUVFBUVFYBZYCYDUXHDEUBUH - ZDEHUXHUXJLNDEYTUXHUXJYEPYFYRYSUVBMEYQBYGYHYIYLYJWGYTYQUWOUUAFUCUVKUUQOUW - TYRYQUWOYSUWPXLYTBUXEYQYRYSYKYMACUUNUUAUUNYBYNYOYTUVLUVIUURLACUVFBUXIYNVJ - YP $. + ( vn cz wcel cc0 wne wbr wa c1 cif cfv cmul cn co wceq adantl wdc 0z cc + vx vy w3a cneg clt cabs cv cprime clgs cpc cexp cmpt iftrue oveq1d simpl2 + cseq wn zdclt mpan2 oveq2 neg1mulneg1e1 eqtrdi ax-1cn mulm1i ifsbdc simpr + 3syl biantrud ifbid oveq2d simpl3 necomd wb zltlen sylancl mpbiran2d zred + cle le0neg1d cr renegcld lenlt sylancr 3bitrd znegcl ifnotdc eqtrd 3eqtrd + 0re 3eqtr3d 1t1e1 iffalse intnand iffalsed oveq12d 3eqtr4a wo exmiddc syl + simp1 mpjaodan 3eqtr2rd cq zq syl2anc adantlr ifeq1dadc mpteq2dva seqeq3d + pcneg prmdc zcn 3ad2ant2 absnegd fveq12d a1i 1cnd ifcldcd dcand nnuz 1zzd + neg1cn eqid lgsfcl3 ffvelrnda seqf nnabscl 3adant1 ffvelrnd mulassd simp3 + zmulcl zcnd negne0d lgsval4 syl3anc 3eqtr4d ) ADEZBDEZBFGZUCZBUDZFUEHZAFU + EHZIZJUDZJKZUUBUFLZMCNCUGZUHEZAUUIUIOZUUIUUBUJOZUKOZJKZULZJUPZLZMOZUUDUUF + JKZBFUEHZUUDIZUUFJKZBUFLZMCNUUJUUKUUIBUJOZUKOZJKZULZJUPZLZMOZMOZAUUBUIOZU + USABUIOZMOUUAUURUUSUVBMOZUVIMOUVKUUAUUGUVNUUQUVIMUUAUVNUUGUVNUUGUUAUUDUVN + UUGPUUDUQZUUAUUDIZUVNUUFUVBMOZUUCUUFJKZUUGUVPUUSUUFUVBMUUDUUSUUFPUUAUUDUU + FJUMQUNUVPUUFUUTUUFJKZMOZUUTJUUFKZUVQUVRUVPYSUUTRZUVTUWAPYRYSYTUUDUOZYSFD + EZUWBSBFURUSZUUTUUFJUVTJUUFUVSUUFPUVTUUFUUFMOJUVSUUFUUFMUTVAVBUVSJPUVTUUF + JMOUUFUVSJUUFMUTJVCVDVBVEVGUVPUVSUVBUUFMUVPUUTUVAUUFJUVPUUDUUTUUAUUDVFZVH + VIVJUVPUWAUUCUQZJUUFKZUVRUVPUUTUWGJUUFUVPUUTBFVRHZFUUBVRHZUWGUVPUUTUWIFBG + ZUVPBFYRYSYTUUDVKVLUVPYSUWDUUTUWIUWKIVMUWCSBFVNVOVPUVPBUVPBUWCVQZVSUVPFVT + EUUBVTEUWJUWGVMWIUVPBUWLWAFUUBWBWCWDVIUVPYSUUCRZUWHUVRPUWCYSUUBDEZUWDUWMB + WEZSUUBFURVOUUCJUUFWFVGWGWJUVPUUCUUEUUFJUVPUUDUUCUWFVHVIWHUUAUVOIZJJMOJUV + NUUGWKUWPUUSJUVBJMUVOUUSJPUUAUUDUUFJWLQUWPUVAUUFJUWPUUDUUTUUAUVOVFZWMWNWO + UWPUUEUUFJUWPUUDUUCUWQWMWNWPUUAUUDRZUUDUVOWQUUAYRUWDUWRYRYSYTWTZSAFURVOZU + UDWRWSXAZUXAUXAXBUUAUUHUVCUUPUVHUUAUUOUVGMJUUACNUUNUVFUUAUUINEZIUUJUUMUVE + JUUAUUJUUMUVEPUXBUUAUUJIZUULUVDUUKUKUXCUUJBXCEZUULUVDPUUAUUJVFUXCYSUXDYRY + SYTUUJUOBXDWSBUUIXJXEVJXFUXBUUJRUUAUUIXKQXGXHXIUUABYSYRBTEYTBXLXMZXNXOWOU + UAUUSUVBUVIUUAUUDUUFJTUUFTEUUAYBXPZUUAXQZUWTXRUUAUVAUUFJTUXFUXGUUAUUTUUDY + SYRUWBYTUWEXMUWTXSXRUUAUVIUUANDUVCUVHUUAUAUBMDUVGJNXTUUAYAUUANDUAUGZUVGAC + UVGBUVGYCZYDYEUXHDEUBUGZDEIUXHUXJMODEUUAUXHUXJYLQYFYSYTUVCNEYRBYGYHYIYMYJ + WGUUAYRUWNUUBFGUVLUURPUWSYSYRUWNYTUWOXMUUABUXEYRYSYTYKYNACUUOUUBUUOYCYOYP + UUAUVMUVJUUSMACUVGBUXIYOVJYQ $. $( The Legendre symbol for nonnegative first parameter is unchanged by negation of the second. (Contributed by Mario Carneiro, 4-Feb-2015.) $) @@ -157504,70 +157600,70 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is lgsdir $p |- ( ( ( A e. ZZ /\ B e. ZZ /\ N e. ZZ ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( ( A x. B ) /L N ) = ( ( A /L N ) x. ( B /L N ) ) ) $= - ( vn cz wcel cc0 wa wceq cmul co clgs cexp c1 cif wdc zcnd wbr oveq12d - cn vk vv w3a c2 wn cc 1cnd 0cnd zsqcl 3ad2ant2 1z zdceq sylancl ifcldcd - wne mulid2d ad3antrrr iftrue adantl oveq1d simpl1 ad2antrr simpl2 simpr - sqmuld sqcld 3eqtrd eqeq1d ifbid 3eqtr4d iffalse cdvds dvdsmul1 syl2anc - mul02d wb zmulcld dvdssq mpbid adantr breq2 syl5ibcom cle simprl neneqd - wi sqeq0 syl mtbird cn0 wo zsqcl2 elnn0 sylib ecased nnzd dvdsle nnge1d - 1nn jctird cr nnred 1re letri3 exmiddc mpjaodan oveq2 sylan9eqr clt cfv - lgs0 cv cprime cpc cmpt cseq nnuz wf eqid lgsfcl3 syl3anc ffvelrn lgscl - syl2an eqtrd adantlr ifbieq1d zexpcl ifcldadc fvmptd3 lgsval4 a1i zdclt - 1zzd 0z dcan2 sylc ffvelrnda seqf ffvelrnd sylibrd syld con3dimp simpl3 + ( vn cz wcel cc0 wa wceq cmul co clgs cexp cif sylancl zcnd wbr oveq12d + c1 cn vk vv w3a wne c2 wn cc 1cnd 0cnd wdc zsqcl 3ad2ant2 zdceq ifcldcd + 1z mulid2d ad3antrrr iftrue adantl oveq1d simpl1 ad2antrr simpl2 sqmuld + simpr sqcld 3eqtrd eqeq1d ifbid 3eqtr4d mul02d iffalse dvdsmul1 syl2anc + cdvds wb dvdssq mpbid adantr breq2 syl5ibcom cle wi simprl neneqd sqeq0 + zmulcld syl mtbird cn0 zsqcl2 elnn0 sylib ecased nnzd 1nn dvdsle nnge1d + wo jctird cr nnred 1re letri3 exmiddc mpjaodan oveq2 lgs0 sylan9eqr clt + cfv cv cprime cpc cmpt cseq nnuz wf eqid lgsfcl3 syl3anc ffvelrn syl2an + lgscl eqtrd adantlr 1t1e1 ifbieq1d zexpcl 1zzd ifcldadc fvmptd3 lgsval4 + a1i 0z zdclt dcand ffvelrnda seqf ffvelrnd sylibrd syld con3dimp simpl3 iffalsed 3eqtr4rd cneg cabs lgsdilem cuz nnabscl sylan eleqtrdi simpll1 - simpll3 elnnuz biimpri simpll2 prmz pczcl syl12anc mulexpd 1t1e1 eqcomi - lgsdirprm 3eqtr4a prmdc eleq1w oveq1 prod3fmul neg1cn zmulcl neg1z dcne - mul4d ) AEFZBEFZCEFZUCZAGUOZBGUOZHZHZCGIZABJKZCLKZACLKZBCLKZJKZICGUOZUW - CUWDHZAUDMKZNIZNGOZBUDMKZNIZNGOZJKZUWEUDMKZNIZNGOZUWIUWFUWKUWMUWRUXAIUW - MUEZUWKUWMHZNUWQJKZUWQUWRUXAUVSUXDUWQIUWBUWDUWMUVSUWQUVSUWPNGUFUVSUGUVS - UHUVSUWOEFZNEFZUWPPUVQUVPUXEUVRBUIUJUKUWONULUMUNZUPUQUXCUWNNUWQJUWMUWNN - IUWKUWMNGURUSUTUXCUWTUWPNGUXCUWSUWONUXCUWSUWLUWOJKNUWOJKUWOUXCABUWCAUFF - ZUWDUWMUWCAUVPUVQUVRUWBVAZQZVBUWCBUFFUWDUWMUWCBUVPUVQUVRUWBVCZQZVBVEUXC - UWLNUWOJUWKUWMVDUTUXCUWOUWCUWOUFFUWDUWMUWCBUXLVFVBUPVGVHVIVJUWKUXBHZGUW - QJKZGUWRUXAUVSUXNGIUWBUWDUXBUVSUWQUXGVOUQUXMUWNGUWQJUXBUWNGIUWKUWMNGVKU - SUTUXMUWTNGUWKUWTUWMUWKUWTUWLNVLRZUWMUWKUWLUWSVLRZUWTUXOUWCUXPUWDUWCAUW - EVLRZUXPUWCUVPUVQUXQUXIUXKABVMVNUWCUVPUWEEFZUXQUXPVPUXIUWCABUXIUXKVQZAU - WEVRVNVSVTUWSNUWLVLWAWBUWKUXOUWLNWCRZNUWLWCRZHZUWMUWKUXOUXTUYAUWKUWLEFZ - NTFUXOUXTWFUWKUWLUWCUWLTFZUWDUWCUYDUWLGIZUWCUYEAGIZUWCAGUVSUVTUWAWDWEUW - CUXHUYEUYFVPUXJAWGWHWIUWCUWLWJFZUYDUYEWKUWCUVPUYGUXIAWLWHUWLWMWNWOVTZWP - ZWSUWLNWQUMUWKUWLUYHWRWTUWKUWLXAFNXAFUWMUYBVPUWKUWLUYHXBXCUWLNXDUMUUAUU - BUUCUUEVJUWKUWMPZUWMUXBWKUWKUYCUXFUYJUYIUKUWLNULUMUWMXEWHXFUWKUWGUWNUWH - UWQJUWDUWCUWGAGLKZUWNCGALXGUWCUVPUYKUWNIUXIAXKWHXHUWDUWCUWHBGLKZUWQCGBL - XGUWCUVQUYLUWQIUXKBXKWHXHSUWDUWCUWFUWEGLKZUXACGUWELXGUWCUXRUYMUXAIUXSUW - EXKWHXHUUFUWCUWJHZCGXIRZUWEGXIRHNUUGZNOZCUUHXJZJDTDXLZXMFZUWEUYSLKZUYSC - XNKZMKZNOZXOZNXPXJZJKZUYOAGXIRZHZUYPNOZUYOBGXIRZHZUYPNOZJKZUYRJDTUYTAUY - SLKZVUBMKZNOZXOZNXPZXJZUYRJDTUYTBUYSLKZVUBMKZNOZXOZNXPZXJZJKZJKZUWFUWIU - YNUYQVUNVUFVVGJUWCUYQVUNIUWJABCUUIVTUYNUAVURVVDVUENUYRUYNUYRTNUUJXJZUWC - UVRUWJUYRTFUVPUVQUVRUWBUUDZCUUKUULZXQUUMUYNUAXLZVVIFZHZVVLVURXJZUYNTEVU - RXRZVVLTFZVVOEFVVMUYNUVPUVRUWJVVPUVPUVQUVRUWBUWJUUNZUVPUVQUVRUWBUWJUUOZ - UWCUWJVDZADVURCVURXSZXTYAZVVQVVMVVLUUPUUQZTEVVLVURYBYDQVVNVVLVVDXJZUYNT - EVVDXRZVVQVWDEFVVMUYNUVQUVRUWJVWEUVPUVQUVRUWBUWJUURZVVSVVTBDVVDCVVDXSZX - TYAZVWCTEVVLVVDYBYDQVVNVVLXMFZUWEVVLLKZVVLCXNKZMKZNOZVWIAVVLLKZVWKMKZNO - ZVWIBVVLLKZVWKMKZNOZJKZVVLVUEXJVVOVWDJKVVNVWIVWMVWTIZVWIUEZUYNVWIVXAVVM - UYNVWIHZVWLVWOVWRJKZVWMVWTVXCVWLVWNVWQJKZVWKMKVXDVXCVWJVXEVWKMVXCUVPUVQ - VWIVWJVXEIUYNUVPVWIVVRVTUYNUVQVWIVWFVTUYNVWIVDZABVVLUVEYAUTVXCVWNVWQVWK - VXCVWNUYNUVPVVLEFZVWNEFZVWIVVRVVLUUSZAVVLYCYDZQVXCVWQUYNUVQVXGVWQEFZVWI - VWFVXIBVVLYCYDZQVXCVWIUVRUWJVWKWJFZVXFUYNUVRVWIVVSVTUYNUWJVWIVVTVTVVLCU - UTUVAZUVBYEVWIVWMVWLIUYNVWIVWLNURUSVWIVWTVXDIUYNVWIVWPVWOVWSVWRJVWIVWON - URVWIVWRNURSUSVJYFVXBVXAVVNVXBNNNJKZVWMVWTVXONUVCUVDVWIVWLNVKVXBVWPNVWS - NJVWIVWONVKVWIVWRNVKSUVFUSVVNVWIPZVWIVXBWKVVNVVQVXPVVMVVQUYNVWCUSZVVLUV - GWHZVWIXEWHXFVVNDVVLVUDVWMTVUEEVUEXSZUYSVVLIZUYTVWIVUCVWLNDUAXMUVHZVXTV - UAVWJVUBVWKMUYSVVLUWELXGUYSVVLCXNUVIZSYGVXQVVNVWIVWLNEVVNVWIHZVWJEFZVXM - VWLEFVYCUXRVXGVYDUWCUXRUWJVVMVWIUXSUQVWIVXGVVNVXIUSUWEVVLYCVNUYNVWIVXMV - VMVXNYFZVWJVWKYHVNVVNVXBHYNZVXRYIYJVVNVVOVWPVWDVWSJVVNDVVLVUQVWPTVUREVW - AVXTUYTVWIVUPVWONVYAVXTVUOVWNVUBVWKMUYSVVLALXGVYBSYGVXQVVNVWIVWONEVYCVX - HVXMVWOEFUYNVWIVXHVVMVXJYFVYEVWNVWKYHVNVYFVXRYIYJVVNDVVLVVCVWSTVVDEVWGV - XTUYTVWIVVBVWRNVYAVXTVVAVWQVUBVWKMUYSVVLBLXGVYBSYGVXQVVNVWIVWRNEVYCVXKV - XMVWREFUYNVWIVXKVVMVXLYFVYEVWQVWKYHVNVYFVXRYIYJSVJUVJSUYNUXRUVRUWJUWFVU - GIUWCUXRUWJUXSVTVVSVVTUWEDVUECVXSYKYAUYNUWIVUJVUTJKZVUMVVFJKZJKVVHUYNUW - GVYGUWHVYHJUYNUVPUVRUWJUWGVYGIVVRVVSVVTADVURCVWAYKYAUYNUVQUVRUWJUWHVYHI - VWFVVSVVTBDVVDCVWGYKYASUYNVUJVUTVUMVVFUYNVUIUYPNUFUYPUFFUYNUVKYLUYNUGUY - NUYOPZVUHPZVUIPUYNUVRGEFZVYIVVSYOCGYMUMZUYNUVPVYKVYJVVRYOAGYMUMUYOVUHYP - YQUNUYNVUTUYNTEUYRVUSUYNUAUBJEVURNTXQUYNYNZUYNTEVVLVURVWBYRVXGUBXLZEFHV - VLVYNJKEFUYNVVLVYNUVLUSZYSVVKYTQUYNVUMUYNVULUYPNEUYPEFUYNUVMYLVYMUYNVYI - VUKPZVULPVYLUYNUVQVYKVYPVWFYOBGYMUMUYOVUKYPYQUNQUYNVVFUYNTEUYRVVEUYNUAU - BJEVVDNTXQVYMUYNTEVVLVVDVWHYRVYOYSVVKYTQUVOYEVJUWCUWDPZUWDUWJWKUWCUVRVY - KVYQVVJYOCGULUMCGUVNWNXF $. + simpll3 elnnuz biimpri simpll2 lgsdirprm simplr pczcl syl12anc 3eqtr2ri + prmz mulexpd 3eqtr4a prmdc eleq1 oveq1 ad5ant12 prod3fmul neg1cn zmulcl + 3syl neg1z mul4d dcne ) AEFZBEFZCEFZUCZAGUDZBGUDZHZHZCGIZABJKZCLKZACLKZ + BCLKZJKZICGUDZUWEUWFHZAUEMKZSIZSGNZBUEMKZSIZSGNZJKZUWGUEMKZSIZSGNZUWKUW + HUWMUWOUWTUXCIUWOUFZUWMUWOHZSUWSJKZUWSUWTUXCUWAUXFUWSIUWDUWFUWOUWAUWSUW + AUWRSGUGUWAUHUWAUIUWAUWQEFZSEFZUWRUJUVSUVRUXGUVTBUKULUOUWQSUMOUNZUPUQUX + EUWPSUWSJUWOUWPSIUWMUWOSGURUSUTUXEUXBUWRSGUXEUXAUWQSUXEUXAUWNUWQJKSUWQJ + KUWQUXEABUWEAUGFZUWFUWOUWEAUVRUVSUVTUWDVAZPZVBUWEBUGFUWFUWOUWEBUVRUVSUV + TUWDVCZPZVBVDUXEUWNSUWQJUWMUWOVEUTUXEUWQUWEUWQUGFUWFUWOUWEBUXNVFVBUPVGV + HVIVJUWMUXDHZGUWSJKZGUWTUXCUWAUXPGIUWDUWFUXDUWAUWSUXIVKUQUXOUWPGUWSJUXD + UWPGIUWMUWOSGVLUSUTUXOUXBSGUWMUXBUWOUWMUXBUWNSVOQZUWOUWMUWNUXAVOQZUXBUX + QUWEUXRUWFUWEAUWGVOQZUXRUWEUVRUVSUXSUXKUXMABVMVNUWEUVRUWGEFZUXSUXRVPUXK + UWEABUXKUXMWGZAUWGVQVNVRVSUXASUWNVOVTWAUWMUXQUWNSWBQZSUWNWBQZHZUWOUWMUX + QUYBUYCUWMUWNEFZSTFUXQUYBWCUWMUWNUWEUWNTFZUWFUWEUYFUWNGIZUWEUYGAGIZUWEA + GUWAUWBUWCWDWEUWEUXJUYGUYHVPUXLAWFWHWIUWEUWNWJFZUYFUYGWSUWEUVRUYIUXKAWK + WHUWNWLWMWNVSZWOZWPUWNSWQOUWMUWNUYJWRWTUWMUWNXAFSXAFUWOUYDVPUWMUWNUYJXB + XCUWNSXDOUUAUUBUUCUUEVJUWMUWOUJZUWOUXDWSUWMUYEUXHUYLUYKUOUWNSUMOUWOXEWH + XFUWMUWIUWPUWJUWSJUWFUWEUWIAGLKZUWPCGALXGUWEUVRUYMUWPIUXKAXHWHXIUWFUWEU + WJBGLKZUWSCGBLXGUWEUVSUYNUWSIUXMBXHWHXIRUWFUWEUWHUWGGLKZUXCCGUWGLXGUWEU + XTUYOUXCIUYAUWGXHWHXIUUFUWEUWLHZCGXJQZUWGGXJQHSUUGZSNZCUUHXKZJDTDXLZXMF + ZUWGVUALKZVUACXNKZMKZSNZXOZSXPXKZJKZUYQAGXJQZHZUYRSNZUYQBGXJQZHZUYRSNZJ + KZUYTJDTVUBAVUALKZVUDMKZSNZXOZSXPZXKZUYTJDTVUBBVUALKZVUDMKZSNZXOZSXPZXK + ZJKZJKZUWHUWKUYPUYSVUPVUHVVIJUWEUYSVUPIUWLABCUUIVSUYPUAVUTVVFVUGSUYTUYP + UYTTSUUJXKZUWEUVTUWLUYTTFUVRUVSUVTUWDUUDZCUUKUULZXQUUMUYPUAXLZVVKFZHZVV + NVUTXKZUYPTEVUTXRZVVNTFZVVQEFVVOUYPUVRUVTUWLVVRUVRUVSUVTUWDUWLUUNZUVRUV + SUVTUWDUWLUUOZUWEUWLVEZADVUTCVUTXSZXTYAZVVSVVOVVNUUPUUQZTEVVNVUTYBYCPVV + PVVNVVFXKZUYPTEVVFXRZVVSVWFEFVVOUYPUVSUVTUWLVWGUVRUVSUVTUWDUWLUURZVWAVW + BBDVVFCVVFXSZXTYAZVWETEVVNVVFYBYCPVVPVVNXMFZUWGVVNLKZVVNCXNKZMKZSNZVWKA + VVNLKZVWMMKZSNZVWKBVVNLKZVWMMKZSNZJKZVVNVUGXKVVQVWFJKVVPVWKVWOVXBIZVWKU + FZUYPVWKVXCVVOUYPVWKHZVWNVWQVWTJKZVWOVXBVXEVWNVWPVWSJKZVWMMKVXFVXEVWLVX + GVWMMVXEUVRUVSVWKVWLVXGIUYPUVRVWKVVTVSUYPUVSVWKVWHVSUYPVWKVEZABVVNUUSYA + UTVXEVWPVWSVWMVXEVWPUYPUVRVVNEFZVWPEFZVWKVVTVVNUVDZAVVNYDYCZPVXEVWSUYPU + VSVXIVWSEFZVWKVWHVXKBVVNYDYCZPVXEVWKUVTUWLVWMWJFZVXHUYPUVTVWKVWAVSUWEUW + LVWKUUTVVNCUVAUVBZUVEYEVWKVWOVWNIUYPVWKVWNSURUSVWKVXBVXFIUYPVWKVWRVWQVX + AVWTJVWKVWQSURVWKVWTSURRUSVJYFVXDVXCVVPVXDSSSJKZVWOVXBVXQSVXQSYGYGYGUVC + VWKVWNSVLVXDVWRSVXASJVWKVWQSVLVWKVWTSVLRUVFUSVVPVVSVWKUJZVWKVXDWSVVOVVS + UYPVWEUSZVVNUVGZVWKXEUVNXFVVPDVVNVUFVWOTVUGEVUGXSZVUAVVNIZVUBVWKVUEVWNS + VUAVVNXMUVHZVYBVUCVWLVUDVWMMVUAVVNUWGLXGVUAVVNCXNUVIZRYHVXSVVPVWKVWNSEV + VPVWKHZVWLEFZVXOVWNEFVYEUXTVXIVYFUWAUWDUXTUWLVVOVWKUYAUVJVWKVXIVVPVXKUS + UWGVVNYDVNUYPVWKVXOVVOVXPYFZVWLVWMYIVNVVPVXDHYJZVVPVVSVXRVXSVXTWHZYKYLV + VPVVQVWRVWFVXAJVVPDVVNVUSVWRTVUTEVWCVYBVUBVWKVURVWQSVYCVYBVUQVWPVUDVWMM + VUAVVNALXGVYDRYHVXSVVPVWKVWQSEVYEVXJVXOVWQEFUYPVWKVXJVVOVXLYFVYGVWPVWMY + IVNVYHVYIYKYLVVPDVVNVVEVXATVVFEVWIVYBVUBVWKVVDVWTSVYCVYBVVCVWSVUDVWMMVU + AVVNBLXGVYDRYHVXSVVPVWKVWTSEVYEVXMVXOVWTEFUYPVWKVXMVVOVXNYFVYGVWSVWMYIV + NVYHVYIYKYLRVJUVKRUYPUXTUVTUWLUWHVUIIUWEUXTUWLUYAVSVWAVWBUWGDVUGCVYAYMY + AUYPUWKVULVVBJKZVUOVVHJKZJKVVJUYPUWIVYJUWJVYKJUYPUVRUVTUWLUWIVYJIVVTVWA + VWBADVUTCVWCYMYAUYPUVSUVTUWLUWJVYKIVWHVWAVWBBDVVFCVWIYMYARUYPVULVVBVUOV + VHUYPVUKUYRSUGUYRUGFUYPUVLYNUYPUHUYPUYQVUJUYPUVTGEFZUYQUJVWAYOCGYPOZUYP + UVRVYLVUJUJVVTYOAGYPOYQUNUYPVVBUYPTEUYTVVAUYPUAUBJEVUTSTXQUYPYJZUYPTEVV + NVUTVWDYRVXIUBXLZEFHVVNVYOJKEFUYPVVNVYOUVMUSZYSVVMYTPUYPVUOUYPVUNUYRSEU + YREFUYPUVOYNVYNUYPUYQVUMVYMUYPUVSVYLVUMUJVWHYOBGYPOYQUNPUYPVVHUYPTEUYTV + VGUYPUAUBJEVVFSTXQVYNUYPTEVVNVVFVWJYRVYPYSVVMYTPUVPYEVJUWEUWFUJZUWFUWLW + SUWEUVTVYLVYQVVLYOCGUMOCGUVQWMXF $. $} ${ @@ -157630,50 +157726,50 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is mpbid nnuz wf simpl1 eqid lgsfcl3 syl3anc elnnuz biimpri ffvelrn syl2an caddc simpr ad2antrr pcmul syl122anc oveq2d prmz adantl lgscl cn0 pczcl wn syl12anc expaddd eqtrd iftrue 3eqtr4rd 1t1e1 iffalse 3eqtr4a exmiddc - wdc prmdc syl mpjaodan eleq1w oveq2 oveq1 ifbieq1d zexpcl 1zzd ifcldadc - wo fvmptd3 prod3fmul lgsdilem2 mulcomd fveq2d lgsval4 neg1z zdclt dcan2 - eqtr4d a1i sylc ifcldcd ffvelrnda zmulcl seqf ffvelrnd mul4d 3eqtr4d ) - AEFZBEFZCEFZUCZBGUDZCGUDZHZHZBCIJZGUEKZAGUEKZHZLUFZLMZUUHUGNZIDTDUHZUIF - ZAUUOUJJZUUOUUHOJZPJZLMZUKZLULNZIJZBGUEKZUUJHZUULLMZCGUEKZUUJHZUULLMZIJ - ZBUGNZIDTUUPUUQUUOBOJZPJZLMZUKZLULZNZCUGNZIDTUUPUUQUUOCOJZPJZLMZUKZLULZ - NZIJZIJZAUUHUJJZABUJJZACUJJZIJZUUGUUMUVJUVBUWEIUUGUUJUUIHZUULLMZUUJUVDH - ZUULLMZUUJUVGHZUULLMZIJZUUMUVJUUCUUAUUBYTUCUUFUWLUWQQYTUUAUUBUMBCAUNUOU - UKUWKUPUUMUWLQUUIUUJUQUUKUWKUULLURUSUVFUWNUVIUWPIUVEUWMUPUVFUWNQUVDUUJU - QUVEUWMUULLURUSUVHUWOUPUVIUWPQUVGUUJUQUVHUWOUULLURUSUTVAUUGUVBUUNUVPNZU - UNUWCNZIJUWEUUGUAUVOUWBUVALUUNUUGUUNTLVFNZUUGUUHEFZUUHGUDZUUNTFUUGBCYTU - UAUUBUUFVBZYTUUAUUBUUFVCZVDZUUGUUHGVGKZUXBUUGBCUUGBUXCRZUUGCUXDRZUUGBGV - GKZUUDUUCUUDUUEVEZUUGUUAGEFZUXIUUDUPUXCVHBGVIVJVKUUGCGVGKZUUEUUCUUDUUEV - LZUUGUUBUXKUXLUUEUPUXDVHCGVIVJVKVMUUGUXAUXKUXFUXBUPUXEVHUUHGVIVJVQZUUHV - NVOVRVPUUGUAUHZUWTFZHZUXOUVONZUUGTEUVOVSZUXOTFZUXREFUXPUUGYTUUAUUDUXSYT - UUAUUBUUFVTZUXCUXJADUVOBUVOWAZWBWCZUXTUXPUXOWDWEZTEUXOUVOWFWGRUXQUXOUWB - NZUUGTEUWBVSZUXTUYEEFUXPUUGYTUUBUUEUYFUYAUXDUXMADUWBCUWBWAZWBWCZUYDTEUX - OUWBWFWGRUXQUXOUIFZAUXOUJJZUXOBOJZPJZLMZUYIUYJUXOCOJZPJZLMZIJZUYIUYJUXO - UUHOJZPJZLMZUXRUYEIJUXOUVANUXQUYIUYQUYTQZUYIWSZUXQUYIHZUYSUYLUYOIJZUYTU - YQVUCUYSUYJUYKUYNWHJZPJVUDVUCUYRVUEUYJPVUCUYIUUAUUDUUBUUEUYRVUEQUXQUYIW - IZUUGUUAUXPUYIUXCWJZUUGUUDUXPUYIUXJWJZUUGUUBUXPUYIUXDWJZUUGUUEUXPUYIUXM - WJZBCUXOWKWLWMVUCUYJUYKUYNVUCUYJVUCYTUXOEFZUYJEFZUUGYTUXPUYIUYAWJUYIVUK - UXQUXOWNWOAUXOWPVOZRVUCUYIUUBUUEUYNWQFZVUFVUIVUJUXOCWRWTZVUCUYIUUAUUDUY - KWQFZVUFVUGVUHUXOBWRWTZXAXBUYIUYTUYSQUXQUYIUYSLXCWOUYIUYQVUDQUXQUYIUYMU - YLUYPUYOIUYIUYLLXCUYIUYOLXCSWOXDVUBVUAUXQVUBLLIJLUYQUYTXEVUBUYMLUYPLIUY - IUYLLXFUYIUYOLXFSUYIUYSLXFXGWOUXPUYIVUBXTZUUGUXPUXTVURUYDUXTUYIXIZVURUX - OXJZUYIXHXKXKWOXLUXQUXRUYMUYEUYPIUXQDUXOUVNUYMTUVOEUYBUUOUXOQZUUPUYIUVM - UYLLDUAUIXMZVVAUUQUYJUVLUYKPUUOUXOAUJXNZUUOUXOBOXOSXPUXPUXTUUGUYDWOZUXQ - UYIUYLLEVUCVULVUPUYLEFVUMVUQUYJUYKXQVOUXQVUBHXRZUXQUXTVUSVVDVUTXKZXSYAU - XQDUXOUWAUYPTUWBEUYGVVAUUPUYIUVTUYOLVVBVVAUUQUYJUVSUYNPVVCUUOUXOCOXOSXP - VVDUXQUYIUYOLEVUCVULVUNUYOEFVUMVUOUYJUYNXQVOVVEVVFXSYASUXQDUXOUUTUYTTUV - AEUVAWAZVVAUUPUYIUUSUYSLVVBVVAUUQUYJUURUYRPVVCUUOUXOUUHOXOSXPVVDUXQUYIU - YSLEVUCVULUYRWQFZUYSEFVUMVUCUYIUXAUXBVVHVUFUUGUXAUXPUYIUXEWJUUGUXBUXPUY - IUXNWJUXOUUHWRWTUYJUYRXQVOVVEVVFXSYAXDYBUUGUVQUWRUWDUWSIUUGADUVOBCUYAUX - CUXDUXJUXMUYBYCUUGUWDCBIJZUGNZUWCNUWSUUGADUWBCBUYAUXDUXCUXMUXJUYGYCUUGU - UNVVJUWCUUGUUHVVIUGUUGBCUXGUXHYDYEYEYJSYJSUUGYTUXAUXBUWGUVCQUYAUXEUXNAD - UVAUUHVVGYFWCUUGUWJUVFUVQIJZUVIUWDIJZIJUWFUUGUWHVVKUWIVVLIUUGYTUUAUUDUW - HVVKQUYAUXCUXJADUVOBUYBYFWCUUGYTUUBUUEUWIVVLQUYAUXDUXMADUWBCUYGYFWCSUUG - UVFUVQUVIUWDUUGUVFUUGUVEUULLEUULEFUUGYGYKZUUGXRZUUGUVDXIZUUJXIZUVEXIUUG - UUAUXKVVOUXCVHBGYHVJUUGYTUXKVVPUYAVHAGYHVJZUVDUUJYIYLYMRUUGUVQUUGTEUVKU - VPUUGUAUBIEUVOLTVRVVNUUGTEUXOUVOUYCYNVUKUBUHZEFHUXOVVRIJEFUUGUXOVVRYOWO - ZYPUUGUUAUUDUVKTFUXCUXJBVNVOYQRUUGUVIUUGUVHUULLEVVMVVNUUGUVGXIZVVPUVHXI - UUGUUBUXKVVTUXDVHCGYHVJVVQUVGUUJYIYLYMRUUGUWDUUGTEUVRUWCUUGUAUBIEUWBLTV - RVVNUUGTEUXOUWBUYHYNVVSYPUUGUUBUUEUVRTFUXDUXMCVNVOYQRYRXBYS $. + wdc prmdc 3syl mpjaodan eleq1 oveq2 oveq1 ifbieq1d zexpcl 1zzd ifcldadc + syl fvmptd3 prod3fmul lgsdilem2 mulcomd fveq2d eqtr4d lgsval4 neg1z a1i + wo zdclt dcand ifcldcd ffvelrnda zmulcl seqf ffvelrnd mul4d 3eqtr4d ) A + EFZBEFZCEFZUCZBGUDZCGUDZHZHZBCIJZGUEKZAGUEKZHZLUFZLMZUUHUGNZIDTDUHZUIFZ + AUUOUJJZUUOUUHOJZPJZLMZUKZLULNZIJZBGUEKZUUJHZUULLMZCGUEKZUUJHZUULLMZIJZ + BUGNZIDTUUPUUQUUOBOJZPJZLMZUKZLULZNZCUGNZIDTUUPUUQUUOCOJZPJZLMZUKZLULZN + ZIJZIJZAUUHUJJZABUJJZACUJJZIJZUUGUUMUVJUVBUWEIUUGUUJUUIHZUULLMZUUJUVDHZ + UULLMZUUJUVGHZUULLMZIJZUUMUVJUUCUUAUUBYTUCUUFUWLUWQQYTUUAUUBUMBCAUNUOUU + KUWKUPUUMUWLQUUIUUJUQUUKUWKUULLURUSUVFUWNUVIUWPIUVEUWMUPUVFUWNQUVDUUJUQ + UVEUWMUULLURUSUVHUWOUPUVIUWPQUVGUUJUQUVHUWOUULLURUSUTVAUUGUVBUUNUVPNZUU + NUWCNZIJUWEUUGUAUVOUWBUVALUUNUUGUUNTLVFNZUUGUUHEFZUUHGUDZUUNTFUUGBCYTUU + AUUBUUFVBZYTUUAUUBUUFVCZVDZUUGUUHGVGKZUXBUUGBCUUGBUXCRZUUGCUXDRZUUGBGVG + KZUUDUUCUUDUUEVEZUUGUUAGEFZUXIUUDUPUXCVHBGVIVJVKUUGCGVGKZUUEUUCUUDUUEVL + ZUUGUUBUXKUXLUUEUPUXDVHCGVIVJVKVMUUGUXAUXKUXFUXBUPUXEVHUUHGVIVJVQZUUHVN + VOVRVPUUGUAUHZUWTFZHZUXOUVONZUUGTEUVOVSZUXOTFZUXREFUXPUUGYTUUAUUDUXSYTU + UAUUBUUFVTZUXCUXJADUVOBUVOWAZWBWCZUXTUXPUXOWDWEZTEUXOUVOWFWGRUXQUXOUWBN + ZUUGTEUWBVSZUXTUYEEFUXPUUGYTUUBUUEUYFUYAUXDUXMADUWBCUWBWAZWBWCZUYDTEUXO + UWBWFWGRUXQUXOUIFZAUXOUJJZUXOBOJZPJZLMZUYIUYJUXOCOJZPJZLMZIJZUYIUYJUXOU + UHOJZPJZLMZUXRUYEIJUXOUVANUXQUYIUYQUYTQZUYIWSZUXQUYIHZUYSUYLUYOIJZUYTUY + QVUCUYSUYJUYKUYNWHJZPJVUDVUCUYRVUEUYJPVUCUYIUUAUUDUUBUUEUYRVUEQUXQUYIWI + ZUUGUUAUXPUYIUXCWJZUUGUUDUXPUYIUXJWJZUUGUUBUXPUYIUXDWJZUUGUUEUXPUYIUXMW + JZBCUXOWKWLWMVUCUYJUYKUYNVUCUYJVUCYTUXOEFZUYJEFZUUGYTUXPUYIUYAWJUYIVUKU + XQUXOWNWOAUXOWPVOZRVUCUYIUUBUUEUYNWQFZVUFVUIVUJUXOCWRWTZVUCUYIUUAUUDUYK + WQFZVUFVUGVUHUXOBWRWTZXAXBUYIUYTUYSQUXQUYIUYSLXCWOUYIUYQVUDQUXQUYIUYMUY + LUYPUYOIUYIUYLLXCUYIUYOLXCSWOXDVUBVUAUXQVUBLLIJLUYQUYTXEVUBUYMLUYPLIUYI + UYLLXFUYIUYOLXFSUYIUYSLXFXGWOUXPUYIVUBYJZUUGUXPUXTUYIXIZVURUYDUXOXJZUYI + XHXKWOXLUXQUXRUYMUYEUYPIUXQDUXOUVNUYMTUVOEUYBUUOUXOQZUUPUYIUVMUYLLUUOUX + OUIXMZVVAUUQUYJUVLUYKPUUOUXOAUJXNZUUOUXOBOXOSXPUXPUXTUUGUYDWOZUXQUYIUYL + LEVUCVULVUPUYLEFVUMVUQUYJUYKXQVOUXQVUBHXRZUXQUXTVUSVVDVUTXTZXSYAUXQDUXO + UWAUYPTUWBEUYGVVAUUPUYIUVTUYOLVVBVVAUUQUYJUVSUYNPVVCUUOUXOCOXOSXPVVDUXQ + UYIUYOLEVUCVULVUNUYOEFVUMVUOUYJUYNXQVOVVEVVFXSYASUXQDUXOUUTUYTTUVAEUVAW + AZVVAUUPUYIUUSUYSLVVBVVAUUQUYJUURUYRPVVCUUOUXOUUHOXOSXPVVDUXQUYIUYSLEVU + CVULUYRWQFZUYSEFVUMVUCUYIUXAUXBVVHVUFUUGUXAUXPUYIUXEWJUUGUXBUXPUYIUXNWJ + UXOUUHWRWTUYJUYRXQVOVVEVVFXSYAXDYBUUGUVQUWRUWDUWSIUUGADUVOBCUYAUXCUXDUX + JUXMUYBYCUUGUWDCBIJZUGNZUWCNUWSUUGADUWBCBUYAUXDUXCUXMUXJUYGYCUUGUUNVVJU + WCUUGUUHVVIUGUUGBCUXGUXHYDYEYEYFSYFSUUGYTUXAUXBUWGUVCQUYAUXEUXNADUVAUUH + VVGYGWCUUGUWJUVFUVQIJZUVIUWDIJZIJUWFUUGUWHVVKUWIVVLIUUGYTUUAUUDUWHVVKQU + YAUXCUXJADUVOBUYBYGWCUUGYTUUBUUEUWIVVLQUYAUXDUXMADUWBCUYGYGWCSUUGUVFUVQ + UVIUWDUUGUVFUUGUVEUULLEUULEFUUGYHYIZUUGXRZUUGUVDUUJUUGUUAUXKUVDXIUXCVHB + GYKVJUUGYTUXKUUJXIUYAVHAGYKVJZYLYMRUUGUVQUUGTEUVKUVPUUGUAUBIEUVOLTVRVVN + UUGTEUXOUVOUYCYNVUKUBUHZEFHUXOVVPIJEFUUGUXOVVPYOWOZYPUUGUUAUUDUVKTFUXCU + XJBVNVOYQRUUGUVIUUGUVHUULLEVVMVVNUUGUVGUUJUUGUUBUXKUVGXIUXDVHCGYKVJVVOY + LYMRUUGUWDUUGTEUVRUWCUUGUAUBIEUWBLTVRVVNUUGTEUXOUWBUYHYNVVQYPUUGUUBUUEU + VRTFUXDUXMCVNVOYQRYRXBYS $. $} $( The Legendre symbol is nonzero (and hence equal to ` 1 ` or ` -u 1 ` ) @@ -157684,120 +157780,121 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is ( cz wcel wa cc0 wceq co wne c1 wb c2 adantr syl wbr syl2anc cap cn cdvds cexp vn vk vx vp vy clgs cgcd cif cabs cfv wdc wi 1z zdceq sylancl wn a1i eqnetrd cr ad2antrr cle oveq2 sylan9eqr eqeq1d 3bitr4d lgscl 0z zapne clt - 1ne0 cmul cv cprime cpc simpr iftrued neg1ne0 iffalsed zdclt sylc exmiddc - wo mpjaodan 3adant3 1zzd zcnd nnuz adantl seqf nnabscl ffvelrnd cuz mulcl - nnzd cc prmz ad2antrl dvdsgcdb syl3anc mpbird dvdsabsb mpbid prmnn eleq1w - mpd oveq1 oveq12d ifbieq1d pczcl syl12anc zexpcl eqeltrd fvmptd3 c8 eqtrd - cn0 cmo c7 cmin cdiv caddc simpll1 eldifsn sylanbrc cq oddprm nnnn0d mp1i - zq nnq nngt0 dvdsval3 q0mod 0expd oveq1d dcne sylib ad3antrrr breq1 elrab - zsqcl iffalse necon1aidc iftrue impbid1 zre absresq eqeq12d recnd absge0d - sq1 abscld 1re 0le1 sq11 mpanr12 3bitr2d lgs0 neeq1d gcdid0 w3a cneg cmpt - cseq lgsval4 breq1d simpl dcan2 biantrurd neg1z ifcldcd lgsfcl3 ffvelrnda - eqid zmulcl 3adant1 mulap0bd anbi12d zmulcld 3bitr3d bitr2d gcd2n0cl wrex - eluz2b3 exprmfct sylbir wf elnnuz mul02 mul01 simprr simpl1 simpl2 simprd - biimpri cfz dvdsle eleqtrdi elfz5 simprl simpl3 lgs2 simpld eqbrtrrd cdif - cpr csn lgsval3 1nn 0zd eqtr4d modqexp 0p1e1 oveq1i eqtrdi prmuz2 eluzelz - modqadd1 eluz2gt1 q1mod 1m1e0 pcabs pcelnn eqeltrrd seq3z rexlimdvaa syl5 - 2z 3eqtrd mpand a1d necon1ddc sylbid simp1 simp2 simp3 ifcldadc nprmdvds1 - prmdc simpll2 simplr breq2d bitrd mtbird imnan sylibr con2d imp syl5ibcom - crab notbid 8nn zmodcl mpan2 nn0zd nnzi dcor elprg ad4antr dvdsgcd mpan2d - 7nn dcbid absexpd gcdabs dvds0 syl5ibrcom necon3bd simpll3 rplpwr 3eqtr3d - breq2 sylibd mtod necon3bbid lgsvalmod 3netr4d expclzaplem pceq0 3bitr2rd - necon3i biimpar oveq2d exp0d ax-1cn 1ap0 mpbir2an eqeltrdi dvdsdc adantlr - ad2ant2r mulap0 jca syl2anb simprbi ex impbid 3bitrd 3expa bitr3d ) ACDZB - CDZEZBFGZABUFHZFIZABUGHZJGZKBFIZVXCVXDEZALTHZJGZJFUHZFIZAUIUJZJGZVXFVXHVX - JVXNVXLVXOLTHZJLTHZGZVXPVXCVXNVXLKVXDVXCVXNVXLVXCVXLUKZVXNVXLULVXCVXKCDZJ - CDZVXTVXAVYAVXBAUUAMUMVXKJUNUOVXLVXMFVXLUPVXMFGULVXTVXLJFUUBUQUUCNVXLVXMJ - FVXLJFUUDJFIZVXLVJUQURUUEMVXJVXQVXKVXRJVXJAUSDZVXQVXKGVXAVYDVXBVXDAUUFUTZ - AUUGNVXRJGVXJUUKUQUUHVXJVXOUSDZFVXOVAOZVXSVXPKZVXJAVXJAVYEUUIZUULVXJAVYIU - UJVYFVYGEJUSDFJVAOVYHUUMUUNVXOJUUOUUPPUUQVXJVXEVXMFVXDVXCVXEAFUFHZVXMBFAU - FVBVXAVYJVXMGVXBAUURMVCUUSVXJVXGVXOJVXDVXCVXGAFUGHZVXOBFAUGVBVXAVYKVXOGVX - BAUUTMVCVDVEVXCVXIEZVXEFQOZVXFVXHVYLVXECDZFCDZVYMVXFKVXCVYNVXIABVFMVGVXEF - VHUOVXAVXBVXIVYMVXHKVXAVXBVXIUVAZVYMBFVIOZAFVIOZEZJUVBZJUHZBUIUJZVKUARUAV - LZVMDZAWUCUFHZWUCBVNHZTHZJUHZUVCZJUVDZUJZVKHZFQOZWUKFQOZVXHVYPVXEWULFQAUA - WUIBWUIUVNZUVEUVFVYPWULFIZWUKFIZWUMWUNVYPWUQWUAFIZWUQEZWUPVXAVXBWUQWUSKVX - IVXCWURWUQVXCVYSWURVYSUPZVXCVYSEZWUAVYTFWVAVYSVYTJVXCVYSVOVPVYTFIZWVAVQUQ - URVXCWUTEZWUAJFWVCVYSVYTJVXCWUTVOVRVYCWVCVJUQURVXCVYSUKZVYSWUTWBVXCVYQUKZ - VYRUKZWVDVXCVXBVYOWVEVXAVXBVOZVGBFVSUOVXCVXAVYOWVFVXAVXBUVGVGAFVSUOVYQVYR - UVHVTZVYSWANWCUVIWDVYPWUAFQOZWUNEWUMWUSWUPVYPWUAWUKVYPWUAVXAVXBWUACDZVXIV - XCVYSVYTJCVYTCDVXCUVJUQVXCWEWVHUVKWDZWFVYPWUKVYPRCWUBWUJVYPUBUCVKCWUIJRWG - VYPWEVYPRCUBVLZWUIAUAWUIBWUOUVLZUVMWVLCDZUCVLZCDEWVLWVOVKHZCDVYPWVLWVOUVO - WHWIVXBVXIWUBRDZVXABWJZUVPZWKZWFUVQVYPWVIWURWUNWUQVYPWVJVYOWVIWURKWVKVGWU - AFVHUOVYPWUKCDVYOWUNWUQKWVTVGWUKFVHUOZUVRVYPWULCDVYOWUMWUPKVYPWUAWUKWVKWV - TUVSVGWULFVHUOZUVTUWAWWBWWAVEVYPWUNVXHVYPWUNWUQVXHWWAVYPVXHUKZWUQVXHULVYP - VXGCDVYBWWCVYPVXGABUWBZWNUMVXGJUNUOVYPVXGJWUKFVYPVXGJIZWUKFGZULWWCVYPVXGR - DZWWEWWFWWDWWGWWEEZUDVLZVXGSOZUDVMUWCZVYPWWFWWHVXGLWLUJZDWWKVXGUWDVXGUDUW - EUWFVYPWWJWWFUDVMVYPWWIVMDZWWJEZEZUBUCVKWOWUIWWIJWUBFWVLWODZWVOWODEWVPWOD - WWOWVLWVOWMWHWWOWVLJWLUJZDZEZWVLWUIUJZWWSRCWVLWUIVYPRCWUIUWGWWNWWRWVMUTWW - RWVLRDZWWOWXAWWRWVLUWHUWOWHWKWFWWPFWVLVKHFGWWOWVLUWIWHWWPWVLFVKHFGWWOWVLU - WJWHWWOWWIJWUBUWPHDZWWIWUBVAOZWWOWWIWUBSOZWXCWWOWWIBSOZWXDWWOWWIASOZWXEWW - OWXFWXEEZWWJVYPWWMWWJUWKWWOWWICDZVXAVXBWXGWWJKWWMWXHVYPWWJWWIWPWQZVXAVXBV - XIWWNUWLZVXAVXBVXIWWNUWMZWWIABWRWSWTZUWNWWOWXHVXBWXEWXDKWXIWXKWWIBXAPXBZW - WOWXHWVQWXDWXCULWXIVYPWVQWWNWVSMZWWIWUBUWQPXEWWOWWIWWQDWUBCDWXBWXCKWWOWWI - RWWQWWMWWIRDZVYPWWJWWIXCZWQZWGUWRWWOWUBWXNWNWWIJWUBUWSPWTWWOWWIWUIUJWWMAW - WIUFHZWWIBVNHZTHZJUHZWXTFWWOUAWWIWUHWYARWUICWUOWUCWWIGZWUDWWMWUGWXTJUAUDV - MXDWYBWUEWXRWUFWXSTWUCWWIAUFVBWUCWWIBVNXFXGXHWXQWWOWYAWXTCWWOWWMWXTJVYPWW - MWWJUWTZVPZWWOWXRCDZWXSXPDZWXTCDWWOVXAWXHWYEWXJWXIAWWIVFPWWOWWMVXBVXIWYFW - YCWXKVXAVXBVXIWWNUXAWWIBXIXJWXRWXSXKPXLXMWYDWWOWXTFWXSTHFWWOWXRFWXSTWWOWW - ILGZWXRFGWWILIZWWOWYGEZWXRLASOZFAXNXQHZJXRUXFDZJVYTUHZUHZFWYGWWOWXRALUFHZ - WYNWWILAUFVBWWOVXAWYOWYNGZWXJAUXBZNVCWYIWYJFWYMWYIWWILASWWOWYGVOWWOWXFWYG - WWOWXFWXEWXLUXCZMUXDVPXOWWOWYHEZWXRAWWIJXSHLXTHZTHZJYAHWWIXQHZJXSHZFWYSVX - AWWIVMLUXGUXEZDZWXRXUCGVXAVXBVXIWWNWYHYBZWYSWWMWYHXUEWWOWWMWYHWYCMZWWOWYH - VOWWIVMLYCYDZAWWIUXHPWYSXUCJJXSHFWYSXUBJJXSWYSXUBJWWIXQHZJWYSXUBFJYAHZWWI - XQHXUIWYSXUAFJWWIWYSXUACDZXUAYEDWYSVXAWYTXPDXUKXUFWYSWYTWYSXUEWYTRDXUHWWI - YFNZYGZAWYTXKPXUAYINVYOFYEDWYSVGFYIYHJRDJYEDWYSUXIJYJYHWYSWXOWWIYEDZWYSWW - MWXOXUGWXPNZWWIYJZNZWYSWXOFWWIVIOZXUOWWIYKZNZWYSXUAWWIXQHFWYTTHZWWIXQHFWW - IXQHZWYSAFWYTWWIXUFWYSUXJXUMXUQXUTWYSAWWIXQHZFXVBWYSWXFXVCFGZWWOWXFWYHWYR - MWYSWXOVXAWXFXVDKXUOXUFWWIAYLPXBWYSWXOXVBFGZXUOWXOXUNXURXVEXUPXUSWWIYMPNU - XKUXLWYSXVAFWWIXQWYSWYTXULYNYOXOUXRXUJJWWIXQUXMUXNUXOWYSWWIWWLDZXUIJGZWYS - WWMXVFXUGWWIUXPNXVFXUNJWWIVIOXVGXVFWXHXUNLWWIUXQWWIYINWWIUXSWWIUXTPNXOYOU - YAUXOXOWWOWYGUKZWYGWYHWBWWOWXHLCDZXVHWXIUYHWWILUNUOWWILYPYQWCYOWWOWXSWWOW - WIWUBVNHZWXSRWWOWWMBYEDZXVJWXSGWYCWWOVXBXVKWXKBYIZNBWWIUYBPWWOXVJRDZWXDWX - MWWOWWMWVQXVMWXDKWYCWXNWWIWUBUYCPWTUYDYNXOUYIUYEUYFUYGUYJUYKUYLXEUYMVYPVX - HWUNVYPVXHEZWUKWVOFQOZUCWOVUJZDZWUNXVNRXVPWUBWUJXVNUBUEVKXVPWUIJRWGXVNWEX - VNWXAEZWWTWVLVMDZAWVLUFHZWVLBVNHZTHZJUHZXVPXVRUAWVLWUHXWCRWUICWUOWUCWVLGZ - WUDXVSWUGXWBJUAUBVMXDXWDWUEXVTWUFXWATWUCWVLAUFVBWUCWVLBVNXFXGXHXVNWXAVOXV - RXVSXWBJCXVRXVSEZXVTCDZXWAXPDZXWBCDXWEVXAWVNXWFVYPVXAVXHWXAXVSVXAVXBVXIUY - NZYRXVSWVNXVRWVLWPZWHAWVLVFZPXWEXVSVXBVXIXWGXVRXVSVOVYPVXBVXHWXAXVSVXAVXB - VXIUYOYRVYPVXIVXHWXAXVSVXAVXBVXIUYPYRWVLBXIZXJXVTXWAXKPXVRXVSUPEZWEWXAXVS - UKXVNWVLUYSWHZUYQXMXVRXVSXWBJXVPXVNXVSXWBXVPDZWXAXVNXVSEZWVLBSOZXWNXWPUPZ - XWOXWPEZXVTWODZXVTFQOZXWACDZXWNXWOXWSXWPXWOXVTXWOVXAWVNXWFVXAVXBVXIVXHXVS - YBZXVSWVNXVNXWIWHZXWJPZWFZMXWRXWTXVTFIZXWRWVLLGZXXFWVLLIZXWRXXGEZXVTWYMFX - XIXVTWYNWYMXXGXWRXVTWYOWYNWVLLAUFVBXWRVXAWYPXWOVXAXWPXXBMZWYQNVCXXIWYJFWY - MXWRXXGWYJUPZXWRWVLASOZUPZXXGXXKXWOXWPXXMXWOXXLXWPXWOXXLXWPEZUPXXLXWQULXW - OXXNWVLJSOZXVSXXOUPZXVNWVLUYRZWHXWOXXNWVLVXGSOZXXOXWOWVNVXAVXBXXNXXRKXXCX - XBVXAVXBVXIVXHXVSUYTZWVLABWRWSXWOVXGJWVLSVYPVXHXVSVUAZVUBVUCVUDXXLXWPVUEV - UFVUGVUHZXXGXXLWYJWVLLASYSVUKVUIVUHVRXOVYPWYMFIZVXHXVSXWPXXGVYPVXAXYBXWHV - XAWYLXYBWYLUPZVXAWYLEZWYMJFXYDWYLJVYTVXAWYLVOVPVYCXYDVJUQURVXAXYCEZWYMVYT - FXYEWYLJVYTVXAXYCVOVRWVBXYEVQUQURVXAWYLUKZWYLXYCWBVXAXYFWYKJGZWYKXRGZWBZU - KZVXAXYGUKZXYHUKZXYJVXAWYKCDZVYBXYKVXAWYKVXAXNRDWYKXPDZVULAXNVUMVUNZVUOZU - MWYKJUNUOVXAXYMXRCDXYLXYPXRVVBVUPWYKXRUNUOXYGXYHVUQVTVXAWYLXYIVXAXYNWYLXY - IKXYOWYKJXRXPVURNVVCWTWYLWANWCNVUSURXWRXXHEZXVTWVLXQHZFWVLXQHZIXXFXYQAWVL - JXSHLXTHZTHZWVLXQHZFXYRXYSXYQWVLYUASOZUPYUBFIXYQYUCXXOXYQXVSXXPXWOXVSXWPX - XHXVNXVSVOZUTZXXQNXYQYUCWVLYUABUGHZSOZXXOXYQYUCXWPYUGXWOXWPXXHVUAXYQWVNYU - ACDZVXBYUCXWPEYUGULXYQXVSWVNYUEXWINZXYQVXAXYTXPDYUHXWRVXAXXHXXJMZXYQXYTXY - QWVLXUDDZXYTRDZXYQXVSXXHYUKYUEXWRXXHVOWVLVMLYCYDZWVLYFNZYGZAXYTXKPZXWOVXB - XWPXXHXXSUTZWVLYUABVUTWSVVAXYQYUFJWVLSXYQYUAUIUJZWUBUGHZVXOXYTTHZWUBUGHZY - UFJXYQYURYUTWUBUGXYQAXYTXYQAYUJWFYUOVVDYOXYQYUHVXBYUSYUFGYUPYUQYUABVVEPXY - QVXOWUBUGHZJGZYVAJGZXYQYVBVXGJXYQVXAVXBYVBVXGGYUJYUQABVVEPXWOVXHXWPXXHXXT - UTXOXYQVXORDZWVQYULYVCYVDULXYQVXAAFIZYVEYUJXYQXXMYVFXWRXXMXXHXYAMXYQXXLAF - XYQXXLAFGWVLFSOZXYQWVNYVGYUIWVLVVFNAFWVLSVVLVVGVVHXEAWJPXWOWVQXWPXXHXWOVX - BVXIWVQXXSVXAVXBVXIVXHXVSVVIZWVRPZUTYUNVXOWUBXYTVVJWSXEVVKVUBVVMVVNXYQYUC - YUBFXYQWXAYUHYUCYUBFGKXWOWXAXWPXXHXVSWXAXVNWVLXCWHZUTZYUPWVLYUAYLPVVOXBXY - QVXAYUKXYRYUBGYUJYUMAWVLVVPPXYQWXAXYSFGZYVKWXAWVLYEDFWVLVIOYVLWVLYJWVLYKW - VLYMPNVVQXVTFXYRXYSXVTFWVLXQXFVWANXWRXXGUKZXXGXXHWBXWRWVNXVIYVMXWOWVNXWPX - XCMUYHWVLLUNUOWVLLYPYQWCXWRXWFVYOXWTXXFKXWOXWFXWPXXDMVGXVTFVHUOWTXWOXXAXW - PXWOXWAXWOXVSVXBVXIXWGYUDXXSYVHXWKXJVUOMUCXVTXWAVVRWSXWOXWQEZXWBJXVPYVNXW - BXVTFTHJYVNXWAFXVTTXWOXWAFGZXWQXWOXWQWVLWUBSOZUPZWVLWUBVNHZFGZYVOXWOXWPYV - PXWOWVNVXBXWPYVPKXXCXXSWVLBXAPVUKXWOXVSWVQYVSYVQKYUDYVIWVLWUBVVSPXWOYVRXW - AFXWOXVSXVKYVRXWAGYUDXWOVXBXVKXXSXVLNBWVLUYBPVDVVTVWBVWCYVNXVTXWOXWSXWQXX - EMVWDXOJXVPDZJWODJFQOZVWEVWFXVOYWAUCJWOWVOJFQYSYTVWGZVWHXWOXWPUKZXWPXWQWB - XWOWXAVXBYWCYVJXXSWVLBVWIPXWPWANWCVWJYVTXWLYWBUQXWMUYQXLWVLXVPDZUEVLZXVPD - ZEZWVLYWEVKHZXVPDZXVNYWGYWHWODZYWHFQOZEZYWIYWDWWPWVLFQOZEZYWEWODZYWEFQOZE - ZYWLYWFXVOYWMUCWVLWOWVOWVLFQYSYTXVOYWPUCYWEWOWVOYWEFQYSYTYWNYWQEYWJYWKWWP - YWOYWJYWMYWPWVLYWEWMVWKWVLYWEVWLVWMVWNXVOYWKUCYWHWOWVOYWHFQYSYTVUFWHWIVYP - WVQVXHWVSMWKXVQWUKWODWUNXVOWUNUCWUKWOWVOWUKFQYSYTVWONVWPVWQVWRVWSVWTVXCVX - DUKZVXDVXIWBVXCVXBVYOYWRWVGVGBFUNUOBFYPYQWC $. + 1ne0 cmul cv cprime simpr iftrued neg1ne0 iffalsed zdclt exmiddc mpjaodan + cpc wo 3adant3 1zzd zcnd nnuz adantl seqf nnabscl ffvelrnd nnzd cuz mulcl + cc prmz ad2antrl dvdsgcdb syl3anc mpbird dvdsabsb mpbid prmnn eleq1 oveq1 + mpd oveq12d ifbieq1d cn0 pczcl syl12anc zexpcl eqeltrd fvmptd3 c8 c7 cmin + cmo eqtrd cdiv caddc simpll1 eldifsn sylanbrc oddprm nnnn0d mp1i nnq 3syl + cq nngt0 dvdsval3 q0mod oveq1d dcne sylib ad3antrrr breq1 ad3antlr elrab + zq zsqcl iffalse necon1aidc iftrue impbid1 zre absresq sq1 eqeq12d abscld + recnd absge0d 0le1 sq11 mpanr12 3bitr2d lgs0 neeq1d gcdid0 cneg cmpt cseq + 1re w3a eqid lgsval4 breq1d simpl dcand biantrurd neg1z ifcldcd ffvelrnda + lgsfcl3 zmulcl 3adant1 mulap0bd anbi12d zmulcld 3bitr3d gcd2n0cl exprmfct + bitr2d wrex eluz2b3 sylbir wf elnnuz mul02 mul01 cfz simprr simpl1 simpl2 + biimpri simprd dvdsle eleqtrdi simprl simpl3 cpr lgs2 simpld eqbrtrrd csn + elfz5 cdif simplrl lgsval3 1nn eqtr4d modqexp 0expd modqadd1 0p1e1 oveq1i + eqtrdi prmuz2 eluzelz eluz2gt1 q1mod 1m1e0 2z pcabs pcelnn eqeltrrd seq3z + 0zd 3eqtrd rexlimdvaa syl5 mpand necon1ddc sylbid simp1 simp2 simp3 prmdc + a1d crab ifcldadc nprmdvds1 simplr breq2d bitrd mtbird imnan sylibr con2d + simpll2 imp notbid syl5ibcom 8nn zmodcl mpan2 nn0zd nnzi dcor elprg dcbid + sylc 3ad2ant1 ad4antr simpllr dvdsgcd mpan2d absexpd gcdabs simp-4r dvds0 + 7nn breq2 syl5ibrcom necon3bd simpll3 rplpwr 3eqtr3d necon3bbid lgsvalmod + sylibd mtod 3netr4d necon3i ad2antlr expclzaplem syl2an2 3bitr2rd biimpar + pceq0 oveq2d ax-1cn 1ap0 mpbir2an eqeltrdi dvdsdc adantlr ad2ant2r mulap0 + exp0d jca syl2anb simprbi ex impbid 3bitrd 3expa bitr3d ) ACDZBCDZEZBFGZA + BUFHZFIZABUGHZJGZKBFIZVXKVXLEZALTHZJGZJFUHZFIZAUIUJZJGZVXNVXPVXRVYBVXTVYC + LTHZJLTHZGZVYDVXKVYBVXTKVXLVXKVYBVXTVXKVXTUKZVYBVXTULVXKVXSCDZJCDZVYHVXIV + YIVXJAUUAMUMVXSJUNUOVXTVYAFVXTUPVYAFGULVYHVXTJFUUBUQUUCNVXTVYAJFVXTJFUUDJ + FIZVXTVJUQURUUEMVXRVYEVXSVYFJVXRAUSDZVYEVXSGVXIVYLVXJVXLAUUFUTZAUUGNVYFJG + VXRUUHUQUUIVXRVYCUSDZFVYCVAOZVYGVYDKZVXRAVXRAVYMUUKZUUJVXRAVYQUULVYNVYOEJ + USDFJVAOVYPUVCUUMVYCJUUNUUOPUUPVXRVXMVYAFVXLVXKVXMAFUFHZVYABFAUFVBVXIVYRV + YAGVXJAUUQMVCUURVXRVXOVYCJVXLVXKVXOAFUGHZVYCBFAUGVBVXIVYSVYCGVXJAUUSMVCVD + VEVXKVXQEZVXMFQOZVXNVXPVYTVXMCDZFCDZWUAVXNKVXKWUBVXQABVFMVGVXMFVHUOVXIVXJ + VXQWUAVXPKVXIVXJVXQUVDZWUABFVIOZAFVIOZEZJUUTZJUHZBUIUJZVKUARUAVLZVMDZAWUK + UFHZWUKBWAHZTHZJUHZUVAZJUVBZUJZVKHZFQOZWUSFQOZVXPWUDVXMWUTFQAUAWUQBWUQUVE + ZUVFUVGWUDWUTFIZWUSFIZWVAWVBWUDWVEWUIFIZWVEEZWVDVXIVXJWVEWVGKVXQVXKWVFWVE + VXKWUGWVFWUGUPZVXKWUGEZWUIWUHFWVIWUGWUHJVXKWUGVNVOWUHFIZWVIVPUQURVXKWVHEZ + WUIJFWVKWUGWUHJVXKWVHVNVQVYKWVKVJUQURVXKWUGUKWUGWVHWBVXKWUEWUFVXKVXJWUCWU + EUKVXIVXJVNZVGBFVRUOVXKVXIWUCWUFUKVXIVXJUVHVGAFVRUOUVIZWUGVSNVTUVJWCWUDWU + IFQOZWVBEWVAWVGWVDWUDWUIWUSWUDWUIVXIVXJWUICDZVXQVXKWUGWUHJCWUHCDVXKUVKUQV + XKWDWVMUVLWCZWEWUDWUSWUDRCWUJWURWUDUBUCVKCWUQJRWFWUDWDWUDRCUBVLZWUQAUAWUQ + BWVCUVNZUVMWVQCDZUCVLZCDEWVQWVTVKHZCDWUDWVQWVTUVOWGWHVXJVXQWUJRDZVXIBWIZU + VPZWJZWEUVQWUDWVNWVFWVBWVEWUDWVOWUCWVNWVFKWVPVGWUIFVHUOWUDWUSCDWUCWVBWVEK + WWEVGWUSFVHUOZUVRWUDWUTCDWUCWVAWVDKWUDWUIWUSWVPWWEUVSVGWUTFVHUOZUVTUWCWWG + WWFVEWUDWVBVXPWUDWVBWVEVXPWWFWUDVXPUKZWVEVXPULWUDVXOCDVYJWWHWUDVXOABUWAZW + KUMVXOJUNUOWUDVXOJWUSFWUDVXOJIZWUSFGZULWWHWUDVXORDZWWJWWKWWIWWLWWJEZUDVLZ + VXOSOZUDVMUWDZWUDWWKWWMVXOLWLUJZDWWPVXOUWEVXOUDUWBUWFWUDWWOWWKUDVMWUDWWNV + MDZWWOEZEZUBUCVKWNWUQWWNJWUJFWVQWNDZWVTWNDEWWAWNDWWTWVQWVTWMWGWWTWVQJWLUJ + ZDZEZWVQWUQUJZWXDRCWVQWUQWUDRCWUQUWGWWSWXCWVRUTWXCWVQRDZWWTWXFWXCWVQUWHUW + OWGWJWEWXAFWVQVKHFGWWTWVQUWIWGWXAWVQFVKHFGWWTWVQUWJWGWWTWWNJWUJUWKHDZWWNW + UJVAOZWWTWWNWUJSOZWXHWWTWWNBSOZWXIWWTWWNASOZWXJWWTWXKWXJEZWWOWUDWWRWWOUWL + WWTWWNCDZVXIVXJWXLWWOKWWRWXMWUDWWOWWNWOWPZVXIVXJVXQWWSUWMZVXIVXJVXQWWSUWN + ZWWNABWQWRWSZUWPWWTWXMVXJWXJWXIKWXNWXPWWNBWTPXAZWWTWXMWWBWXIWXHULWXNWUDWW + BWWSWWDMZWWNWUJUWQPXEWWTWWNWXBDWUJCDWXGWXHKWWTWWNRWXBWWRWWNRDZWUDWWOWWNXB + ZWPZWFUWRWWTWUJWXSWKWWNJWUJUXFPWSWWTWWNWUQUJWWRAWWNUFHZWWNBWAHZTHZJUHZWYE + FWWTUAWWNWUPWYFRWUQCWVCWUKWWNGZWULWWRWUOWYEJWUKWWNVMXCWYGWUMWYCWUNWYDTWUK + WWNAUFVBWUKWWNBWAXDXFXGWYBWWTWYFWYECWWTWWRWYEJWUDWWRWWOUWSZVOZWWTWYCCDZWY + DXHDZWYECDWWTVXIWXMWYJWXOWXNAWWNVFPWWTWWRVXJVXQWYKWYHWXPVXIVXJVXQWWSUWTWW + NBXIXJWYCWYDXKPXLXMWYIWWTWYEFWYDTHFWWTWYCFWYDTWWTWWNLGZWYCFGWWNLIZWWTWYLE + ZWYCLASOZFAXNXQHZJXOUXADZJWUHUHZUHZFWYLWWTWYCALUFHZWYSWWNLAUFVBWWTVXIWYTW + YSGZWXOAUXBZNVCWYNWYOFWYRWYNWWNLASWWTWYLVNWWTWXKWYLWWTWXKWXJWXQUXCZMUXDVO + XRWWTWYMEZWYCAWWNJXPHLXSHZTHZJXTHWWNXQHZJXPHZFXUDVXIWWNVMLUXEUXGZDZWYCXUH + GVXIVXJVXQWWSWYMYAZXUDWWRWYMXUJWUDWWRWWOWYMUXHZWWTWYMVNWWNVMLYBYCZAWWNUXI + PXUDXUHJJXPHFXUDXUGJJXPXUDXUGJWWNXQHZJXUDXUGFJXTHZWWNXQHXUNXUDXUFFJWWNXUD + XUFCDZXUFYIDXUDVXIXUEXHDXUPXUKXUDXUEXUDXUJXUERDXUMWWNYDNZYEZAXUEXKPXUFYTN + WUCFYIDXUDVGFYTYFJRDJYIDXUDUXJJYGYFXUDWWRWXTWWNYIDZXULWYAWWNYGZYHZXUDWWRW + XTFWWNVIOZXULWYAWWNYJZYHZXUDXUFWWNXQHFXUETHZWWNXQHFWWNXQHZXUDAFXUEWWNXUKX + UDUYHXURXVAXVDXUDAWWNXQHZFXVFXUDWXKXVGFGZWWTWXKWYMXUCMXUDWXTVXIWXKXVHKXUD + WWRWXTXULWYANXUKWWNAYKPXAXUDWWRWXTXVFFGZXULWYAWXTXUSXVBXVIXUTXVCWWNYLPYHU + XKUXLXUDXVEFWWNXQXUDXUEXUQUXMYMXRUXNXUOJWWNXQUXOUXPUXQXUDWWRWWNWWQDZXUNJG + ZXULWWNUXRXVJXUSJWWNVIOXVKXVJWXMXUSLWWNUXSWWNYTNWWNUXTWWNUYAPYHXRYMUYBUXQ + XRWWTWYLUKZWYLWYMWBWWTWXMLCDZXVLWXNUYCWWNLUNUOWWNLYNYOVTYMWWTWYDWWTWWNWUJ + WAHZWYDRWWTWWRBYIDZXVNWYDGWYHWWTVXJXVOWXPBYTZNBWWNUYDPWWTXVNRDZWXIWXRWWTW + WRWWBXVQWXIKWYHWXSWWNWUJUYEPWSUYFUXMXRUYIUYGUYJUYKUYLUYSUYMXEUYNWUDVXPWVB + WUDVXPEZWUSWVTFQOZUCWNUYTZDZWVBXVRRXVTWUJWURXVRUBUEVKXVTWUQJRWFXVRWDXVRWX + FEZWXEWVQVMDZAWVQUFHZWVQBWAHZTHZJUHZXVTXWBUAWVQWUPXWGRWUQCWVCWUKWVQGZWULX + WCWUOXWFJWUKWVQVMXCXWHWUMXWDWUNXWETWUKWVQAUFVBWUKWVQBWAXDXFXGXVRWXFVNXWBX + WCXWFJCXWBXWCEZXWDCDZXWEXHDZXWFCDXWIVXIWVSXWJWUDVXIVXPWXFXWCVXIVXJVXQUYOY + PXWCWVSXWBWVQWOZWGAWVQVFZPXWIXWCVXJVXQXWKXWBXWCVNWUDVXJVXPWXFXWCVXIVXJVXQ + UYPYPWUDVXQVXPWXFXWCVXIVXJVXQUYQYPWVQBXIZXJXWDXWEXKPXWBXWCUPEZWDWXFXWCUKX + VRWVQUYRWGZVUAXMXWBXWCXWFJXVTXVRXWCXWFXVTDZWXFXVRXWCEZWVQBSOZXWQXWSUPZXWR + XWSEZXWDWNDZXWDFQOZXWECDZXWQXWRXXBXWSXWRXWDXWRVXIWVSXWJVXIVXJVXQVXPXWCYAZ + XWCWVSXVRXWLWGZXWMPZWEZMXXAXXCXWDFIZXXAWVQLGZXXIWVQLIZXXAXXJEZXWDWYRFXXLX + WDWYSWYRXXJXXAXWDWYTWYSWVQLAUFVBXXAVXIXUAXWRVXIXWSXXEMXUBNVCXXLWYOFWYRXXA + XXJWYOUPZXXAWVQASOZUPZXXJXXMXWRXWSXXOXWRXXNXWSXWRXXNXWSEZUPXXNXWTULXWRXXP + WVQJSOZXWCXXQUPZXVRWVQVUBZWGXWRXXPWVQVXOSOZXXQXWRWVSVXIVXJXXPXXTKXXFXXEVX + IVXJVXQVXPXWCVUJZWVQABWQWRXWRVXOJWVQSWUDVXPXWCVUCVUDVUEVUFXXNXWSVUGVUHVUI + VUKZXXJXXNWYOWVQLASYQVULVUMVUKVQXRWUDWYRFIZVXPXWCXWSXXJVXIVXJXYCVXQVXIWYQ + XYCWYQUPZVXIWYQEZWYRJFXYEWYQJWUHVXIWYQVNVOVYKXYEVJUQURVXIXYDEZWYRWUHFXYFW + YQJWUHVXIXYDVNVQWVJXYFVPUQURVXIWYQUKZWYQXYDWBVXIXYGWYPJGZWYPXOGZWBZUKZVXI + XYHUKZXYIUKZXYKVXIWYPCDZVYJXYLVXIWYPVXIXNRDWYPXHDZVUNAXNVUOVUPZVUQZUMWYPJ + UNUOVXIXYNXOCDXYMXYQXOVVLVURWYPXOUNUOXYHXYIVUSVVBVXIWYQXYJVXIXYOWYQXYJKXY + PWYPJXOXHVUTNVVAWSWYQVSNVTVVCVVDURXXAXXKEZXWDWVQXQHZFWVQXQHZIXXIXYRAWVQJX + PHLXSHZTHZWVQXQHZFXYSXYTXYRWVQYUBSOZUPYUCFIXYRYUDXXQXWCXXRXVRXWSXXKXXSYRX + YRYUDWVQYUBBUGHZSOZXXQXYRYUDXWSYUFXWRXWSXXKVUCXYRWVSYUBCDZVXJYUDXWSEYUFUL + XWCWVSXVRXWSXXKXWLYRXYRVXIYUAXHDYUGXWRVXIXWSXXKXXEUTZXYRYUAXYRWVQXUIDZYUA + RDZXYRXWCXXKYUIXVRXWCXWSXXKVVEZXXAXXKVNWVQVMLYBYCZWVQYDNZYEZAYUAXKPZXWRVX + JXWSXXKXYAUTZWVQYUBBVVFWRVVGXYRYUEJWVQSXYRYUBUIUJZWUJUGHZVYCYUATHZWUJUGHZ + YUEJXYRYUQYUSWUJUGXYRAYUAXYRAYUHWEYUNVVHYMXYRYUGVXJYURYUEGYUOYUPYUBBVVIPX + YRVYCWUJUGHZJGZYUTJGZXYRYVAVXOJXYRVXIVXJYVAVXOGYUHYUPABVVIPWUDVXPXWCXWSXX + KVVJXRXYRVYCRDZWWBYUJYVBYVCULXYRVXIAFIZYVDYUHXYRXXOYVEXXAXXOXXKXYBMXYRXXN + AFXYRXXNAFGWVQFSOZXYRXWCWVSYVFYUKXWLWVQVVKYHAFWVQSVVMVVNVVOXEAWIPXWRWWBXW + SXXKXWRVXJVXQWWBXYAVXIVXJVXQVXPXWCVVPZWWCPZUTYUMVYCWUJYUAVVQWRXEVVRVUDVWA + VWBXYRYUDYUCFXYRWXFYUGYUDYUCFGKXWCWXFXVRXWSXXKWVQXBZYRZYUOWVQYUBYKPVVSXAX + YRVXIYUIXYSYUCGYUHYULAWVQVVTPXYRWXFXYTFGZYVJWXFWVQYIDFWVQVIOYVKWVQYGWVQYJ + WVQYLPNVWCXWDFXYSXYTXWDFWVQXQXDVWDNXXAXXJUKZXXJXXKWBXXAWVSXVMYVLXWCWVSXVR + XWSXWLVWEUYCWVQLUNUOWVQLYNYOVTXXAXWJWUCXXCXXIKXWRXWJXWSXXGMVGXWDFVHUOWSXW + RXXDXWSXWRXWEXWRXWCVXJVXQXWKXVRXWCVNZXYAYVGXWNXJVUQMUCXWDXWEVWFWRXWRXWTEZ + XWFJXVTYVNXWFXWDFTHJYVNXWEFXWDTXWRXWEFGZXWTXWRXWTWVQWUJSOZUPZWVQWUJWAHZFG + ZYVOXWRXWSYVPXWCWVSXVRVXJXWSYVPKXWLXYAWVQBWTVWGVULXWRXWCWWBYVSYVQKYVMYVHW + VQWUJVWJPXWRYVRXWEFXWRXWCXVOYVRXWEGYVMXWRVXJXVOXYAXVPNBWVQUYDPVDVWHVWIVWK + YVNXWDXWRXXBXWTXXHMVWTXRJXVTDZJWNDJFQOZVWLVWMXVSYWAUCJWNWVTJFQYQYSVWNZVWO + XWRXWSUKZXWSXWTWBXWCWXFXVRVXJYWCYVIXYAWVQBVWPVWGXWSVSNVTVWQYVTXWOYWBUQXWP + VUAXLWVQXVTDZUEVLZXVTDZEZWVQYWEVKHZXVTDZXVRYWGYWHWNDZYWHFQOZEZYWIYWDWXAWV + QFQOZEZYWEWNDZYWEFQOZEZYWLYWFXVSYWMUCWVQWNWVTWVQFQYQYSXVSYWPUCYWEWNWVTYWE + FQYQYSYWNYWQEYWJYWKWXAYWOYWJYWMYWPWVQYWEWMVWRWVQYWEVWSVXAVXBXVSYWKUCYWHWN + WVTYWHFQYQYSVUHWGWHWUDWWBVXPWWDMWJXWAWUSWNDWVBXVSWVBUCWUSWNWVTWUSFQYQYSVX + CNVXDVXEVXFVXGVXHVXKVXLUKZVXLVXQWBVXKVXJWUCYWRWVLVGBFUNUOBFYNYOVT $. $( The Legendre symbol is nonzero (and hence equal to ` 1 ` or ` -u 1 ` ) precisely when the arguments are coprime. (Contributed by Mario @@ -163453,20 +163550,20 @@ a singleton (where the latter can also be thought of as representing ( Q ` ( i e. _om |-> if ( i e. k , 1o , (/) ) ) ) = 1o ) $= ( com wcel c2o xnninf cv c1o c0 wceq csuc wral wdc wi suceq raleqdv dcbid imbi2d vw cmap cif cmpt cfv elmapi peano1 nnnninf mp1i ffvelrnd 2onn elnn - vj co sylancl 1onn nndceq csn suc0 raleqi 0ex eleq2 ifbid mpteq2dv fveq2d - eqeq1d ralsn bitri dcbii sylibr wa cun wf adantl peano2 adantr syl ralsng - wb mpbird dcan2 mpan9 ralunb df-suc exp31 a2d finds impcom ) DEFAGHUBUNFZ - BEBIZCIZFZJKUCZUDZAUEZJLZCDMZNZOZWIWPCUAIZMZNZOZPWIWPCKMZNZOZPWIWPCUMIZMZ - NZOZPWIWPCXHMZNZOZPWIWSPUAUMDWTKLZXCXFWIXNXBXEXNWPCXAXDWTKQRSTWTXGLZXCXJW - IXOXBXIXOWPCXAXHWTXGQRSTWTXHLZXCXMWIXPXBXLXPWPCXAXKWTXHQRSTWTDLZXCWSWIXQX - BWRXQWPCXAWQWTDQRSTWIBEWJKFZJKUCZUDZAUEZJLZOZXFWIYAEFZJEFZYCWIYAGFGEFZYDW - IHGXTAAGHUFZKEFXTHFWIUGBKUHUIUJUKYAGULUOUPYAJUQUOXEYBXEWPCKURZNYBWPCXDYHU - SUTWPYBCKVAWKKLZWOYAJYIWNXTAYIBEWMXSYIWLXRJKWKKWJVBVCVDVEVFVGVHVIVJXGEFZW - IXJXMYJWIXJXMYJWIVKZXJVKZWPCXHXHURZVLZNZOZXMYLXIWPCYMNZVKZOZYPYKYQOZXJYSY - KYTBEWJXHFZJKUCZUDZAUEZJLZOZYKUUDEFZYEUUFYKUUDGFYFUUGYKHGUUCAWIHGAVMYJYGV - NYKXHEFZUUCHFYJUUHWIXGVOVPZBXHUHVQUJUKUUDGULUOUPUUDJUQUOYKYQUUEYKUUHYQUUE - VSUUIWPUUECXHEWKXHLZWOUUDJUUJWNUUCAUUJBEWMUUBUUJWLUUAJKWKXHWJVBVCVDVEVFVR - VQSVTXIYQWAWBYOYRWPCXHYMWCVIVJXLYOWPCXKYNXHWDUTVIVJWEWFWGWH $. + vj co sylancl 1onn nndceq suc0 raleqi eleq2 ifbid mpteq2dv fveqeq2d ralsn + csn 0ex bitri dcbii sylibr wa cun wf adantl peano2 adantr syl ralsng dcan + wb mpbird ex mpan9 ralunb df-suc exp31 a2d finds impcom ) DEFAGHUBUNFZBEB + IZCIZFZJKUCZUDZAUEJLZCDMZNZOZWIWOCUAIZMZNZOZPWIWOCKMZNZOZPWIWOCUMIZMZNZOZ + PWIWOCXGMZNZOZPWIWRPUAUMDWSKLZXBXEWIXMXAXDXMWOCWTXCWSKQRSTWSXFLZXBXIWIXNX + AXHXNWOCWTXGWSXFQRSTWSXGLZXBXLWIXOXAXKXOWOCWTXJWSXGQRSTWSDLZXBWRWIXPXAWQX + PWOCWTWPWSDQRSTWIBEWJKFZJKUCZUDZAUEZJLZOZXEWIXTEFZJEFZYBWIXTGFGEFZYCWIHGX + SAAGHUFZKEFXSHFWIUGBKUHUIUJUKXTGULUOUPXTJUQUOXDYAXDWOCKVEZNYAWOCXCYGURUSW + OYACKVFWKKLZWNXSJAYHBEWMXRYHWLXQJKWKKWJUTVAVBVCVDVGVHVIXFEFZWIXIXLYIWIXIX + LYIWIVJZXIVJZWOCXGXGVEZVKZNZOZXLYKXHWOCYLNZVJZOZYOYJYPOZXIYRYJYSBEWJXGFZJ + KUCZUDZAUEZJLZOZYJUUCEFZYDUUEYJUUCGFYEUUFYJHGUUBAWIHGAVLYIYFVMYJXGEFZUUBH + FYIUUGWIXFVNVOZBXGUHVPUJUKUUCGULUOUPUUCJUQUOYJYPUUDYJUUGYPUUDVSUUHWOUUDCX + GEWKXGLZWNUUBJAUUIBEWMUUAUUIWLYTJKWKXGWJUTVAVBVCVQVPSVTXIYSYRXHYPVRWAWBYN + YQWOCXGYLWCVHVIXKYNWOCXJYMXGWDUSVHVIWEWFWGWH $. $} ${