metamath/valid/mathd-algebra-31.mm

${
  $d U k x $.
  $d U n x $.
  $d X k x $.
  $d X n x $.
  $d k ph x $.
  $d n ph x $.
  mathd-algebra-31.0 $e |- ( ph -> A. n e. NN ( U ` ( n + 1 ) ) = ( sqrt ` ( X 
+ ( U ` n ) ) ) ) $.
  mathd-algebra-31.1 $e |- ( ph -> U ~~> 9 ) $.
  mathd-algebra-31.2 $e |- ( ph -> X e. RR+ ) $.
  mathd-algebra-31.3 $e |- ( ph -> U : NN --> RR+ ) $.
  $( (Contributed by Kunhao Zheng, 15-Apr-2021.) $)
  mathd-algebra-31 $p |- ( ph -> 9 = ( sqrt ` ( X + 9 ) ) ) $=
( vx cn c1 caddc co cfv c9 csqrt wceq cvv wcel crp vk cv cmpt cli nnuz 1zzd wbr 
nnexALT mptexg mp1i climrel brrelexi syl eqidd simpr fveq2d ax-frege54c wa 
oveq1 fvex fvmpt3i eqtr4d climshft2 mpbird ccom cmnf cc0 cioc cdif ccncf cc 
cres nfcv sqrtcn a1i wss rpcn cr clt cle wn rpgt0 0red rpre ltnled mpbid w3a 
intn3an3d cxr wb mnfxr 0re elioc2 mp2an sylnibr eldifd cncfmptss sselda ssriv 
fvres mpteq2dva eleq1d adantr ffvelrnda fmptd oveq2d fvmptd climaddc2 rpaddcld 
rpcnd 9nn nnrpd climcncf fveq2 cbvmptv fmptco eleq1 anbi2d eqeq12d wi imbi12d 
r19.21bi chvarv eqcomd 3eqtrd 3brtr3d jca climuni ) AIJIUBZKLMZB 
NZUCZOUDUGZYLDOLMZPNZUDUGZUROYOQAYMYPAYMBOUDUGZFAOUAYLBKKRRJUEAUFZYRJRSZYLR 
SAUHIJYKRUIUJAYQBRSFBOUDUKULUMAUAUBZJSZURZYTKLMZBNZUUDYTYLNZUUBUUDUNUUBUUAU 
UEUUDQAUUAUOZIYTYKUUDJYLYIYTQZYJUUCBYIYTKLUSUPYLUQYJBUTVAUMVBVCVDAITYIPNZUC 
ZIJDYIBNZLMZUCZVEZYNUUINZYLYOUDATVKYNUUIUULKJUEYRAITYIPVKVFVGVHMZVIZVLZNZUC 
ZTVKVJMZSUUIUUTSAIUUPVKTUUQIUUQVMUUQUUPVKVJMSAUUPUUPUQVNVOTUUPVPACTUUPCUBZT 
SZUVAVKUUOUVAVQUVBUVAVRSZVFUVAVSUGZUVAVGVTUGZWGZUVAUUOSZUVBUVEUVCUVDUVBVGUV 
AVSUGUVEWAUVAWBUVBVGUVAUVBWCUVAWDWEWFWHVFWISVGVRSUVGUVFWJWKWLVFVGUVAWMWNWOW 
PWSVOZWQAUUSUUIUUTAITUURUUHAYITSURYIUUPSUURUUHQATUUPYIUVHWRYIUUPPWTUMXAXBWF 
AIJUUKTUULAYIJSZURZDUUJADTSZUVIGXCAJTYIBHXDXIUULUQXEAODUABUULKRJUEYRFADGXJY 
SUULRSAUHIJUUKRUIUJUUBYTBNZAJTYTBHXDZXJUUBIYTUUKDUVLLMJUULTUUBUULUNUUBUUGUR 
ZUUJUVLDLUVNYIYTBUUBUUGUOUPXFUUFUUBDUVLAUVKUUAGXCUVMXIXGXHADOGAOOJSAXKVOXLX 
IZXMAUUMCJDUVABNZLMZPNZUCZIJUUKPNZUCZYLACIJTUVQUUHUVRUULUUIAUVAJSZURZDUVPAU 
VKUWBGXCAJTUVABHXDXIUULCJUVQUCQAICJUUKUVQYIUVAQUUJUVPDLYIUVABXNXFXOVOAUUIUN 
YIUVQPXNXPUVSUWAQACIJUVRUVTUVAYIQZUVQUUKPUWDUVPUUJDLUVAYIBXNXFUPZXOVOAIJUVT 
YKUVJYKUVTUWCUVAKLMZBNZUVRQZXTUVJYKUVTQZXTCIUWDUWCUVJUWHUWIUWDUWBUVIAUVAYIJ 
XQXRUWDUWGYKUVRUVTUWDUWFYJBUVAYIKLUSUPUWEXSYAAUWHCJEYBYCYDXAYEAYNTSUUNYOQUV 
OIYNUUHYOTUUIYIYNPXNUUIUQYIPUTVAUMYFYGOYOYLYHUM $.
$}