diff --git a/iset.mm b/iset.mm index 725f9e02d..5ca1f0348 100644 --- a/iset.mm +++ b/iset.mm @@ -183867,8 +183867,28 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is lgsquad.5 $e |- N = ( ( Q - 1 ) / 2 ) $. lgsquad.6 $e |- S = { <. x , y >. | ( ( x e. ( 1 ... M ) /\ y e. ( 1 ... N ) ) /\ ( y x. P ) < ( x x. Q ) ) } $. - $( Lemma for Quadratic Reciprocity. Count the members of ` S ` with odd - coordinates. (Contributed by Mario Carneiro, 19-Jun-2015.) $) + $( Lemma for ~ lgsquad . ` S ` is finite. (Contributed by Jim Kingdon, + 16-Sep-2025.) $) + lgsquadlemsfi $p |- ( ph -> S e. Fin ) $= + ( cv co c1 nnzd wcel cn cmul clt wbr cfz 1zzd gausslemma2dlem0b fzfigd wa + wdc cz elfznn ad2antll gausslemma2dlem0a adantr nnmulcld ad2antrl syl2anc + zdclt ralrimivva opabfi ) ACOZDUAPZBOZEUAPZUBUCZBCQGUDPZQHUDPZFNAQGAUEZAG + ADGILUFRUGAQHVHAHAEHJMUFRUGAVEUIZBCVFVGAVCVFSZVAVGSZUHZUHZVBUJSVDUJSVIVMV + BVMVADVKVATSAVJVAHUKULADTSVLADIUMUNUORVMVDVMVCEVJVCTSAVKVCGUKUPAETSVLAEJU + MUNUORVBVDURUQUSUT $. + + $( Lemma for ~ lgsquad . There are finitely many members of ` S ` with odd + first part. (Contributed by Jim Kingdon, 16-Sep-2025.) $) + lgsquadlemofi $p |- ( ph -> { z e. S | -. 2 || ( 1st ` z ) } e. Fin ) $= + ( c2 cv wcel wa co c1st cfv cdvds wbr wn lgsquadlemsfi wdc cn 2nn cfz cxp + cz cmul clt copab opabssxp eqsstri sseli xp1st syl elfzelzd adantl dvdsdc + c1 sylancr dcn ralrimiva ssfirab ) APDQZUAUBZUCUDZUEZDGABCEFGHIJKLMNOUFAV + LUGZDGAVIGRZSZVKUGZVMVOPUHRVJULRZVPUIVNVQAVNVJVDHVNVIVDHUJTZVDIUJTZUKZRVJ + VRRGVTVIGBQZVRRCQZVSRSWBEUMTWAFUMTUNUDZSBCUOVTOWCBCVRVSUPUQURVIVRVSUSUTVA + VBPVJVCVEVKVFUTVGVH $. + + $( Lemma for ~ lgsquad . Count the members of ` S ` with odd coordinates. + (Contributed by Mario Carneiro, 19-Jun-2015.) $) lgsquadlem1 $p |- ( ph -> ( -u 1 ^ sum_ u e. ( ( ( |_ ` ( M / 2 ) ) + 1 ) ... M ) ( |_ ` ( ( Q / P ) x. ( 2 x. u ) ) ) ) = @@ -183876,149 +183896,343 @@ mathematician Ptolemy (Claudius Ptolemaeus). This particular version is ( c2 co wbr wcel vv vn c1 cneg cdiv cfl cfv caddc cfz cmul csu cexp cdvds cv c1st wn crab chash cc neg1cn a1i cc0 cap cz gausslemma2dlem0b nnzd 2nn cn cq sylancl flqcld peano2zd fzfigd wa gausslemma2dlem0a adantr syl2an2r - znq 2z elfzelz adantl zmulcl sylancr syl syl2anc fsumzcl cn0 cfn clt 1zzd - wdc elfznn ad2antll nnmulcld ad2antrl ralrimivva ralrimiva ssfirab hashcl - cxp nn0zd wceq ax-1cn oveq1i eqtrid cmin zsubcld wral elrab nncnd adantrr - oveq2d zcnd nncand eqtrd oveq1d 2cnd 2ap0 wrex cprime ad2antrr wb syl3anc - breq2d 3syl cle zred nnred rehalfcld zltp1le mpbird syl112anc mpbid recnd - cr sub32d nngt0d 3eqtrd eqbrtrd fznn neg1ap0 qmulcl expclzapd zdclt copab - zq opabfi opabssxp eqsstri sseli xp1st elfzelzd dvdsdc dcn expcl recidapd - expap0d 1div1e1 negeqi 1ap0 divneg2ap mp3an eqtr3i exprecapd ciun syl2anr - zdceq fveqeq2 simprbi divcanap3d invdisj hashiun iunrab csn cdif eldifsni - wdisj wne necomd neneqd cuz ax-mp eldifad dvdsprm mtbird adantlr dvdsmul1 - uzid npcand dvds2add mpan2d mtod breq2 notbid syl5ibrcom rexlimdva sselid - wi simpr odd2np1 simprl zre simprr eqeltrd elfzle2 2re ltmuldiv2 2halvesd - flqle mvlraddd breqtrd ltsub13d lelttrd 2t0e0 2cn zcn mulcl pncan nnm1nn0 - 2pos eqeltrrd eqbrtrid 0red lemul2 subge02d elfzd prmnn peano2cn subsub4d - nn0ge0d subdid oveq2i peano2zm gt0ap0d divcanap2d eqtr2d 3eqtr3d 3eqtr3rd - 1cnd rspceeqv rexlimdvaa sylbid impbid rabbidva fveq2d wss wrel relopabiv - oveq2 ssrab2 relss mp2 relxp cop eleq2i opabidw bitri anass lesub mulcomd - nnre nnap0d divcanap1d nndivred 3eqtr2d oveq12d subdird remulcld resubcld - mul32d 3eqtr4d ltmul1 ltsub13 3bitr2d nnz zsubcl syl2an peano2rem 3bitr4d - flqlt 3bitrd anbi2d nnmulcl 2timesd mvrladdd ltm1d ltled div32apd flqltp1 - ltdiv1 elfzle1 ltletrd ltdivmul eqbrtrrid zlem1lt ledivmul lemuldiv letrd - div23apd flqge subled pm4.71rd bitr4d pm5.32da breqtrdi lemuldiv2 posdifd - bitrid elnnz sylanbrc oveq12i pncan2d eqtr3d ltsub23d mpbir2and biantrurd - letr bitr3d anbi12d op1std eqeq1d biancomi opelxp anbi1i 3bitr4g eqrelrdv - vex velsn cen xpsnen2g hashen ltmul2 ltdivmul2 eqbrtrrd zltlem1 syl3anbrc - breqtrrd eluz2 uznn0sub hashfz1 sumeq2dv fsumsub pncan3d fsumconst nn0cnd - mul12d zmulcld expmulzap syl22anc neg1sqe1 1exp expaddzap mulcanap2ad ) A - UCUDZIQUERZUFUGZUCUHRZIUIRZGFUERZQEUNZUJRZUJRZUFUGZEUKZULRZWUNQDUNZUOUGZU - MSZUPZDHUQZURUGZULRZWVLAWUNWVDWUNUSTZAUTVAZWUNVBVCSZAUUAVAZAWURWVCEAWUQIA - WUPAWUOAIVDTZQVHTZWUOVITZAIAFIKNVEZVFZVGIQVRVJZVKVLZWWAVMZAWUTWURTZVNZWVB - WWFWUSVITZWVAVITZWVBVITZAGVDTZWWEFVHTZWWGAGAGLVOZVFAWWKWWEAFKVOZVPZGFVRVQ - WWFWVAVDTZWWHWWFQVDTZWUTVDTZWWOVSWWEWWQAWUTWUQIVTZWAZQWUTWBWCZWVAUUFWDWUS - WVAUUBWEZVKZWFZUUCAWVMWVKWGTZWVLUSTUTAWVJWHTWXDAWVIDHACUNZFUJRZBUNZGUJRZW - ISZBCUCIUIRZUCJUIRZHPAUCIAWJZWWAVMAUCJWXLAJAGJLOVEZVFZVMAWXIWKZBCWXJWXKAW - XGWXJTZWXEWXKTZVNZVNZWXFVDTWXHVDTWXOWXSWXFWXSWXEFWXQWXEVHTZAWXPWXEJWLWMAW - WKWXRWWMVPWNVFWXSWXHWXSWXGGWXPWXGVHTAWXQWXGIWLWOAGVHTZWXRWWLVPWNVFWXFWXHU - UDWEWPUUGZAWVIWKZDHAWVFHTZVNZWVHWKZWYCWYEWVRWVGVDTZWYFVGWYDWYGAWYDWVGUCIW - YDWVFWXJWXKWTZTZWVGWXJTZHWYHWVFHWXRWXIVNZBCUUEZWYHPWXIBCWXJWXKUUHUUIZUUJW - VFWXJWXKUUKZWDUULZWAQWVGUUMWCWVHUUNWDWQWRWVJWSWDZWUNWVKUUOWCZWYQAWUNWVKWV - NWVPAWVKWYPXAZUUQZAWVLWVLUJRZWUNWVDWVKUHRZULRZWVEWVLUJRZAWVLUCWVLUERZUJRU - CWYTXUBAWVLWYQWYSUUPAWVLXUDWVLUJAWVLUCWUNUERZWVKULRXUDWUNXUEWVKULUCUCUERZ - UDZWUNXUEXUFUCUURUUSUCUSTZXUHUCVBVCSXUGXUEXBXCXCUUTUCUCUVAUVBUVCXDAWUNWVK - WVNWVPWYRUVDXEXLAXUBWUNQWURURUGZJUJRZUJRZULRZWUNQULRZXUJULRZUCAXUAXUKWUNU - LAXUAWVDWURQJUJRZEUKZWVDXFRZUHRXUPXUKAWVKXUQWVDUHAWURXUOWVCXFRZEUKZWVKXUQ - AEWURWVGFWVAXFRZXBZDHUQZUVEZURUGWURXVBURUGZEUKWVKXUSAEWURXVBWWDWWFXVADHAH - WHTWWEWYBVPWWFXVAWKZDHWYDWYGXUTVDTZXVEWWFWYOWWFFWVAWWFFWWNVFZWWTXGWVGXUTU - VGUVFWQWRZAFUAUNZUOUGZXFRZQUERZWUTXBZUAXVBXHEWURXHEWURXVBUVQAXVMEUAWURXVB - AWWEXVIXVBTZVNVNZXVLWVAQUERWUTXVOXVKWVAQUEXVOXVKFXUTXFRWVAXVOXVJXUTFXFXVN - XVJXUTXBZAWWEXVNXVIHTXVPXVAXVPDXVIHWVFXVIXUTUOUVHXIUVIWMXLXVOFWVAAWWEFUST - XVNWWFFWWNXJZXKAWWEWVAUSTXVNWWFWVAWWTXMZXKXNXOXPXVOWUTQAWWEWUTUSTXVNWWFWU - TWWSXMXKXVOXQQVBVCSZXVOXRVAUVJXOWPEUAWURXVBXVLUVKWDUVLAXVCWVJURAXVCXVAEWU - RXSZDHUQWVJXVAEDWURHUVMAXVTWVIDHWYEXVTWVIWYEXVAWVIEWURWYEWWEVNZWVIXVAQXUT - UMSZUPXWAXWBQXUTWVAUHRZUMSZXWAXWDQFUMSZXWAXWEQFXBZAXWFUPWYDWWEAQFAFQAFXTQ - UVNZUVOTFQUVRKFXTQUVPWDUVSUVTYAXWAQQUWAUGTZFXTTZXWEXWFYBWWPXWHVSQUWHUWBAX - WIWYDWWEAFXTXWGKUWCZYAFQUWDWCUWEXWAXWCFQUMXWAFWVAXWAFAWWKWYDWWEWWMYAZXJXW - AWVAAWWEWWOWYDWWTUWFZXMUWIYDUWEXWAXWBQWVAUMSZXWDXWAWWPWWQXWMVSWWEWWQWYEWW - RWAQWUTUWGWCXWAWWPXVFWWOXWBXWMVNXWDUWRWWPXWAVSVAXWAFWVAXWAFXWKVFXWLXGXWLQ - XUTWVAUWJYCUWKUWLXVAWVHXWBWVGXUTQUMUWMUWNUWOUWPWYEWVIQUBUNZUJRZUCUHRZWVGX - BZUBVDXSZXVTWYEWYJWYGWVIXWRYBWYEWYIWYJWYEHWYHWVFWYMAWYDUWSUWQWYNWDZWVGUCI - VTUBWVGUWTYEWYEXWQXVTUBVDWYEXWNVDTZXWQVNZVNZIXWNXFRZWURTWVGFQXXCUJRZXFRZX - BXVTXXBXXCWUQIXXBWUPXXBWUOAWVSWYDXXAWWBYAZVKZVLXXBIAIVHTZWYDXXAWVTYAVFZXX - BIXWNXXIWYEXWTXWQUXAZXGZXXBWUPXXCWISZWUQXXCYFSZXXBWUPWUOXXCXXBWUPXXGYGXXB - IAIYOTZWYDXXAAIWVTYHZYAZYIZXXBXXCXXKYGXXBWVSWUPWUOYFSXXFWUOUXIWDXXBXWNIWU - OXWTXWNYOTZWYEXWQXWNUXBWOZXXPXXQXXBXWNWUOIWUOXFRWIXXBXWOIWISZXWNWUOWISZXX - BXXTXWPIYFSZXXBXWPWXJTZXYBXXBXWPWVGWXJWYEXWTXWQUXCZWYEWYJXXAXWSVPUXDZXWPU - CIUXEWDXXBXWOVDTZWVQXXTXYBYBXXBWWPXWTXYFVSXXJQXWNWBWCXXIXWOIYJWEYKXXBXXRX - XNQYOTZVBQWISZXXTXYAYBXXSXXPXYGXXBUXFVAZXYHXXBUXTVAZXWNIQUXGYLYMXXBWUOWUO - IXXBWUOXXQYNZXYKXXBIAIUSTZWYDXXAAIWVTXJZYAZUXHUXJUXKUXLUXMXXBWUPVDTXXCVDT - XXLXXMYBXXGXXKWUPXXCYJWEYMXXBVBXWNYFSZXXCIYFSXXBXYOQVBUJRZXWOYFSZXXBXYPVB - XWOYFUXNXXBXWOXXBXWPUCXFRZXWOWGXXBXWOUSTZXUHXYRXWOXBXXBQUSTXWNUSTZXYSUXOX - WTXYTWYEXWQXWNUXPWOZQXWNUXQWCZXCXWOUCUXRVJXXBXYCXWPVHTXYRWGTXYEXWPIWLXWPU - XSYEUYAUYJUYBXXBVBYOTXXRXYGXYHXYOXYQYBXXBUYCXXSXYIXYJVBXWNQUYDYLYKXXBIXWN - XXPXXSUYEYMUYFXXBFFXWPXFRZXFRXWPXXEWVGXXBFXWPXXBFXXBXWIWWKAXWIWYDXXAXWJYA - FUYGWDXJZXXBXYSXWPUSTYUBXWOUYHWDXNXXBYUCXXDFXFXXBFXWOXFRUCXFRFUCXFRZXWOXF - RZYUCXXDXXBFXWOUCYUDYUBXXBUYSZYPXXBFXWOUCYUDYUBYUGUYIXXBXXDQIUJRZXWOXFRYU - FXXBQIXWNXXBXQZXYNYUAUYKXXBYUHYUEXWOXFXXBYUHQYUEQUERZUJRYUEIYUJQUJNUYLXXB - YUEQXXBYUEXXBFVDTZYUEVDTZAYUKWYDXXAAFWWMVFZYAFUYMZWDXMYUIXXBQXYIXYJUYNUYO - XEXPUYPUYQXLXYDUYREXXCWURXUTXXEWVGWUTXXCXBWVAXXDFXFWUTXXCQUJVUIXLUYTWEVUA - VUBVUCVUDXEVUEAWURXVDXUREWWFXVDXUTUVNZUCXURUIRZWTZURUGZYUPURUGZXURWWFXVBY - UQURWWFBCXVBYUQXVBHVUFHVUGXVBVUGXVADHVUJWYKBCHPVUHXVBHVUKVULYUOYUPVUMWWFW - XGXUTXBZWXGWXEVUNZHTZVNYUTWXEYUPTZVNZYVAXVBTZYVAYUQTZWWFYUTYVBYVCYVBWYKWW - FYUTVNZYVCYVBYVAWYLTWYKHWYLYVAPVUOWYKBCVUPVUQYVGWXTWXEJYFSZVNZWXFXUTGUJRZ - WISZVNZWXTWXEXURYFSZVNZWYKYVCYVLWXTYVHYVKVNZVNZYVGYVNWXTYVHYVKVURWWFYVPYV - NYBYUTWWFWXTYVOYVMWWFWXTVNZYVOYVHYVMVNYVMYVQYVKYVMYVHYVQWVCUCUHRZGWXEXFRZ - YFSZWXEGYVRXFRZYFSZYVKYVMYVQYVRYOTZGYOTZWXEYOTZYVTYWBYBWWFYWCWXTWWFYVRWWF - WVCWXBVLYGVPAYWDWWEWXTAGWWLYHZYAZWXTYWEWWFWXEVVAWAZYVRGWXEVUSYCYVQYVKWVBY - VSWISZWVCYVSWISZYVTYVQYVKWXFGWVBXFRZFUJRZWISZWXEYWKWISZYWIYVQYVJYWLWXFWIW - WFYVJYWLXBWXTWWFFGUJRZWVAGUJRZXFRGFUJRZWVBFUJRZXFRYVJYWLWWFYWOYWQYWPYWRXF - WWFFGXVQWWFGAYWDWWEYWFVPZYNZVUTWWFYWPGWVAUJRZWUSFUJRZWVAUJRYWRWWFWVAGXVRY - WTVUTWWFYXBGWVAUJWWFGFYWTXVQWWFFWWNVVBZVVCXPWWFWUSFWVAWWFWUSAWUSYOTWWEAGF - YWFWWMVVDVPZYNXVQXVRVVJVVEVVFWWFFWVAGXVQXVRYWTVVGWWFGWVBFYWTWWFWVBWWFWUSW - VAYXDWWFWVAWWTYGZVVHZYNXVQVVGVVKVPYDYVQYWEYWKYOTFYOTZVBFWISZYWNYWMYBYWHYV - QGWVBYWGWWFWVBYOTZWXTYXFVPZVVIYVQFWWFWWKWXTWWNVPZYHYVQFYXKYQWXEYWKFVVLYLY - VQYWEYWDYXIYWNYWIYBYWHYWGYXJWXEGWVBVVMYCVVNWWFWWIWXTYVSVDTZYWIYWJYBWXAWWF - WWJWXEVDTYXLWXTWWFGAWYAWWEWWLVPZVFZWXEVVOGWXEVVPVVQZWVBYVSVVTVQWWFWVCVDTZ - WXTYXLYWJYVTYBWXBYXOWVCYVSYJVQVWAYVQXURYWAWXEYFWWFXURYWAXBWXTWWFXURGUCXFR - ZWVCXFRGWVCXFRUCXFRYWAWWFXUOYXQWVCXFWWFXUOQYXQQUERZUJRYXQJYXRQUJOUYLWWFYX - QQWWFYXQWWFYWDYXQYOTZYWSGVVRWDZYNWWFXQZXVSWWFXRVAZUYOXEZXPWWFGUCWVCYWTWWF - UYSZWWFWVCWXBXMZYPWWFGWVCUCYWTYYEYYDUYIYRVPYDVVSVWBYVQYVMYVHYVQYVMXURJYFS - ZYVHWWFYYFWXTWWFXUOJWVCWWFXUOAXUOVHTZWWEAWVRJVHTZYYGVGWXMQJVWCWCZVPZYHWWF - JAYYHWWEWXMVPYHZWWFWVCWXBYGWWFXUOJXFRJWVCYFWWFXUOJJAJUSTWWEAJWXMXJZVPZYYM - WWFJYYMVWDVWEWWFJWVBYFSZJWVCYFSZWWFJGQUERZWVBYYKWWFGYWSYIZYXFWWFJYYPYYKYY - QWWFJYXRYYPWIOWWFYXQGWISZYXRYYPWISZWWFGYWSVWFWWFYXSYWDXYGXYHYYRYYSYBYXTYW - SXYGWWFUXFVAZXYHWWFUXTVAZYXQGQVWJYLYMUYBVWGWWFYYPYXAFUERZWVBYFWWFYYPFUJRZ - YXAYFSZYYPUUUBYFSZWWFUUUCGFQUERZUJRZYXAYFWWFGQFYWTYYAXVQYYBVWHWWFUUUFWVAY - FSZUUUGYXAYFSZWWFUUUHFQWVAUJRZYFSZWWFUUUKYUEUUUJWISZWWFYUJWVAWISZUUULWWFY - UJIWVAWINWWFWUOWUTWISZIWVAWISZWWFWUOWUQWUTWWFIAXXNWWEXXOVPZYIWWFWUQAWUQVD - TWWEWWCVPYGWWFWUTWWSYGZWWFWVSWUOWUQWISAWVSWWEWWBVPWUOVWIWDWWEWUQWUTYFSAWU - TWUQIVWKWAVWLWWFXXNWUTYOTZXYGXYHUUUNUUUOYBUUUPUUUQYYTUUUAIWUTQVWMYLYMZVWN - WWFYUEYOTZWVAYOTZXYGXYHUUUMUUULYBWWFYXGUUUTWWFFWWNYHZFVVRWDZYXEYYTUUUAYUE - WVAQVWMYLYMAYUKWWEUUUJVDTZUUUKUUULYBYUMWWFWWPWWOUUVDVSWWTQWVAWBWCFUUUJVWO - VQYKWWFYXGUUVAXYGXYHUUUHUUUKYBUUVBYXEYYTUUUAFWVAQVWPYLYKWWFUUUFYOTUUVAYWD - VBGWISZUUUHUUUIYBWWFFUUVBYIYXEYWSWWFGYXMYQZUUUFWVAGUYDYLYMYSWWFYYPYOTYXAY - OTZYXGYXHUUUDUUUEYBYYQWWFGWVAYWSYXEVVHZUUVBWWFFWWNYQZYYPYXAFVWQYLYMWWFGWV - AFYWTXVRXVQYXCVWSZUXKVWRWWFWWIJVDTZYYNYYOYBWXAAUUVKWWEWXNVPWVBJVWTWEYMYSV - XAVPYVQYWEXURYOTJYOTYVMYYFVNYVHUWRYWHYVQXURWWFXURVDTZWXTWWFXUOWVCWWFXUOYY - JVFZWXBXGZVPYGYVQJAYYHWWEWXTWXMYAYHWXEXURJVXQYCUWKVXBVXCVXDVPVXHYVGWXRYVI - WXIYVKYVGWXQWXRYVIYVGWXPWXQYVGWXGXUTWXJWWFYUTUWSZWWFXUTWXJTZYUTWWFUUVPXUT - VHTZXUTIYFSZWWFXVFVBXUTWISZUUVQWWFFWVAAYUKWWEYUMVPWWTXGZWWFWVAFWISZUUVSWW - FWVAYUEFYXEUUVCUUVBWWFWVAYUEYFSZWUTYUJYFSZWWFWUTIYUJYFWWEWUTIYFSAWUTWUQIU - XEWANVXEWWFUUURUUUTXYGXYHUUWBUUWCYBUUUQUUVCYYTUUUAWUTYUEQVXFYLYKWWFFUUVBV - WFUXMZWWFWVAFYXEUUVBVXGYMXUTVXIVXJWWFUUVRXUTUCXFRZIWISZWWFUUWEYUEWVAXFRIW - IWWFFWVAUCXVQXVRYYDYPWWFYUEIWVAUUVCUUUPYXEWWFYUEIXFRZIWVAWIWWFIIUHRZIXFRU - UWGIWWFUUWHYUEIXFWWFUUWHYUJYUJUHRYUEIYUJIYUJUHNNVXKWWFYUEWWFYUEWWFYUKYULX - VGYUNWDXMUXHXEXPWWFIIAXYLWWEXYMVPZUUWIVXLVXMUUUSYSVXNYSWWFXVFWVQUUVRUUWFY - BUUVTWWFIAXXHWWEWVTVPVFZXUTIVWOWEYKWWFWVQUUVPUUVQUUVRVNYBUUWJXUTIYTWDVXOV - PUXDVXPYVGUUVKWXQYVIYBAUUVKWWEYUTWXNYAWXEJYTWDVXRYVGWXHYVJWXFWIYVGWXGXUTG - UJUUVOXPYDVXSYVGUUVLYVCYVNYBWWFUUVLYUTUUVNVPWXEXURYTWDVVSVXHVXDYVEYUTYVBX - VAYUTDYVAHWVFYVAXBWVGWXGXUTWXGWXEWVFBVYGCVYGVXTVYAXIVYBYVFWXGYUOTZYVCVNYV - DWXGWXEYUOYUPVYCUUWKYUTYVCBXUTVYHVYDVUQVYEVYFZVUEWWFYURYUSXBZYUQYUPVYISZW - WFXVFYUPWHTZUUWNUUVTWWFUCXURWWFWJUUVNVMZXUTYUPVDWHVYJWEWWFYUQWHTUUWOUUWMU - UWNYBWWFXVBYUQWHUUWLXVHUYAUUWPYUQYUPVYKWEYKWWFXUOWVCUWAUGTZXURWGTYUSXURXB - WWFYXPXUOVDTWVCXUOYFSUUWQWXBUUVMWWFWVCYXQXUOYFWWFWVCGWISZWVCYXQYFSZWWFWVB - GWISZUUWRWWFUUUBWVBGWIUUVJWWFUUUBGWISZYXAYWQWISZWWFUUWAUUXBUUWDWWFUUVAYXG - YWDUUVEUUWAUUXBYBYXEUUVBYWSUUVFWVAFGVYLYLYMWWFUUVGYWDYXGYXHUUXAUUXBYBUUVH - YWSUUVBUUVIYXAGFVYMYLYKVYNWWFWWIWWJUUWTUUWRYBWXAYXNWVBGVVTWEYMWWFYXPWWJUU - WRUUWSYBWXBYXNWVCGVYOWEYMYYCVYQWVCXUOVYRVYPWVCXUOVYSXURVYTYEYRWUAUYRAWURX - UOWVCEWWDAXUOUSTZWWEAXUOYYIXJZVPYYEWUBVXMXLAWVDXUPAWVDWXCXMAXUPAWURXUOEWW - DUUVMWFXMWUCAXUPXUIXUOUJRZXUKAWURWHTZUUXCXUPUUXEXBWWDUUXDWURXUOEWUDWEAXUI - QJAXUIAUUXFXUIWGTWWDWURWSWDZWUEAXQYYLWUFXOYRXLAWVMWVOWWPXUJVDTZXULXUNXBWV - NWVPWWPAVSVAAXUIJAXUIUUXGXAWXNWUGZWUNQXUJWUHWUIAXUNUCXUJULRZUCXUMUCXUJULW - UJXDAUUXHUUXJUCXBUUXIXUJWUKWDXEYRVVKAWVMWVOWVDVDTWVKVDTXUBXUCXBWVNWVPWXCW - YRWUNWVDWVKWULWUIUYPWUM $. + znq 2z elfzelz adantl zmulcl sylancr syl syl2anc fsumzcl cn0 hashcl nn0zd + cfn wceq ax-1cn oveq1i eqtrid oveq2d cmin cxp zsubcld elrab nncnd adantrr + clt wral zcnd nncand oveq1d 2cnd 2ap0 wrex cprime csn ad2antrr cuz mtbird + eqtrd wb breq2d wi syl3anc mpan2d simpr 3syl cle nnred rehalfcld ad2antrl + zred cr eqeltrd elfzle2 mpbird syl112anc mpbid recnd sub32d nngt0d 3eqtrd + zltp1le eqbrtrd fznn neg1ap0 qmulcl expclzapd lgsquadlemofi expcl expap0d + zq recidapd 1div1e1 negeqi divneg2ap mp3an eqtr3i exprecapd lgsquadlemsfi + 1ap0 ciun wdc copab opabssxp eqsstri sseli xp1st elfzelzd zdceq ralrimiva + syl2anr ssfirab wdisj fveqeq2 simprbi ad2antll divcanap3d invdisj hashiun + ralrimivva iunrab cdif wne eldifsni necomd neneqd eldifad dvdsprm adantlr + uzid ax-mp npcand dvdsmul1 mtod breq2 notbid syl5ibrcom rexlimdva odd2np1 + dvds2add sselid simprl zre simprr 2re ltmuldiv2 2halvesd mvlraddd breqtrd + flqle 2pos ltsub13d lelttrd 2t0e0 2cn mulcl pncan elfznn nnm1nn0 eqeltrrd + zcn nn0ge0d eqbrtrid lemul2 subge02d elfzd prmnn peano2cn subsub4d subdid + oveq2i peano2zm gt0ap0d divcanap2d eqtr2d 3eqtr3d 3eqtr3rd oveq2 rspceeqv + 0red 1cnd rexlimdvaa sylbid impbid rabbidva fveq2d ssrab2 relopabiv relss + wss wrel mp2 relxp cop eleq2i opabidw bitri anass nnre mulcomd divcanap1d + nnap0d nndivred 3eqtr2d oveq12d subdird remulcld 3eqtr4d resubcld ltsub13 + lesub mul32d ltmul1 3bitr2d nnz zsubcl syl2an flqlt 3bitrd 3bitr4d anbi2d + peano2rem nnmulcl 2timesd mvrladdd ltm1d div32apd flqltp1 elfzle1 ltletrd + ltdiv1 ltled ltdivmul eqbrtrrid zlem1lt ledivmul lemuldiv div23apd subled + letrd flqge letr pm4.71rd bitr4d pm5.32da bitrid breqtrdi lemuldiv2 elnnz + posdifd sylanbrc oveq12i pncan2d eqtr3d ltsub23d mpbir2and bitr3d anbi12d + biantrurd vex op1std eqeq1d biancomi opelxp velsn anbi1i 3bitr4g eqrelrdv + cen 1zzd xpsnen2g hashen ltmul2 ltdivmul2 eqbrtrrd zltlem1 breqtrrd eluz2 + syl3anbrc uznn0sub hashfz1 sumeq2dv fsumsub pncan3d nn0cnd mul12d zmulcld + fsumconst expmulzap syl22anc neg1sqe1 1exp expaddzap mulcanap2ad ) AUCUDZ + IQUERZUFUGZUCUHRZIUIRZGFUERZQEUNZUJRZUJRZUFUGZEUKZULRZWUKQDUNZUOUGZUMSZUP + ZDHUQZURUGZULRZWVIAWUKWVAWUKUSTZAUTVAZWUKVBVCSZAUUAVAZAWUOWUTEAWUNIAWUMAW + ULAIVDTZQVHTZWULVITZAIAFIKNVEZVFZVGIQVRVJZVKVLZWVRVMZAWUQWUOTZVNZWUSWWCWU + PVITZWURVITZWUSVITZAGVDTZWWBFVHTZWWDAGAGLVOZVFAWWHWWBAFKVOZVPZGFVRVQWWCWU + RVDTZWWEWWCQVDTZWUQVDTZWWLVSWWBWWNAWUQWUNIVTZWAZQWUQWBWCZWURUUGWDWUPWURUU + BWEZVKZWFZUUCAWVJWVHWGTZWVIUSTUTAWVGWJTWXAABCDFGHIJKLMNOPUUDWVGWHWDZWUKWV + HUUEWCZWXCAWUKWVHWVKWVMAWVHWXBWIZUUFZAWVIWVIUJRZWUKWVAWVHUHRZULRZWVBWVIUJ + RZAWVIUCWVIUERZUJRUCWXFWXHAWVIWXCWXEUUHAWVIWXJWVIUJAWVIUCWUKUERZWVHULRWXJ + WUKWXKWVHULUCUCUERZUDZWUKWXKWXLUCUUIUUJUCUSTZWXNUCVBVCSWXMWXKWKWLWLUUPUCU + CUUKUULUUMWMAWUKWVHWVKWVMWXDUUNWNWOAWXHWUKQWUOURUGZJUJRZUJRZULRZWUKQULRZW + XPULRZUCAWXGWXQWUKULAWXGWVAWUOQJUJRZEUKZWVAWPRZUHRWYBWXQAWVHWYCWVAUHAWUOW + YAWUTWPRZEUKZWVHWYCAEWUOWVDFWURWPRZWKZDHUQZUUQZURUGWUOWYHURUGZEUKWVHWYEAE + WUOWYHWWAWWCWYGDHAHWJTWWBABCFGHIJKLMNOPUUOVPWWCWYGUURZDHWVCHTZWVDVDTZWYFV + DTZWYKWWCWYLWVDUCIWYLWVCUCIUIRZUCJUIRZWQZTZWVDWYOTZHWYQWVCHBUNZWYOTZCUNZW + YPTZVNZXUBFUJRZWYTGUJRZXBSZVNZBCUUSZWYQPXUGBCWYOWYPUUTUVAZUVBWVCWYOWYPUVC + ZWDUVDWWCFWURWWCFWWKVFZWWQWRWVDWYFUVEUVGUVFUVHZAFUAUNZUOUGZWPRZQUERZWUQWK + ZUAWYHXCEWUOXCEWUOWYHUVIAXUREUAWUOWYHAWWBXUNWYHTZVNVNZXUQWURQUERWUQXUTXUP + WURQUEXUTXUPFWYFWPRWURXUTXUOWYFFWPXUSXUOWYFWKZAWWBXUSXUNHTXVAWYGXVADXUNHW + VCXUNWYFUOUVJWSUVKUVLWOXUTFWURAWWBFUSTXUSWWCFWWKWTZXAAWWBWURUSTXUSWWCWURW + WQXDZXAXEXOXFXUTWUQQAWWBWUQUSTXUSWWCWUQWWPXDXAXUTXGQVBVCSZXUTXHVAUVMXOUVP + EUAWUOWYHXUQUVNWDUVOAWYIWVGURAWYIWYGEWUOXIZDHUQWVGWYGEDWUOHUVQAXVEWVFDHAW + YLVNZXVEWVFXVFWYGWVFEWUOXVFWWBVNZWVFWYGQWYFUMSZUPXVGXVHQWYFWURUHRZUMSZXVG + XVJQFUMSZXVGXVKQFWKZAXVLUPWYLWWBAQFAFQAFXJQXKZUVRTFQUVSKFXJQUVTWDUWAUWBXL + XVGQQXMUGTZFXJTZXVKXVLXPWWMXVNVSQUWFUWGAXVOWYLWWBAFXJXVMKUWCZXLFQUWDWCXNX + VGXVIFQUMXVGFWURXVGFAWWHWYLWWBWWJXLZWTXVGWURAWWBWWLWYLWWQUWEZXDUWHXQXNXVG + XVHQWURUMSZXVJXVGWWMWWNXVSVSWWBWWNXVFWWOWAQWUQUWIWCXVGWWMWYNWWLXVHXVSVNXV + JXRWWMXVGVSVAXVGFWURXVGFXVQVFXVRWRXVRQWYFWURUWPXSXTUWJWYGWVEXVHWVDWYFQUMU + WKUWLUWMUWNXVFWVFQUBUNZUJRZUCUHRZWVDWKZUBVDXIZXVEXVFWYSWYMWVFXWDXPXVFWYRW + YSXVFHWYQWVCXUJAWYLYAUWQXUKWDZWVDUCIVTUBWVDUWOYBXVFXWCXVEUBVDXVFXVTVDTZXW + CVNZVNZIXVTWPRZWUOTWVDFQXWIUJRZWPRZWKXVEXWHXWIWUNIXWHWUMXWHWULAWVPWYLXWGW + VSXLZVKZVLXWHIAIVHTZWYLXWGWVQXLVFZXWHIXVTXWOXVFXWFXWCUWRZWRZXWHWUMXWIXBSZ + WUNXWIYCSZXWHWUMWULXWIXWHWUMXWMYGXWHIAIYHTZWYLXWGAIWVQYDZXLZYEZXWHXWIXWQY + GXWHWVPWUMWULYCSXWLWULUXFWDXWHXVTIWULXWFXVTYHTZXVFXWCXVTUWSYFZXXBXXCXWHXV + TWULIWULWPRXBXWHXWAIXBSZXVTWULXBSZXWHXXFXWBIYCSZXWHXWBWYOTZXXHXWHXWBWVDWY + OXVFXWFXWCUWTZXVFWYSXWGXWEVPYIZXWBUCIYJWDXWHXWAVDTZWVNXXFXXHXPXWHWWMXWFXX + LVSXWPQXVTWBWCXWOXWAIYRWEYKXWHXXDXWTQYHTZVBQXBSZXXFXXGXPXXEXXBXXMXWHUXAVA + ZXXNXWHUXGVAZXVTIQUXBYLYMXWHWULWULIXWHWULXXCYNZXXQXWHIAIUSTZWYLXWGAIWVQWT + ZXLZUXCUXDUXEUXHUXIXWHWUMVDTXWIVDTXWRXWSXPXWMXWQWUMXWIYRWEYMXWHVBXVTYCSZX + WIIYCSXWHXYAQVBUJRZXWAYCSZXWHXYBVBXWAYCUXJXWHXWAXWHXWBUCWPRZXWAWGXWHXWAUS + TZWXNXYDXWAWKXWHQUSTXVTUSTZXYEUXKXWFXYFXVFXWCXVTUXQYFZQXVTUXLWCZWLXWAUCUX + MVJXWHXXIXWBVHTXYDWGTXXKXWBIUXNXWBUXOYBUXPUXRUXSXWHVBYHTXXDXXMXXNXYAXYCXP + XWHUYPXXEXXOXXPVBXVTQUXTYLYKXWHIXVTXXBXXEUYAYMUYBXWHFFXWBWPRZWPRXWBXWKWVD + XWHFXWBXWHFXWHXVOWWHAXVOWYLXWGXVPXLFUYCWDWTZXWHXYEXWBUSTXYHXWAUYDWDXEXWHX + YIXWJFWPXWHFXWAWPRUCWPRFUCWPRZXWAWPRZXYIXWJXWHFXWAUCXYJXYHXWHUYQZYOXWHFXW + AUCXYJXYHXYMUYEXWHXWJQIUJRZXWAWPRXYLXWHQIXVTXWHXGZXXTXYGUYFXWHXYNXYKXWAWP + XWHXYNQXYKQUERZUJRXYKIXYPQUJNUYGXWHXYKQXWHXYKXWHFVDTZXYKVDTZAXYQWYLXWGAFW + WJVFZXLFUYHZWDXDXYOXWHQXXOXXPUYIUYJWNXFUYKUYLWOXXJUYMEXWIWUOWYFXWKWVDWUQX + WIWKWURXWJFWPWUQXWIQUJUYNWOUYOWEUYRUYSUYTVUAWNVUBAWUOWYJWYDEWWCWYJWYFXKZU + CWYDUIRZWQZURUGZYUBURUGZWYDWWCWYHYUCURWWCBCWYHYUCWYHHVUFHVUGWYHVUGWYGDHVU + CXUHBCHPVUDWYHHVUEVUHYUAYUBVUIWWCWYTWYFWKZWYTXUBVUJZHTZVNYUFXUBYUBTZVNZYU + GWYHTZYUGYUCTZWWCYUFYUHYUIYUHXUHWWCYUFVNZYUIYUHYUGXUITXUHHXUIYUGPVUKXUHBC + VULVUMYUMXUBVHTZXUBJYCSZVNZXUEWYFGUJRZXBSZVNZYUNXUBWYDYCSZVNZXUHYUIYUSYUN + YUOYURVNZVNZYUMYVAYUNYUOYURVUNWWCYVCYVAXPYUFWWCYUNYVBYUTWWCYUNVNZYVBYUOYU + TVNYUTYVDYURYUTYUOYVDWUTUCUHRZGXUBWPRZYCSZXUBGYVEWPRZYCSZYURYUTYVDYVEYHTZ + GYHTZXUBYHTZYVGYVIXPWWCYVJYUNWWCYVEWWCWUTWWSVLYGVPAYVKWWBYUNAGWWIYDZXLZYU + NYVLWWCXUBVUOWAZYVEGXUBVVGXSYVDYURWUSYVFXBSZWUTYVFXBSZYVGYVDYURXUEGWUSWPR + ZFUJRZXBSZXUBYVRXBSZYVPYVDYUQYVSXUEXBWWCYUQYVSWKYUNWWCFGUJRZWURGUJRZWPRGF + UJRZWUSFUJRZWPRYUQYVSWWCYWBYWDYWCYWEWPWWCFGXVBWWCGAYVKWWBYVMVPZYNZVUPWWCY + WCGWURUJRZWUPFUJRZWURUJRYWEWWCWURGXVCYWGVUPWWCYWIGWURUJWWCGFYWGXVBWWCFWWK + VURZVUQXFWWCWUPFWURWWCWUPAWUPYHTWWBAGFYVMWWJVUSVPZYNXVBXVCVVHVUTVVAWWCFWU + RGXVBXVCYWGVVBWWCGWUSFYWGWWCWUSWWCWUPWURYWKWWCWURWWQYGZVVCZYNXVBVVBVVDVPX + QYVDYVLYVRYHTFYHTZVBFXBSZYWAYVTXPYVOYVDGWUSYVNWWCWUSYHTZYUNYWMVPZVVEYVDFW + WCWWHYUNWWKVPZYDYVDFYWRYPXUBYVRFVVIYLYVDYVLYVKYWPYWAYVPXPYVOYVNYWQXUBGWUS + VVFXSVVJWWCWWFYUNYVFVDTZYVPYVQXPWWRWWCWWGXUBVDTYWSYUNWWCGAGVHTWWBWWIVPZVF + ZXUBVVKGXUBVVLVVMZWUSYVFVVNVQWWCWUTVDTZYUNYWSYVQYVGXPWWSYXBWUTYVFYRVQVVOY + VDWYDYVHXUBYCWWCWYDYVHWKYUNWWCWYDGUCWPRZWUTWPRGWUTWPRUCWPRYVHWWCWYAYXDWUT + WPWWCWYAQYXDQUERZUJRYXDJYXEQUJOUYGWWCYXDQWWCYXDWWCYVKYXDYHTZYWFGVVRWDZYNW + WCXGZXVDWWCXHVAZUYJWNZXFWWCGUCWUTYWGWWCUYQZWWCWUTWWSXDZYOWWCGWUTUCYWGYXLY + XKUYEYQVPXQVVPVVQYVDYUTYUOYVDYUTWYDJYCSZYUOWWCYXMYUNWWCWYAJWUTWWCWYAAWYAV + HTZWWBAWVOJVHTZYXNVGAGJLOVEZQJVVSWCZVPZYDWWCJAYXOWWBYXPVPYDZWWCWUTWWSYGWW + CWYAJWPRJWUTYCWWCWYAJJAJUSTWWBAJYXPWTZVPZYYAWWCJYYAVVTVWAWWCJWUSYCSZJWUTY + CSZWWCJGQUERZWUSYXSWWCGYWFYEZYWMWWCJYYDYXSYYEWWCJYXEYYDXBOWWCYXDGXBSZYXEY + YDXBSZWWCGYWFVWBWWCYXFYVKXXMXXNYYFYYGXPYXGYWFXXMWWCUXAVAZXXNWWCUXGVAZYXDG + QVWGYLYMUXSVWHWWCYYDYWHFUERZWUSYCWWCYYDFUJRZYWHYCSZYYDYYJYCSZWWCYYKGFQUER + ZUJRZYWHYCWWCGQFYWGYXHXVBYXIVWCWWCYYNWURYCSZYYOYWHYCSZWWCYYPFQWURUJRZYCSZ + WWCYYSXYKYYRXBSZWWCXYPWURXBSZYYTWWCXYPIWURXBNWWCWULWUQXBSZIWURXBSZWWCWULW + UNWUQWWCIAXWTWWBXXAVPZYEWWCWUNAWUNVDTWWBWVTVPYGWWCWUQWWPYGZWWCWVPWULWUNXB + SAWVPWWBWVSVPWULVWDWDWWBWUNWUQYCSAWUQWUNIVWEWAVWFWWCXWTWUQYHTZXXMXXNUUUBU + UUCXPUUUDUUUEYYHYYIIWUQQVWIYLYMZVWJWWCXYKYHTZWURYHTZXXMXXNUUUAYYTXPWWCYWN + UUUHWWCFWWKYDZFVVRWDZYWLYYHYYIXYKWURQVWIYLYMAXYQWWBYYRVDTZYYSYYTXPXYSWWCW + WMWWLUUULVSWWQQWURWBWCFYYRVWKVQYKWWCYWNUUUIXXMXXNYYPYYSXPUUUJYWLYYHYYIFWU + RQVWLYLYKWWCYYNYHTUUUIYVKVBGXBSZYYPYYQXPWWCFUUUJYEYWLYWFWWCGYWTYPZYYNWURG + UXTYLYMYSWWCYYDYHTYWHYHTZYWNYWOYYLYYMXPYYEWWCGWURYWFYWLVVCZUUUJWWCFWWKYPZ + YYDYWHFVWMYLYMWWCGWURFYWGXVCXVBYWJVWNZUXEVWPWWCWWFJVDTZYYBYYCXPWWRAUUUSWW + BAJYXPVFZVPWUSJVWQWEYMYSVWOVPYVDYVLWYDYHTJYHTYUTYXMVNYUOXRYVOYVDWYDWWCWYD + VDTZYUNWWCWYAWUTWWCWYAYXRVFZWWSWRZVPYGYVDJAYXOWWBYUNYXPXLYDXUBWYDJVWRXSXT + VWSVWTVXAVPVXBYUMXUDYUPXUGYURYUMXUCXUDYUPYUMXUAXUCYUMWYTWYFWYOWWCYUFYAZWW + CWYFWYOTZYUFWWCUUVEWYFVHTZWYFIYCSZWWCWYNVBWYFXBSZUUVFWWCFWURAXYQWWBXYSVPW + WQWRZWWCWURFXBSZUUVHWWCWURXYKFYWLUUUKUUUJWWCWURXYKYCSZWUQXYPYCSZWWCWUQIXY + PYCWWBWUQIYCSAWUQWUNIYJWANVXCWWCUUUFUUUHXXMXXNUUVKUUVLXPUUUEUUUKYYHYYIWUQ + XYKQVXDYLYKWWCFUUUJVWBUXIZWWCWURFYWLUUUJVXFYMWYFVXEVXGWWCUUVGWYFUCWPRZIXB + SZWWCUUVNXYKWURWPRIXBWWCFWURUCXVBXVCYXKYOWWCXYKIWURUUUKUUUDYWLWWCXYKIWPRZ + IWURXBWWCIIUHRZIWPRUUVPIWWCUUVQXYKIWPWWCUUVQXYPXYPUHRXYKIXYPIXYPUHNNVXHWW + CXYKWWCXYKWWCXYQXYRXULXYTWDXDUXCWNXFWWCIIAXXRWWBXXSVPZUUVRVXIVXJUUUGYSVXK + YSWWCWYNWVNUUVGUUVOXPUUVIWWCIAXWNWWBWVQVPVFZWYFIVWKWEYKWWCWVNUUVEUUVFUUVG + VNXPUUVSWYFIYTWDVXLVPYIVXOYUMUUUSXUCYUPXPAUUUSWWBYUFUUUTXLXUBJYTWDVXMYUMX + UFYUQXUEXBYUMWYTWYFGUJUUVDXFXQVXNYUMUUVAYUIYVAXPWWCUUVAYUFUUVCVPXUBWYDYTW + DVVPVXBVXAYUKYUFYUHWYGYUFDYUGHWVCYUGWKWVDWYTWYFWYTXUBWVCBVXPCVXPVXQVXRWSV + XSYULWYTYUATZYUIVNYUJWYTXUBYUAYUBVXTUUVTYUFYUIBWYFVYAVYBVUMVYCVYDZVUBWWCY + UDYUEWKZYUCYUBVYESZWWCWYNYUBWJTZUUWCUUVIWWCUCWYDWWCVYFUUVCVMZWYFYUBVDWJVY + GWEWWCYUCWJTUUWDUUWBUUWCXPWWCWYHYUCWJUUWAXUMUXPUUWEYUCYUBVYHWEYKWWCWYAWUT + XMUGTZWYDWGTYUEWYDWKWWCYXCWYAVDTWUTWYAYCSUUWFWWSUUVBWWCWUTYXDWYAYCWWCWUTG + XBSZWUTYXDYCSZWWCWUSGXBSZUUWGWWCYYJWUSGXBUUURWWCYYJGXBSZYWHYWDXBSZWWCUUVJ + UUWKUUVMWWCUUUIYWNYVKUUUMUUVJUUWKXPYWLUUUJYWFUUUNWURFGVYIYLYMWWCUUUOYVKYW + NYWOUUWJUUWKXPUUUPYWFUUUJUUUQYWHGFVYJYLYKVYKWWCWWFWWGUUWIUUWGXPWWRYXAWUSG + VVNWEYMWWCYXCWWGUUWGUUWHXPWWSYXAWUTGVYLWEYMYXJVYMWUTWYAVYNVYOWUTWYAVYPWYD + VYQYBYQVYRUYMAWUOWYAWUTEWWAAWYAUSTZWWBAWYAYXQWTZVPYXLVYSVXJWOAWVAWYBAWVAW + WTXDAWYBAWUOWYAEWWAUUVBWFXDVYTAWYBWXOWYAUJRZWXQAWUOWJTZUUWLWYBUUWNWKWWAUU + WMWUOWYAEWUDWEAWXOQJAWXOAUUWOWXOWGTWWAWUOWHWDZWUAAXGYXTWUBXOYQWOAWVJWVLWW + MWXPVDTZWXRWXTWKWVKWVMWWMAVSVAAWXOJAWXOUUWPWIUUUTWUCZWUKQWXPWUEWUFAWXTUCW + XPULRZUCWXSUCWXPULWUGWMAUUWQUUWSUCWKUUWRWXPWUHWDWNYQVVDAWVJWVLWVAVDTWVHVD + TWXHWXIWKWVKWVMWWTWXDWUKWVAWVHWUIWUFUYKWUJ $. + + $( Lemma for ~ lgsquad . Count the members of ` S ` with even coordinates, + and combine with ~ lgsquadlem1 to get the total count of lattice points + in ` S ` (up to parity). (Contributed by Mario Carneiro, + 18-Jun-2015.) $) + lgsquadlem2 $p |- ( ph -> ( Q /L P ) = ( -u 1 ^ ( # ` S ) ) ) $= + ( co c1 c2 clt wbr wcel vu vz vv cmin cdiv cfz cv cmul cfl cfv cexp caddc + csu chash oveq2i cin c0 wceq cz cn gausslemma2dlem0b nnzd 2nn znq sylancl + cq flqcld syl cc0 wo cun cn0 cle nnrpd rpge0d flqge0nn0 syl2anc nnred crp + rphalflt wb mpbid cuz eleqtrdi eqtrdi oveq1 oveq1d 1zzd gausslemma2dlem0a + 0p1e1 fzfigd wa adantr elfznn adantl sylancr oveq2d c1st cdvds crab wn cc + a1i sseqtrrid sselda syldan fsumnn0cl expaddd cfn hashcl wdc cxp elfzelzd + ralrimiva ssfirab csn mpbird wrel bitri wne ad2antrr rehalfcld cr elfzle2 + flqge syl2an 2re 2pos syl112anc peano2rem eqbrtrid wi cprime mpan2d simpr + syl3anc nngt0d nncnd wral wrex clgs cneg lgseisen sumeq1i ltp1d rphalfcld + zred fzdisj nnnn0d flqlt ltled elfz2nn0 syl3anbrc nn0uz elfzp12 un0 uncom + eqtr3i oveq2 fz10 uneq12d eqtr4id fzsplit oveq1i jaoi syl2an2r nnmulcl zq + eleq2s qmulcl rpdivcld rpmulcld nn0cnd eqtr3id neg1cn ssun2 lgsquadlemofi + fsumsplit peano2zd ssun1 lgsquadlemsfi copab opabssxp eqsstri sseli xp1st + dvdsdc ciun cen nn0zd xpsnen2g snfig xpfi hashen wss ssrab2 relopabiv mp2 + relss relxp cop eleq2i opabidw anass elfzelz lemuldiv2 ltm1d ltdiv1 lttrd + lelttrd zltnle eldifad prmz dvdsle mtod cgcd prmrp coprmdvds nnz dvdsmul2 + breq2 syl5ibrcom necon3bd nnmulcld zltlen mpbiran2d nnre lemuldiv gt0ap0d + mpd div23apd breq2d 3bitrd ltmul2 cap w3a divassap div23ap eqtr3d breqtrd + 2cnd remulcld lttr ltmul1 sylibrd recnd divsubdirapd eqtr4di ax-1cn nncan + halflt1 eqbrtrdi eqbrtrrd 1red ltsubadd2d peano2re syld nnleltp1 pm4.71rd + 3bitr3d bitrid nnuz elfz5 eqeltrd biantrurd fznn bitr3d mulcomd sylan9eqr + pm5.32da anbi12d 3bitr4d op1std eqeq2d eqcom bitrdi elrab biancomi opelxp + vex velsn anbi1i 3bitr4g eqrelrdv eqcomd fveq2d hashfz1 3eqtr3rd sumeq2dv + zdceq simprbi ad2antll adantrr 2ap0 divcanap3d ralrimivva invdisj hashiun + wdisj iunrab 2cn zcn mulcom eqeq1d rexbidva anim1i reximi2 simprr eqbrtrd + fveq2 sselid zre ad2antrl simprl 2t0e0 0red elnnz sylanbrc jca ex impbid2 + reximdv2 divides rabbidva eqtrid 3eqtr2d lgsquadlem1 oveq12d eqtr4d inrab + pm3.24 ralrimivw rabeq0 sylibr hashun unrab rabid2 exmiddc mprgbir eqtr4i + 2z fveq2i eqtr3di 3eqtrd ) AEDUUAOPUUBZPDPUDOZQUEOZUFOZEDUEOZQUAUGZUHOZUH + OZUIUJZUAUMZUKOWUEPGQUEOZUIUJZUFOZWUMUAUMZWUPPULOZGUFOZWUMUAUMZULOZUKOZWU + EFUNUJZUKOZAUADEIJKUUCAWUNWVBWUEUKAWUNPGUFOZWUMUAUMWVBWVFWUHWUMUAGWUGPUFL + UOUUDAWUQWUTWUMWVFUAAWUPWUSRSWUQWUTUPUQURAWUPAWUPAWUOAGUSTZQUTTZWUOVFTZAG + ADGILVAZVBZVCGQVDVEZVGZUUGZUUEPWUPWUSGUUHVHAWUPVIURZWUPVIPULOZGUFOZTZVJZW + VFWUQWUTVKZURZAWUPVIGUFOTZWVSAWUPVLTZGVLTWUPGVMSWWBAWVIVIWUOVMSWWCWVLAWUO + AGAGWVJVNZUUFVOWUOVPVQAGWVJUUIZAWUPGWVNAGWVJVRZAWUOGRSZWUPGRSZAGVSTWWGWWD + GVTVHAWVIWVGWWGWWHWAWVLWVKWUOGUUJVQWBUUKWUPGUULUUMAGVIWCUJZTWWBWVSWAAGVLW + WIWWEUUNWDWUPVIGUUOVHWBWVOWWAWVRWVOWVFUQWVFVKZWVTWVFUQVKWVFWWJWVFUUPWVFUQ + UUQUURWVOWUQUQWUTWVFWVOWUQPVIUFOUQWUPVIPUFUUSUUTWEWVOWUSPGUFWVOWUSWVPPWUP + VIPULWFWJWEWGUVAUVBWWAWUPWVFWVQWUPPGUVCWVPPGUFWJUVDUVIUVEVHZAPGAWHZWVKWKA + WUJWVFTZWLZWUMWWNWULVFTZVIWULVMSWUMVLTZWWNWUIVFTZWUKVFTZWWOAEUSTZWWMDUTTZ + WWQAEAEJWIZVBAWWTWWMADIWIZWMEDVDUVFWWNWUKUSTZWWRWWNWUKWWNWVHWUJUTTZWUKUTT + ZVCWWMWXDAWUJGWNWOQWUJUVGWPZVBZWUKUVHVHWUIWUKUVJVQZWWNWULWWNWUIWUKAWUIVST + WWMAEDAEWXAVNADWXBVNUVKWMWWNWUKWXFVNUVLVOWULVPVQZUVMUVRUVNWQAWVCWUEWURUKO + ZWUEWVAUKOZUHOZWUEQUBUGZWRUJZWSSZUBFWTZUNUJZWXOXAZUBFWTZUNUJZULOZUKOZWVEA + WUEWURWVAWUEXBTAUVOXCZAWUTWUMUAAWUSGAWUPWVMUVSWVKWKAWUJWUTTWWMWWPAWUTWVFW + UJAWVTWUTWVFWUTWUQUVPWWKXDXEWXIXFXGAWUQWUMUAAPWUPWWLWVMWKZAWUJWUQTZWWMWWP + AWUQWVFWUJAWVTWUQWVFWUQWUTUVTWWKXDXEZWXIXFZXGXHAWYBWUEWXQUKOZWUEWXTUKOZUH + OWXLAWUEWXQWXTWYCAWXSXITZWXTVLTABCUBDEFGHIJKLMNUVQZWXSXJVHAWXPXITZWXQVLTA + WXOUBFABCDEFGHIJKLMNUWAZAWXOXKZUBFAWXMFTZWLZWVHWXNUSTZWYNVCWYOWYQAWYOWXNP + GWYOWXMWVFPHUFOZXLZTZWXNWVFTZFWYSWXMFBUGZWVFTZCUGZWYRTZWLZXUDDUHOZXUBEUHO + ZRSZWLZBCUWBZWYSNXUIBCWVFWYRUWCUWDZUWEWXMWVFWYRUWFZVHXMZWOQWXNUWGZWPXNXOZ + WXPXJVHXHAWXJWYHWXKWYIUHAWURWXQWUEUKAWURWUQWUKWXNURZUBFWTZUNUJZUAUMUAWUQX + URUWHZUNUJWXQAWUQWUMXUSUAAWYEWLZWUKXPZPWUMUFOZXLZUNUJZXVCUNUJZXUSWUMXVAXV + EXVFURZXVDXVCUWISZXVAWXEXVCXITZXVHAWYEWWMWXEWYFWXFXFZXVAPWUMXVAWHXVAWUMWY + GUWJWKZWUKXVCUTXIUWKVQXVAXVDXITZXVIXVGXVHWAXVAXVBXITZXVIXVLXVAWXEXVMXVJWU + KUTUWLVHXVKXVBXVCUWMVQXVKXVDXVCUWNVQXQXVAXVDXURUNXVAXURXVDXVABCXURXVDXURF + UWOFXRXURXRXUQUBFUWPXUJBCFNUWQXURFUWSUWRXVBXVCUWTXVAXUBWUKURZXUBXUDUXAZFT + ZWLXVNXUDXVCTZWLZXVOXURTZXVOXVDTZXVAXVNXVPXVQXVPXUJXVAXVNWLZXVQXVPXVOXUKT + XUJFXUKXVONUXBXUJBCUXCXSXWAXUDUTTZXUDHVMSZWLZXUGEWUKUHOZRSZWLZXWBXUDWUMVM + SZWLZXUJXVQXVAXWGXWIWAXVNXWGXWBXWCXWFWLZWLXVAXWIXWBXWCXWFUXDXVAXWBXWJXWHX + VAXWBWLZXWFXUDWULVMSZXWJXWHXWKXWFXUGXWEVMSZXUDXWEDUEOZVMSZXWLXWKXWFXWMXWE + XUGXTZXWKDXWEWSSZXAXWPXWKXWQDWUKWSSZXWKXWRDWUKVMSZXWKWUKDRSZXWSXAZXWKWUKD + QUEOZDXWKWUKXVAWXEXWBXVJWMZVRZXWKDXWKDAWWTWYEXWBWXBYAZVRZYBZXXFXWKWUKGXXB + XXDXVAGYCTZXWBAXXHWYEWWFWMZWMXXGXVAWUKGVMSZXWBXVAXXJWUJWUOVMSZXVAXXKWUJWU + PVMSZWYEXXLAWUJPWUPYDWOAWVIWUJUSTZXXKXXLWAZWYEWVLWUJPWUPUXEZWUOWUJYEZYFXQ + XVAWUJYCTZXXHQYCTZVIQRSZXXJXXKWAZXVAWUJWYEWXDAWUJWUPWNWOZVRXXIXXRXVAYGXCX + XSXVAYHXCWUJGQUXFZYIXQZWMXWKGWUGXXBRLXWKWUFDRSZWUGXXBRSZXWKDXXFUXGXWKWUFY + CTZDYCTZXXRXXSXYDXYEWAXWKXYGXYFXXFDYJVHXXFXXRXWKYGXCZXXSXWKYHXCZWUFDQUXHY + IWBYKUXJZXWKDVSTXXBDRSXWKDXXEVNDVTVHUXIXWKWXCDUSTZXWTXXAWAXWKWUKXXCVBZXWK + DXXEVBWUKDUXKVQWBXWKXYKWXEXWRXWSYLXWKDYMTZXYKAXYMWYEXWBADYMQXPZIUXLZYADUX + MVHZXXCDWUKUXNVQUXOXWKXWQDEUXPOPURZXWRAXYQWYEXWBAXYQDEXTZKAXYMEYMTZXYQXYR + WAXYOAEYMXYNJUXLZDEUXQVQXQYAXWKXYKWWSWXCXWQXYQWLXWRYLXYPXWKXYSWWSAXYSWYEX + WBXYTYAEUXMVHXYLDEWUKUXRYPYNUXOXWKXWQXWEXUGXWKXWQXWEXUGURDXUGWSSZXWKXUDUS + TZXYKYUAXWBYUBXVAXUDUXSZWOXYPXUDDUXTVQXWEXUGDWSUYAUYBUYCUYJXWKXUGUSTXWEUS + TXWFXWMXWPWLWAXWKXUGXWKXUDDXVAXWBYOZXXEUYDZVBXWKXWEXVAXWEUTTXWBXVAEWUKAEU + TTZWYEWXAWMZXVJUYDWMZVBXUGXWEUYEVQUYFXWKXUDYCTZXWEYCTZXYGVIDRSZXWMXWOWAXW + BYUIXVAXUDUYGWOZXWKXWEYUHVRZXXFXWKDXXEYQZXUDXWEDUYHYIXWKXWNWULXUDVMXWKEWU + KDXWKEXVAYUFXWBYUGWMZYRZXWKWUKXXCYRXWKDXXEYRZXWKDXXFYUNUYIUYKUYLUYMXWKXWF + XWCXWKXWFXUDHPULOZRSZXWCXWKXWFXUDEQUEOZRSZYUSXWKXWFXUGYUTDUHOZRSZYVAXWKXW + FXWEYVBRSZYVCXWKXWEEXXBUHOZYVBRXWKWUKXXBRSZXWEYVERSZXYJXWKWUKYCTXXBYCTEYC + TZVIERSYVFYVGWAXXDXXGXWKEYUOVRZXWKEYUOYQWUKXXBEUYNYIWBXWKEXBTZDXBTZQXBTZQ + VIUYOSZYVEYVBURYUPYUQXWKVUAZXWKQXYHXYIUYIZYVJYVKYVLYVMWLUYPEDUHOQUEOYVEYV + BEDQUYQEDQUYRUYSYIUYTXWKXUGYCTYUJYVBYCTXWFYVDWLYVCYLXWKXUGYUEVRYUMXWKYUTD + XWKEYVIYBZXXFVUBXUGXWEYVBVUCYPYNXWKYUIYUTYCTZXYGYUKYVAYVCWAYULYVPXXFYUNXU + DYUTDVUDYIVUEXWKYVAYUTYURRSZYUSXWKYUTHUDOZPRSYVRXWKEEPUDOZUDOZQUEOZYVSPRX + WKYWBYUTYVTQUEOZUDOYVSXWKEYVTQYUPXWKYVTXWKYVHYVTYCTYVIEYJVHVUFYVNYVOVUGHY + WCYUTUDMUOVUHXWKYWBPQUEOPRXWKYWAPQUEXWKYVJPXBTYWAPURYUPVUIEPVUJVEWGVUKVUL + VUMXWKYUTHPYVPXWKHAHUTTZWYEXWBAEHJMVAZYAZVRZXWKVUNVUOWBXWKYUIYVQYURYCTZYV + AYVRWLYUSYLYULYVPXWKHYCTYWHYWGHVUPVHXUDYUTYURVUCYPYNVUQXWKXWBYWDXWCYUSWAY + UDYWFXUDHVURVQVUEVUSXVAWWOYUBXWLXWHWAXWBAWYEWWMWWOWYFWXHXFZYUCWULXUDYEYFV + UTVVJVVAWMXWAXUFXWDXUIXWFXWAXUEXUFXWDXWAXUCXUEXWAXUBWUKWVFXVAXVNYOXVAWUKW + VFTZXVNXVAYWJXXJXYCXVAWUKPWCUJZTWVGYWJXXJWAXVAWUKUTYWKXVJVVBWDAWVGWYEWVKW + MWUKPGVVCVQXQWMVVDVVEXWAHUSTZXUEXWDWAAYWLWYEXVNAHYWEVBYAXUDHVVFVHVVGXWAXU + HXWEXUGRXVNXVAXUHWUKEUHOXWEXUBWUKEUHWFXVAWUKEXVAWUKXVJYRXVAEYUGYRVVHVVIUY + LVVKXVAXVQXWIWAZXVNXVAWUMUSTYWMXVAWULYWIVGXUDWUMVVFVHWMVVLVVAVVJXVSXVNXVP + XUQXVNUBXVOFWXMXVOURZXUQWUKXUBURXVNYWNWXNXUBWUKXUBXUDWXMBVVTCVVTVVMVVNWUK + XUBVVOVVPVVQVVRXVTXUBXVBTZXVQWLXVRXUBXUDXVBXVCVVSYWOXVNXVQBWUKVWAVWBXSVWC + VWDVWEVWFXVAWWPXVFWUMURWYGWUMVWGVHVWHVWIAUAWUQXURWYDXVAXUQUBFAFXITWYEWYMW + MXVAXUQXKZUBFXVAWXCWYQYWPWYOAWYEWWMWXCWYFWXGXFXUNWUKWXNVWJYFXNXOAUCUGZWRU + JZQUEOZWUJURZUCXURYSUAWUQYSUAWUQXURVWSAYWTUAUCWUQXURAWYEYWQXURTZWLWLZWUKQ + UEOYWSWUJYXBWUKYWRQUEYXAWUKYWRURZAWYEYXAYWQFTYXCXUQYXCUBYWQFWXMYWQURWXNYW + RWUKWXMYWQWRVXJVVNVVQVWKVWLWGYXBWUJQAWYEWUJXBTZYXAXVAWUJXYAYRVWMYXBVUAYVM + YXBVWNXCVWOUYSVWPUAUCWUQXURYWSVWQVHVWRAXUTWXPUNAXUTXUQUAWUQYTZUBFWTWXPXUQ + UAUBWUQFVWTAYXEWXOUBFWYPXUQUAUSYTZWUJQUHOZWXNURZUAUSYTZYXEWXOWYPXUQYXHUAU + SWYPXXMWLZWUKYXGWXNYXJYVLYXDWUKYXGURVXAXXMYXDWYPWUJVXBWOQWUJVXCWPVXDVXEWY + PYXEYXFXUQXUQUAWUQUSWYEXXMXUQXXOVXFVXGWYPXUQXUQUAUSWUQWYPXXMXUQWLZWYEXUQW + LWYPYXKWLZWYEXUQYXLWYEXXLYXLXXKXXLYXLXXJXXKYXLWUKWXNGVMWYPXXMXUQVXHZYXLXU + AWXNGVMSWYPXUAYXKWYPWYTXUAWYPFWYSWXMXULAWYOYOVXKXUMVHZWMZWXNPGYDVHVXIYXLX + XQXXHXXRXXSXXTXXMXXQWYPXUQWUJVXLVXMZAXXHWYOYXKWWFYAXXRYXLYGXCZXXSYXLYHXCZ + XYBYIWBYXLWVIXXMXXNAWVIWYOYXKWVLYAWYPXXMXUQVXNZXXPVQWBYXLWUJYWKTWUPUSTZWY + EXXLWAYXLWUJUTYWKYXLXXMVIWUJRSZWXDYXSYXLYYAQVIUHOZWUKRSZYXLYYBVIWUKRVXOYX + LWUKYXLWUKWXNUTYXMYXLXUAWXNUTTYXOWXNGWNVHVVDYQYKYXLVIYCTXXQXXRXXSYYAYYCWA + YXLVXPYXPYXQYXRVIWUJQUYNYIXQWUJVXQVXRVVBWDAYXTWYOYXKWVMYAWUJPWUPVVCVQXQYX + MVXSVXTVYBVYAWYPQUSTWYQWXOYXIWAWUAWYPWXNPGYXNXMUAQWXNVYCWPVVLVYDVYEVWFVYF + WQABCUBUADEFGHIJKLMNVYGVYHVYIAWYAWVDWUEUKAWXPWXSVKZUNUJZWYAWVDAWYLWYJWXPW + XSUPZUQURYYEWYAURXUPWYKAYYFWXOWXRWLZUBFWTZUQWXOWXRUBFVYJAYYGXAZUBFYSYYHUQ + URAYYIUBFYYIAWXOVYKXCVYLYYGUBFVYMVYNVYEWXPWXSVYOYPYYDFUNYYDWXOWXRVJZUBFWT + ZFWXOWXRUBFVYPFYYKURYYJUBFYYJUBFVYQWYOWYNYYJWYOWVHWYQWYNVCXUNXUOWPWXOVYRV + HVYSVYTWUBWUCWQVYFWUD $. + + $d M j x y $. $d N j x y $. $d P j x y $. $d Q j x y $. + $( Lemma for ~ lgsquad . (Contributed by Mario Carneiro, 18-Jun-2015.) $) + lgsquadlem3 $p |- ( ph -> + ( ( P /L Q ) x. ( Q /L P ) ) = ( -u 1 ^ ( M x. N ) ) ) $= + ( co cmul c1 wcel wa syl vw vz vj clgs cneg cv cfz clt wbr copab cfv cexp + chash caddc necomd weq wb eleq1w bi2anan9 biancomd oveq1 breqan12d ancoms + anbi12d cbvopabv lgsquadlem2 wceq cen ccnv cfn relopabv gausslemma2dlem0b + wrel eqid 1zzd nnzd fzfigd wdc cz cn elfznn ad2antrl cprime c2 csn adantr + eldifad prmnn nnmulcld ad2antll gausslemma2dlem0a zdclt ralrimivva opabfi + syl2anc cnven sylancr cnvopab breqtrdi lgsquadlemsfi hashen mpbird oveq2d + eqtr4d oveq12d cc neg1cn a1i cn0 hashcl expaddd cun cxp wo wne cdvds cmin + wn cuz wss cle prmz nnred wi elfzelz syl3anc nncnd cq nnq opabbii 3eqtr4i + ex cin c0 wex cr sylib nexdv nnnn0d hashfz1 peano2zm zred cdiv crp prmuz2 + uz2m1nn nnrpd rphalflt eqbrtrid ltled eluz2 syl3anbrc fzss2 simprr sseldd + fzm1ndvds cgcd prmrp coprmdvds mpan2d mulcomd breq2d mtbid dvdsmul2 breq2 + mtod syl5ibcom necon3bd mpd qlttri2 mpbid pm4.71rd ancom bitr2di opabbidv + unopab uneq2i andi df-xp 3eqtr4g fveq2d inopab ineq2i ltnsym2 imnan opabm + anandi sylnibr notm0 eqtrid hashun hashxp eqtrd 3eqtr3d 3eqtr2d ) ADEUDOZ + EDUDOZPOQUEZBUFZQGUGOZRZCUFZQHUGOZRZSZUWSEPOZUXBDPOZUHUIZSZBCUJZUMUKZULOZ + UWRFUMUKZULOZPOUWRUXKUXMUNOZULOUWRGHPOZULOAUWPUXLUWQUXNPAUWPUWRUXICBUJZUM + UKZULOUXLAUAUBEDUXQHGJIADEKUOZMLUXIUAUFZUXCRZUBUFZUWTRZSZUYBEPOZUXTDPOZUH + UIZSZCBUAUBBUBUPZCUAUPZUXIUYHUQUYIUYJSZUXEUYDUXHUYGUYKUXEUYAUYCUYIUXAUYCU + YJUXDUYABUBUWTURCUAUXCURUSUTUYIUYJUXFUYEUXGUYFUHUWSUYBEPVAUXBUXTDPVAVBVDV + CVEZVFAUXKUXRUWRULAUXKUXRVGZUXJUXQVHUIZAUXJUXJVIZUXQVHAUXJVMUXJVJRZUXJUYO + VHUIUXIBCVKAUXHBCUWTUXCUXJUXJVNAQGAVOZAGADGILVLZVPVQZAQHUYQAHAEHJMVLZVPVQ + ZAUXHVRZBCUWTUXCAUXESZUXFVSRUXGVSRVUBVUCUXFVUCUWSEUXAUWSVTRAUXDUWSGWAWBVU + CEWCRZEVTRZAVUDUXEAEWCWDWEZJWGWFZEWHTZWIZVPVUCUXGVUCUXBDUXDUXBVTRAUXAUXBH + WAWJZADVTRUXEADIWKWFZWIZVPUXFUXGWLWOWMWNZUXJVJWPWQUXIBCWRWSAUYPUXQVJRUYMU + YNUQVUMAUAUBEDUXQHGJIUXSMLUYLWTUXJUXQXAWOXBXCXDABCDEFGHIJKLMNVFXEAUWRUXKU + XMUWRXFRAXGXHAFVJRZUXMXIRABCDEFGHIJKLMNWTZFXJTAUYPUXKXIRVUMUXJXJTXKAUXOUX + PUWRULAUXJFXLZUMUKZUWTUXCXMZUMUKZUXOUXPAVUPVURUMAUXEUXHUXGUXFUHUIZXNZSZBC + UJZUXEBCUJVUPVURAVVBUXEBCAUXEVVAUXESVVBAUXEVVAAUXEVVAVUCUXFUXGXOZVVAVUCEU + XGXPUIZXRVVDVUCEDUXBPOZXPUIZVVEVUCVVGEUXBXPUIZVUCVUEUXBQEQXQOZUGOZRVVHXRV + UHVUCUXCVVJUXBVUCVVIHXSUKRZUXCVVJXTVUCHVSRVVIVSRZHVVIYAUIVVKVUCHAHVTRUXEU + YTWFZVPVUCEVSRZVVLVUCVUDVVNVUGEYBTZEUUATZVUCHVVIVUCHVVMYCVUCVVIVVPUUBVUCH + VVIWDUUCOZVVIUHMVUCVVIUUDRVVQVVIUHUIVUCVVIVUCEWDXSUKRZVVIVTRVUCVUDVVRVUGE + UUETEUUFTUUGVVIUUHTUUIUUJHVVIUUKUULHQVVIUUMTAUXAUXDUUNUUOEUXBUUPWOVUCVVGE + DUUQOQVGZVVHVUCVVSEDXOZAVVTUXEUXSWFVUCVUDDWCRZVVSVVTUQVUGAVWAUXEADWCVUFIW + GWFZEDUURWOXBVUCVVNDVSRZUXBVSRZVVGVVSSVVHYDVVOVUCVWAVWCVWBDYBTUXDVWDAUXAU + XBQHYEWJEDUXBUUSYFUUTUVFVUCVVFUXGEXPVUCDUXBVUCDVUKYGVUCUXBVUJYGUVAUVBUVCV + UCVVEUXFUXGVUCEUXFXPUIZUXFUXGVGVVEVUCUWSVSRZVVNVWEUXAVWFAUXDUWSQGYEWBVVOU + WSEUVDWOUXFUXGEXPUVEUVGUVHUVIVUCUXFYHRZUXGYHRZVVDVVAUQVUCUXFVTRVWGVUIUXFY + ITVUCUXGVTRVWHVULUXGYITUXFUXGUVJWOUVKYLUVLVVAUXEUVMUVNUVOUXJUXEVUTSZBCUJZ + XLUXIVWIXNZBCUJVUPVVCUXIVWIBCUVPFVWJUXJNUVQVVBVWKBCUXEUXHVUTUVRYJYKBCUWTU + XCUVSUVTUWAAUYPVUNUXJFYMZYNVGVUQUXOVGVUMVUOAVWLUXEUXHVUTSZSZBCUJZYNUXJVWJ + YMUXIVWISZBCUJVWLVWOUXIVWIBCUWBFVWJUXJNUWCVWNVWPBCUXEUXHVUTUWGYJYKAUCUFVW + ORUCYOZXRVWOYNVGAVWNCYOZBYOVWQAVWRBAVWNCAUXEVWMXRZYDVWNXRAUXEVWSVUCUXFYPR + UXGYPRVWSVUCUXFVUIYCVUCUXGVULYCUXFUXGUWDWOYLUXEVWMUWEYQYRYRVWNBCUCUWFUWHU + CVWOUWIYQUWJUXJFUWKYFAVUSUWTUMUKZUXCUMUKZPOZUXPAUWTVJRUXCVJRVUSVXBVGUYSVU + AUWTUXCUWLWOAVWTGVXAHPAGXIRVWTGVGAGUYRYSGYTTAHXIRVXAHVGAHUYTYSHYTTXEUWMUW + NXCUWO $. + $} + + ${ + $d w x y z P $. $d w x y z Q $. + $( The Law of Quadratic Reciprocity, see also theorem 9.8 in [ApostolNT] + p. 185. If ` P ` and ` Q ` are distinct odd primes, then the product of + the Legendre symbols ` ( P /L Q ) ` and ` ( Q /L P ) ` is the parity of + ` ( ( P - 1 ) / 2 ) x. ( ( Q - 1 ) / 2 ) ` . This uses Eisenstein's + proof, which also has a nice geometric interpretation - see + ~ https://en.wikipedia.org/wiki/Proofs_of_quadratic_reciprocity . This + is Metamath 100 proof #7. (Contributed by Mario Carneiro, + 19-Jun-2015.) $) + lgsquad $p |- ( ( P e. ( Prime \ { 2 } ) /\ Q e. ( Prime \ { 2 } ) + /\ P =/= Q ) -> ( ( P /L Q ) x. ( Q /L P ) ) = + ( -u 1 ^ ( ( ( P - 1 ) / 2 ) x. ( ( Q - 1 ) / 2 ) ) ) ) $= + ( vz vw vx vy c2 wcel cv c1 cmin co cdiv cfz wa cmul clt wbr eqid weq csn + cprime cdif wne w3a copab simp1 simp2 simp3 eleq1w bi2anan9 oveq1 anbi12d + breqan12rd cbvopabv lgsquadlem3 ) AUBGUAUCZHZBUQHZABUDZUECDABEIZJAJKLGMLZ + NLZHZFIZJBJKLGMLZNLZHZOZVEAPLZVABPLZQRZOZEFUFVBVFURUSUTUGURUSUTUHURUSUTUI + VBSVFSVMCIZVCHZDIZVGHZOZVPAPLZVNBPLZQRZOEFCDECTZFDTZOVIVRVLWAWBVDVOWCVHVQ + ECVCUJFDVGUJUKWCWBVJVSVKVTQVEVPAPULVAVNBPULUNUMUOUP $. $} $( The first supplement to the law of quadratic reciprocity. Negative one is diff --git a/mm_100.html b/mm_100.html index eabbace33..c0331d84d 100644 --- a/mm_100.html +++ b/mm_100.html @@ -266,7 +266,10 @@
  • 7. Law of Quadratic Reciprocity (lgsquad, by Mario Carneiro, 2015-06-19)
    • +href="mpeuni/lgsquad.html">lgsquad, by Mario Carneiro, 2015-06-19). +The intuitionistic logic explorer (iset.mm) database also includes lgsquad +(by Jim Kingdon, 2025-09-17)
  • 9. The Area of a Circle (~ opm , ~ opnzi + + opabn0 + ~ opabm + + df-so ~ df-iso @@ -15274,17 +15279,10 @@ ( DChr syntax) - - lgsquad including lemmas - none - apparently provable and we have a start - at ~ lgsquadlem1 - - lgsquad2 including lemmas none - the set.mm proof uses lgsquad + should be feasible now that we have ~ lgsquad @@ -15378,12 +15376,6 @@