metamath/valid/numbertheory-sqmod4in01d.mm (37 lines of code) (raw):

${ $d A i n z $. $d n ph $. numbertheory-sqmod4in01d.0 $e |- ( ph -> A e. ZZ ) $. $( (Contributed by Stanislas Polu, 12-Feb-2021.) $) numbertheory-sqmod4in01d $p |- ( ph -> ( ( A ^ 2 ) mod 4 ) e. { 0 , 1 } ) $= ( vn vi c2 cexp co c4 cmo cc0 wceq c1 wcel cz cmul oveq1d a1i eqtrd caddc vz wo cpr ceven codd zeoALTV syl wa cv wrex oveq2 eqeq2d eqeq1 eqcom syl6bb cbvrexv rexbidv syl5bbr dfeven4 elrab2 simprbi adantl oveq1 eqcomd 2cnd zcn sqmuld sq2 adantr cc 4cn ad2antlr sqcld mulcomd crp zsqcl 4pos elrpii jctir 4re wi mulmod0 ex rexlimdva rexbii bitr3i dfodd6 simpr simplr mulcld binom2 mpd 1cnd syl2anc mulid1d oveq2d mulassd eqtr3d eqtr4d oveq12d sq1 adddid 4z 2t2e4 zaddcld zmulcld zred 0red 1red zcnd 0mod mp1i modadd1d 0p1e1 1nn0 4nn addcld 1lt4 modidi orim12d ovex elpr sylibr ) ABFGHZIJHZKLZYEMLZUBZYEKMUCNA BUDNZBUENZUBZYHABONZYKCBUFUGAYIYFYJYGAYIYFAYIUHZFDUIZPHZBLZDOUJZYFYIYQAYIYL YQUAUIZFEUIZPHZLZEOUJZYQUABOUDUUBYRYOLZDOUJYRBLZYQUUCUUADEOYNYSLZYOYTYRYNYS FPUKZULUPUUDUUCYPDOUUDUUCBYOLYPYRBYOUMBYOUNUOUQURUAEUSUTVAVBYMYPYFDOYMYNONZ UHZYPYFUUHYPUHZYEYOFGHZIJHZKUUIUUKYEUUIUUJYDIJYPUUJYDLUUHYOBFGVCVBQVDUUIUUK IYNFGHZPHZIJHZKUUHUUKUUNLYPUUHUUJUUMIJUUGUUJUUMLYMUUGUUJFFGHZUULPHUUMUUGFYN UUGVEZYNVFZVGUUGUUOIUULPUUOILUUGVHRQSZVBQVIUUIUUNUULIPHZIJHZKUUIUUMUUSIJUUI IUULIVJNZUUIVKRUUIYNUUGYNVJNZYMYPUUQVLVMVNQUUIUULONZIVONZUHZUUTKLZUUGUVEYMY PUUGUVCUVDYNVPZIVTVQVRZVSVLUVEUVFWAUUIUULIWBRWLSSSWCWDWLWCAYJYGAYJUHZYOMTHZ BLZDOUJZYGYJUVLAYJYLUVLYRYTMTHZLZEOUJZUVLUABOUEUUDUVOBUVMLZEOUJZUVLUUDUVNUV PEOYRBUVMUMUQUVQBUVJLZDOUJUVLUVRUVPDEOUUEUVJUVMBUUEYOYTMTUUFQULUPUVRUVKDOBU VJUNWEWFUOUAEWGUTVAVBUVIUVKYGDOUVIUUGUHZUVKYGUVSUVKUHZYEUVJFGHZIJHZMUVTYDUW AIJUVTUWAYDUVTUVJBFGUVSUVKWHQVDQUVTUWBUUMIYNPHZTHZMTHZIJHZMUVTUUGUWBUWFLUVI UUGUVKWIZUUGUWAUWEIJUUGUWAUUJFYOMPHZPHZTHZMFGHZTHZUWEUUGYOVJNMVJNUWAUWLLUUG FYNUUPUUQWJZUUGWMYOMWKWNUUGUWJUWDUWKMTUUGUUJUUMUWIUWCTUURUUGUWIFYOPHZUWCUUG UWHYOFPUUGYOUWMWOWPUUGFFPHZYNPHUWCUWNUUGUWOIYNPUWOILUUGXDRQUUGFFYNUUPUUPUUQ WQWRWSWTUWKMLUUGXARWTSQUGUVTUWFIUULYNTHZPHZMTHZIJHZMUVTUWEUWRIJUVTUWDUWQMTU VSUWDUWQLUVKUVSUWQUWDUVSIUULYNUVAUVSVKRUVSYNUUGUVBUVIUUQVBZVMUWTXBVDVIQQUVT UWSMIJHZMUVTUWSKMTHZIJHUXAUVTUWQKMIUVTUWQUVTIUWPIONUVTXCRUVTUULYNUUGUVCUVIU VKUVGVLZUWGXEZXFXGUVTXHUVTXIUVDUVTUVHRZUVTUWQIJHZKKIJHZUVTUXFUWPIPHZIJHZKUV TUWQUXHIJUVTIUWPUVAUVTVKRUVTUULYNUVTUULUXCXJUUGUVBUVIUVKUUQVLXQVNQUVTUWPONU VDUXIKLUXDUXEUWPIWBWNSUVTUXGKUVDUXGKLUVTUVHIXKXLVDSXMUVTUXBMIJUXBMLUVTXNRQS UXAMLUVTMIXOXPXRXSRSSSSWCWDWLWCXTWLYEKMYDIJYAYBYC $. $}