metamath/valid/numbertheory-prmdvsneqnsqmodpeq0.mm (76 lines of code) (raw):

${ $d N x y $. $d P x y $. $d ph x y $. numbertheory-prmdvsneqnsqmodpeq0.0 $e |- ( ph -> N e. ZZ ) $. numbertheory-prmdvsneqnsqmodpeq0.1 $e |- ( ph -> P e. Prime ) $. $( (Contributed by Kunhao Zheng, 29-Mar-2021.) $) numbertheory-prmdvsneqnsqmodpeq0 $p |- ( ph -> ( P || N <-> ( ( N ^ 2 ) mod P ) = 0 ) ) $= ( vx cdvds wbr c2 co wceq wa wcel adantr syl simpr ad2antrr zmulcld mpdan cz vy cexp cmo cc0 cmul cc zcnd sqvald oveq1d cn cprime prmnn id simpl 3jca wi mulmoddvds 3impia syl2an3an eqtrd ex cgcd prmz gcddvds syl2anc simpld caddc w3a wrex bezout cmin cdiv oveq1 ad3antrrr nncnd zcn ad2antlr mulcld pncan2d cv adantl sylan9eqr ad4antr sqmuld sqcld wne nnne0d div23d crp zred resqcld cr wb nnrpd biimpa zsqcl eqeltrd jca adantllr reximdva simp3l simp3r simprr mod0 imp gcdcld nn0zd zsubcld dvdsval2 syl3anc bicomd mpbid 3impa reximdvai 3exp adantlr ax-1 3ad2ant1 nn0cnd ad5antr simpllr binom2sub breq2d 3adantr2 com12 jcad simplrl iddvds dvdsmultr1d simprl 2z a1i breqtrd mulcomd adantrl 3syl 2cnd anassrs c1 wn eqcomd adantrr mp2and simplr zaddcld dvds2subd 2nn0 cn0 nn0expcld subcld pncand dvdsmul1 syl2an zmulcl sylancr dvds2addd npcand rexlimdvva ad4ant14 an32s nprmdvds1 simplrr sq1 syl6eq mtand gcdcom intnand wo neneqd gcdn0cl syl21anc dvdsprime orcomd ord mpd simprd eqbrtrrd impbid ) ABCGHZCIUBJZBUCJZUDKZAUVSUWBAUVSLZUWACCUEJZBUCJZUDUWCUVTUWDBUCUWCCACUFMZU VSACDUGZNUHUIABUJMZCTMZUVSUVSUWEUDKZABUKMZUWHEBULZOZDUVSUMUWHUWIUVSUWJUWHUW ILZUWHUWIUWIVHUVSUWJUPUWNUWHUWIUWIUWHUWIUNUWHUWIPZUWOUOCCBUQOURUSUTVAAUWBUV SAUWBLZBCVBJZBKZUVSUWPUWQBGHZUWRAUWSUWBAUWSUWQCGHZABTMZUWIUWSUWTLAUWKUXAEBV CZOZDBCVDVEZVFNUWPUWSLZUWQBFVTZUEJZCUAVTZUEJZVGJZKZUATVIZFTVIZUWRUXEUXAUWIU XMAUXAUWBUWSUXCQAUWIUWBUWSDQFUABCVJVEUXEUXMLUXKUWQUXGVKJZIUBJZBVLJZTMZLZUAT VIZFTVIZUWRUXEUXMUXTUXEUXLUXSFTUXEUXFTMZLZUXKUXRUATUWPUYAUXHTMZUXKUXRUPUWSU WPUYALZUYCLZUXKUXRUYEUXKLZUXKUXQUYEUXKPUYFUXPUXIIUBJZBVLJZTUYFUXOUYGBVLUYFU XNUXIIUBUXKUYEUXNUXJUXGVKJUXIUWQUXJUXGVKVMUYEUXGUXIUYEBUXFUYEBAUWHUWBUYAUYC UWMVNVOUYAUXFUFMUWPUYCUXFVPVQVRUYECUXHAUWFUWBUYAUYCUWGVNUYCUXHUFMZUYDUXHVPZ WAVRVSWBUIUIUYFUYHUVTBVLJZUXHIUBJZUEJZTUYFUYHUVTUYLUEJZBVLJUYMUYFUYGUYNBVLU YFCUXHUYFCAUWIUWBUYAUYCUXKDWCUGUYCUYIUYDUXKUYJVQZWDUIUYFUVTUYLBAUVTUFMUWBUY AUYCUXKACUWGWEWCUYFUXHUYOWEUYFBUYFUWKUWHAUWKUWBUYAUYCUXKEWCUWLOVOABUDWFZUWB UYAUYCUXKABUWMWGZWCWHUTUYFUYKUYLUYDUYKTMZUYCUXKUWPUYRUYAAUWBUYRAUVTWLMBWIMU WBUYRWMACACDWJWKABUWMWNUVTBXDVEWONQUYCUYLTMUYDUXKUXHWPVQRWQWQWRVAWSWTWTXEUX EUXTUWRUXMUXEUXTLUXKUXQBUXOGHZVHZUATVIZFTVIZUWRAUWSUXTVUBUWBAUXTVUBUWSAUXTV UBAUXSVUAFTAUYALZUXRUYTUATVUCUYCUXRUYTVUCUYCUXRVHUXKUXQUYSVUCUYCUXKUXQXAVUC UYCUXKUXQXBVUCUYCUXRUYSVUCUYCLZUXRLZUXQUYSVUDUXKUXQXCVUEUYSUXQVUEUXAUYPUXOT MZUYSUXQWMAUXAUYAUYCUXRUXCVNAUYPUYAUYCUXRUYQVNVUEUXNTMVUFVUEUWQUXGAUWQTMZUY AUYCUXRAUWQABCUXCDXFZXGZVNVUDUXGTMZUXRVUCVUJUYCVUCBUXFAUXAUYAUXCNAUYAPRNNXH UXNWPOBUXOXIXJXKXLXMUOXOXNWTXEXPWSUXEVUBUWRUXTUXEVUBLZBUWQIUBJZGHZUWRVUKUXK BVULIUWQUXGUEJZUEJZVKJZUXGIUBJZVGJZGHZLZUATVIZFTVIZVUMUXEVUBVVBUXEVUAVVAFTU YBUYTVUTUATUYBUYCLZUYTUXKVUSUYTVVCUXKUXKUXQVVCUXKUPUYSUXKVVCXQXRYEVVCUYTVUS VVCUXKUYSVUSUXQVVCUXKUYSLZLZUYSVUSVVCUXKUYSXCVVEUXOVURBGVVEUWQUFMZUXGUFMUXO VURKUWPVVFUWSUYAUYCVVDAVVFUWBAUWQVUHXSNWCVVEBUXFVVEBVVEUWKUWHAUWKUWBUWSUYAU YCVVDEXTUWLOVOVVEUXFUXEUYAUYCVVDYAUGVRUWQUXGYBVEYCXLYDVAYFWTWTXEUWPVVBVUMUW SVUBAVVBVUMUWBAVVBVUMAVUTVUMFUATTAUYAUYCLZLZVUTVUMVVHVUSVUMUXKVVHVUSLZBVUPG HZVUMVVIBVUQGHZVVJVVIBUXGGHZVVKVVIBBUXFAUXAVVGVUSUXCQZVVMAUYAUYCVUSYGZABBGH ZVVGVUSAUWKUXAVVOEUXBBYHYPQYIVVIVVLLVVLVVLVVKVVIVVLPZVVPVVHVVLVVLLZVVKUPVUS VVLVVHVVQVVKVVHVVLVVKVVLVVHVVLLZBUXGUXGUEJZGHZVVKVVRBUXGUXGVVRUWKUXAAUWKVVG VVLEQUXBOZVVRBUXFVWAAUYAUYCVVLYGRZVWBVVHVVLPYIVVRVVTLZVVTVVKVVRVVTPVWCVVSVU QBGVVHVVSVUQKVVLVVTVVHVUQVVSVVHUXGVVHUXGVVHBUXFVVHUWKUXAAUWKVVGENUXBOZAUYAU YCYJZRZUGZUHUUAQYCXLSUUBVAQUUCSVVIVVKLZBVURVUQVKJVUPGVWHBVURVUQAUXAVVGVUSVV KUXCVNZVVHVUSVVKUUDVVIVVKPVVHVURTMVUSVVKVVHVUPVUQVVHVULVUOVVHVUGVULTMVVHUWQ VVHBCVWDAUWIVVGDNXFZXGZUWQWPOVVHIVUNITMZVVHYKYLVVHUWQUXGVWKVWFRZRXHZVVHVUJV UQTMZVWFUXGWPZOUUEQVWHVUJVWOVWHBUXFVWIVVHUYAVUSVVKVWEQRVWPOUUFVWHVUPVUQVVHV UPUFMVUSVVKVVHVULVUOAVULUFMVVGAVULAUWQIVUHIUUHMAUUGYLUUIXSNZVVHIVUNVVHYQVVH VUNVWMUGVRZUUJQVVHVUQUFMVUSVVKVVHUXGVWGWEQUUKYMSVVIVVJLZBVUPVUOVGJZVULGVWSB VUPVUOAUXAVVGVUSVVJUXCVNVVHVUSVVJBVUOGHZVVHVVJVXAVUSVVHVVJLZBVUNIUEJVUOGVXB BVUNIVXBUWKUXAAUWKVVGVVJEQUXBOZVXBUWQUXGVXBUWQVXBBCVXCAUWIVVGVVJDQXFXGZVXBB UXFVXCAUYAUYCVVJYGRZRVWLVXBYKYLVXBBUXGUWQUEJVUNGVXBBUXGUWQVXCVXEVXDVVHVVLVV JAUXAUYAVVLVVGUXCUYAUYCUNBUXFUULUUMNYIVXBUXGUWQVXBUXGVXEUGZVVHVVFVVJVVHUWQV WJXSNZYNYMYIVXBVUNIVXBUWQUXGVXGVXFVRVXBYQYNYMYOYRVVIVVJPVVIVUOTMZVVJVVIVWLV UNTMVXHYKVVIUWQUXGAVUGVVGVUSVUIQVVIBUXFVVMVVNRRIVUNUUNUUONVVHVUPTMVUSVVJVWN QUUPVVHVWTVULKVUSVVJVVHVULVUOVWQVWRUUQQYMSYOVAUURXEXPUUSSVUKVUMLUXEVUMLZUWR UXEVUMVUBVXIVXIVXIVUBVXIUMNUUTUXEVUMVXIUWRVUBVXIUWRVXIUWPUWSVUMUWRUWPUWSVUM LZLZUWQYSKZYTZUWRVXKVXLBYSGHZVXKUWKVXNYTAUWKUWBVXJEQZBUVAOVXKVXLLZBVULYSGUW PUWSVUMVXLUVBVXPVULYSIUBJYSVXPUWQYSIUBVXKVXLPUIUVCUVDYMUVEVXKUWRVXLUVHZVXMU WRUPVXKUWSVXQUWPUWSVUMYJVXKUWKUWQUJMZUWSVXQWMVXOUWPVXRVXJUWPUWQCBVBJZUJUWPU XAUWIUWQVXSKUWPUWKUXAAUWKUWBENUXBOAUWIUWBDNBCUVFVEAVXSUJMZUWBAUWIUXACUDKZBU DKZLYTVXTDUXCAVYBVYAABUDUYQUVIUVGCBUVJUVKNWQNBUWQUVLVEXLVXKVXQLZVXLUWRVYCUW RVXLVXKVXQPUVMUVNSUVOYRNWSSSXPSXPSSSUWPUWRLUWQBCGUWPUWRPAUWTUWBUWRAUWSUWTUX DUVPQUVQSVAUVR $. $}