metamath/valid/numbertheory-xsqpysqintdenomeq.mm

${
  numbertheory-xsqpysqintdenomeq.0 $e |- ( ph -> X e. QQ ) $.
  numbertheory-xsqpysqintdenomeq.1 $e |- ( ph -> Y e. QQ ) $.
  numbertheory-xsqpysqintdenomeq.2 $e |- ( ph -> ( ( X ^ 2 ) + ( Y ^ 2 ) ) = N 
) $.
  numbertheory-xsqpysqintdenomeq.3 $e |- ( ph -> N e. ZZ ) $.
  $( (Contributed by Stanislas Polu, 12-Feb-2021.) $)
  numbertheory-xsqpysqintdenomeq $p |- ( ph -> ( denom ` X ) = ( denom ` Y ) ) 
$=
( wceq c2 cexp co c1 cz wcel syl eqcomd eqtrd cmul zcnd cdenom cfv cdvds wa wbr 
cnumer cgcd cq cn qdencl nnzd qnumcl zgcdsq syl2anc gcdcom qnumdencoprm oveq1d 
sq1 syl6eq cmin zsqcl zmulcld zsubcld 3jca caddc mulcomd cdiv mulcld w3a nnne0d 
2z expne0d divdird div23d divcan4d oveq12d divcld divassd sqdivd a1i dividd 
sqcld mulid1d qeqnumdivden addcld divmuld bicomd mpbird subadd2d subdird 
dvds0lem adantr anim1i coprmdvdsb syl3anc mpdan dvdssq mpbid mul32d wb addcomd 
jca cn0 wi nnnn0d dvdseq ex mpd ) ACUAUBZDUAUBZUCUEZXJXIUCUEZUDZ 
XIXJIZAXKXLAXIJKLZXJJKLZUCUEZXKAXOCUFUBZJKLZUGLZMIZXQAXTXIXRUGLZJKLZMAXINOZ 
XRNOZXTYCIAXIACUHOZXIUIOECUJPZUKZAYFYEECULPZYDYEUDYCXTXIXRUMQUNAYCMJKLZMAYB 
MJKAYBXRXIUGLZMAYDYEYBYKIYHYIXIXRUOUNAYFYKMIECUPPRUQURUSRAYAUDZXQXOXSXPSLZU 
CUEZAYNYAABXPSLZDUFUBZJKLZUTLZNOZXONOZYMNOZVIYRXOSLZYMIYNAYSYTUUAAYOYQABXPH 
AXJNOZXPNOZAXJADUHOZXJUIOFDUJZPZUKZXJVAPZVBZAYPNOZYQNOZAUUEUUKFDULZPZYPVAPZ 
VCAYDYTYHXIVAPZAXSXPAYEXSNOZYIXRVAPZUUIVBVDAYMUUBAYMYOXOSLZYQXOSLZUTLZUUBAU 
VAYMAUVAYMIYMUUTVELZUUSIAUUSUVBAUUSXOYOSLZUVBAYOXOAYOUUJTZAXOUUPTZVFAUVCUVB 
IZUVBXOVGLZYOIZAUVGYMXOVGLZUUTXOVGLZVELZYOAYMUUTXOAXSXPAXSUURTZAXPUUITZVHZA 
YQXOAYQUUOTZUVEVHZUVEAXIJAXIYHTZAXIYGVJZJNOAVKVTZVLZVMAUVKXSXOVGLZXPSLZYQVE 
LZYOAUVIUWBUVJYQVEAXSXPXOUVLUVMUVEUVTVNAYQXOUVOUVEUVTVOVPAYOUWCAYOXPBSLZUWC 
ABXPABHTZUVMVFAUWDUWCIZUWCXPVGLZBIZAUWGCJKLZDJKLZVELZBAUWGUWBXPVGLZYQXPVGLZ 
VELUWKAUWBYQXPAUWAXPAXSXOUVLUVEUVTVQZUVMVHZUVOUVMAXJJAXJUUHTZAXJUUGVJZUVSVL 
ZVMAUWLUWIUWMUWJVEAUWLUWAXPXPVGLZSLZUWIAUWAXPXPUWNUVMUVMUWRVRAUWTXRXIVGLZJK 
LZMSLZUWIAUWAUXBUWSMSAUXBUWAAXRXIAXRYITZUVQUVRVSQAXPUVMUWRWAVPAUXCUXBUWIAUX 
BAUXAAXRXIUXDUVQUVRVQWBWCAUXACJKACUXAAYFCUXAIECWDPQUQRRRAUWMYPXJVGLZJKLZUWJ 
AUXFUWMAYPXJAYPUUNTUWPUWQVSQAUXEDJKADUXEAUUEDUXEIFDWDPQUQRVPRGRAUWHUWFAUWCX 
PBAUWBYQUWOUVOWEUVMUWEUWRWFWGWHRQRRAUVHUVFAUVBXOYOAYMUUTUVNUVPWEUVEUVDUVTWF 
WGWHRQZAUUSUUTYMAYOXOUVDUVEVHUVPUVNWIWHQAUUBUVAAYOYQXOUVDUVOUVEWJQRQYRXOYMW 
KUNWLYLYTUUDUUQYAUDXQYNWTAYTYAUUPWLAUUDYAUUIWLAUUQYAUURWMXOXSXPWNWOWHWPAXKX 
QAYDUUCXKXQWTYHUUHXIXJWQUNWGWRAXPXOUCUEZXLAXPYQUGLZMIZUXHAUXIXJYPUGLZJKLZMA 
UXLUXIAUUCUUKUXLUXIIUUHUUNXJYPUMUNQAUXLYJMAUXKMJKAUUEUXKMIFUUEUXKYPXJUGLZMU 
UEUUCUUKUXKUXMIUUEXJUUFUKUUMXJYPUOUNDUPRPUQURUSRAUXJUDZUXHXPUUTUCUEZAUXOUXJ 
ABXOSLZXSUTLZNOZUUDUUTNOZVIUXQXPSLZUUTIUXOAUXRUUDUXSAUXPXSABXOHUUPVBUURVCUU 
IAYQXOUUOUUPVBVDAUUTUXTAUUTUXPXPSLZYMUTLZUXTAUYBUUTAUYBUUTIUUTYMVELZUYAIAUY 
CUVBUYAAUUTYMUVPUVNXAAUVBUUSUYAUXGABXPXOUWEUVMUVEWSRRAUYAYMUUTAUXPXPABXOUWE 
UVEVHZUVMVHUVNUVPWIWHQAUXTUYBAUXPXSXPUYDUVLUVMWJQRQUXQXPUUTWKUNWLUXNUUDYTUU 
LUXJUDUXHUXOWTAUUDUXJUUIWLAYTUXJUUPWLAUULUXJUUOWMXPYQXOWNWOWHWPAXLUXHAUUCYD 
XLUXHWTUUHYHXJXIWQUNWGWRXBAXIXCOZXJXCOZXMXNXDAXIYGXEAXJUUGXEUYEUYFUDXMXNXIX 
JXFXGUNXH $. 
$}