metamath/valid/amc12b-2003-p6.mm

${
  $d A k $.
  $d R k $.
  $d U k $.
  amc12b-2003-p6.0 $e |- ( ph -> A e. RR ) $.
  amc12b-2003-p6.1 $e |- ( ph -> U : NN0 --> NN0 ) $.
  amc12b-2003-p6.2 $e |- ( ph -> A. k e. NN0 ( U ` k ) = ( A x. ( R ^ k ) ) ) $.
  amc12b-2003-p6.3 $e |- ( ph -> R e. RR ) $.
  amc12b-2003-p6.4 $e |- ( ph -> ( U ` 1 ) = 2 ) $.
  amc12b-2003-p6.5 $e |- ( ph -> ( U ` 3 ) = 6 ) $.
  $( (Contributed by Stanislas Polu, 16-Nov-2020.) $)
  amc12b-2003-p6 $p |- ( ph -> ( ( U ` 0 ) = ( 2 / ( sqrt ` 3 ) ) \/ ( U ` 0 ) 
= -u ( 2 / ( sqrt ` 3 ) ) ) ) $=
( cc0 c3 cdiv co wceq c2 cexp cmul a1i cfv c4 csqrt cneg wo cv wral wcel wi cn0 
0nn0 fveq2 oveq2 oveq2d eqeq12d rspcv syl mpd recnd exp0d mulid1d eqtrd c1 
oveq1d cmin wn 2ne0 neii eqeq1d mtbird wa 1nn0 ax-mp adantr oveq1 expcld mul02d 
sylan9eqr mtand neqned cz 3z expm1d eqcomd 3m1e2 eqtr2d exp1d mul01d 3nn0 
expne0d divcan5d mulexpd mulcomd oveq12d c8 c6 cu2 syl6eq wne 4cn 3ne0 cc 3cn 
pm3.2i 2cnne0 divcan5 mp3an eqcomi 2cn 4t2e8 mulcomli oveq12i eqtr2i 3t2e6 wb 
ffvelrnd nn0cnd cr 4re 3nn nndivred eqsqrtor syl2anc mpbid cle wbr cn crp 4nn0 
nn0ge0i sqrtdiv mp2an sqrt4 oveq1i eqeq2i negeqd eqeq2d orbi12d 3rp ) 
ALDUAZUBMNOZUCUAZPZYTUUBUDZPZUEZYTQMUCUAZNOZPZYTUUHUDZPZUEAYTQROZUUAP 
ZUUFAUULBQROZUUAAYTBQRAYTBCLROZSOZBAEUFZDUAZBCUUQROZSOZPZEUJUGZYTUUPPZHALUJ 
UHZUVBUVCUIUVDAUKTZUVAUVCELUJUUQLPZUURYTUUTUUPUUQLDULUVFUUSUUOBSUUQLCRUMUNU 
OUPUQURAUUPBVCSOBAUUOVCBSACACIUSZUTUNABABFUSZVAVBVBVDAUUNVCDUAZMROZMDUAZNOZ 
UUAAUUNBCSOZMROZBCMROZSOZNOZUVLAUUNUVOBMROZSOZUVOBSOZNOZUVQAUUNUVRBNOZUWAAU 
WBBMVCVEOZROZUUNAUWDUWBABMUVHABLABLPZUVILPZAUWFQLPZUWGVFAQLVGVHTAUVIQLJVIVJ 
ZAUWEVKUVIBCVCROZSOZLAUVIUWJPZUWEAUVBUWKHUVBUWKUIZAVCUJUHZUWLVLUVAUWKEVCUJU 
UQVCPZUURUVIUUTUWJUUQVCDULUWNUUSUWIBSUUQVCCRUMUNUOUPVMTURZVNUWEAUWJLUWISOLB 
LUWISVOAUWIACVCUVGUWMAVLTVPVQVRVBVSVTZMWAUHAWBTZWCWDAUWCQBRUWCQPAWETUNWFAUW 
AUWBAUVRBUVOABMUVHMUJUHZAWITZVPZUVHACMUVGUWSVPZUWPACMUVGACLACLPZUWFUWHAUXBV 
KZUVIUVMLUXCUVIUWJUVMAUWKUXBUWOVNUXCUWICBSAUWICPUXBACUVGWGZVNUNVBUXBAUVMBLS 
OLCLBSUMABUVHWHVRVBVSVTUWQWJWKWDVBAUVSUVNUVTUVPNAUVNUVSAUVNUVRUVOSOUVSABCMU 
VHUVGUWSWLAUVRUVOUWTUXAWMVBWDAUVOBUXAUVHWMWNVBAUVNUVJUVPUVKNAUVJUVNAUVIUVMM 
RAUVIUWJUVMUWOAUWICBSUXDUNVBVDWDAUVBUVPUVKPZHUVBUXEUIAUVBUVKUVPUWRUVBUVKUVP 
PZUIWIUVAUXFEMUJUUQMPZUURUVKUUTUVPUUQMDULUXGUUSUVOBSUUQMCRUMUNUOUPVMWDTURWN 
VBAUVLWOWPNOZUUAAUVJWOUVKWPNAUVJQMROWOAUVIQMRJVDWQWRKWNUXHUUAPAUUAQUBSOZQMS 
OZNOZUXHUXKUUAUBXBUHMXBUHZMLWSZVKQXBUHQLWSVKUXKUUAPWTUXLUXMXCXAXDXEUBMQXFXG 
XHUXIWOUXJWPNUBQWOWTXIXJXKMQWPXCXIXNXKXLXMTVBVBVBAYTXBUHUUAXBUHUUMUUFXOAYTA 
UJUJLDGUVEXPXQAUUAAUBMUBXRUHZAXSTMYGUHAXTTYAUSYTUUAYBYCYDAUUCUUIUUEUUKUUCUU 
IXOAUUBUUHYTUUHUUBUUBUBUCUAZUUGNOZUUHUXNLUBYEYFZVKMYHUHUUBUXPPUXNUXQXSUBYIY 
JXDYSUBMYKYLUXOQUUGNYMYNXMXHZYOTAUUDUUJYTAUUBUUHUUBUUHPAUXRTYPYQYRYD $.
$}