metamath/valid/mathd-algebra-245.mm

${
  mathd-algebra-245.0 $e |- ( ph -> X e. RR ) $.
  mathd-algebra-245.1 $e |- ( ph -> X =/= 0 ) $.
  $( (Contributed by Kunhao Zheng, 31-May-2021.) $)
  mathd-algebra-245 $p |- ( ph -> ( ( ( ( 4 / X ) ^ -u 1 ) x. ( ( ( 3 x. ( X ^ 
3 ) ) / X ) ^ 2 ) ) x. ( ( 1 / ( 2 x. X ) ) ^ -u 3 ) ) = ( ; 1 8 x. ( X ^ 8 ) ) 
) $=
( c4 cdiv co c1 cexp wceq c3 cmul c2 c8 wcel a1i eqtrd oveq2d oveq1d c9 cdc 
cneg 4cn recnd divcld expn1 syl cc0 wne 4ne0 recdivd 3nn0 nn0cni cn0 expcld cc 
divassd caddc cmin 2cn ax-1cn pncan3oi oveq2i cz peano2zd expm1d syl5eqr df-3 
eqtr4d 1cnd 2cnd mulcld 2ne0 mulne0d recne0d expnegd expdivd 1exp mp1i 2z 3z 
expne0d recrecd w3a wa simpr1 simpr2 oveq12d simpr3 sqcld sqmuld 2nn0 sq3 
expmuld 2t2e4 eqtr3d mulexpd cu2 simprl simprr 9cn mul32d 4t2e8 mulassd 4nn0 
dmmcand mulcomd eqcomd df-4 expp1d syl5req mul4d 9t2e18 mulcomli 4p4e8 8cn 
expaddd eqtr2d adantr ex mp2and mp3and ) AEBFGZHUBIGZBEFGZJZKBKIGZLGBFG 
ZMIGZKBMIGZLGZMIGZJZHMBLGZFGZKUBIGZYNKIGZJZYDYILGZYPLGZHNUAZBNIGZLGZJZAYDHY 
CFGZYEAYCUPOYDUUEJAEBEUPOAUCPZABCUDZDUEYCUFUGAEBUUFUUGEUHUIAUJPZDUKQAYHYKMI 
AYHKYGBFGZLGYKAKYGBKUPOAKULUMPZABKUUGKUNOAULPZUOZUUGDUQAYJUUIKLAYJBMHURGZIG 
ZBFGZUUIAYJBUUMHUSGZIGUUOUUPMBIMHUTVAVBVCABUUMUUGDAMMVDOAVTPVEVFVGAYGUUNBFA 
KUUMBIKUUMJAVHPRSVIRVISAYPHYOKIGZFGZYQAYOKAHYNAVJZAMBAVKZUUGVLZAMBUUTUUGMUH 
UIAVMPDVNZUEAYNUVAUVBVOKVDOZAWAPZVPAUURHHKIGZYQFGZFGZYQAUUQUVFHFAHYNKUUSUVA 
UVBUUKVQRAUVGHHYQFGZFGYQAUVFUVHHFAUVEHYQFUVCUVEHJAWAKVRVSSRAYQAYNKUVAUUKUOA 
YNKUVAUVBUVDWBWCQQQAYFYMYRWDZUUDAUVIWEZYTYEYLLGZYQLGZUUCUVJYSUVKYPYQLUVJYDY 
EYIYLLAYFYMYRWFAYFYMYRWGWHAYFYMYRWIWHAUVLUUCJZUVIAYLTBEIGZLGZJZYQNYGLGZJZUV 
MAYLKMIGZYJMIGZLGUVOAKYJUUJABUUGWJWKAUVSTUVTUVNLUVSTJAWMPABMMLGZIGUVTUVNABM 
MUUGMUNOAWLPZUWBWNAUWAEBIUWAEJAWOPRWPWHQAYQMKIGZYGLGUVQAMBKUUTUUGUUKWQAUWCN 
YGLUWCNJAWRPSQAUVPUVRWEZUVMAUWDWEZUVLYEUVOLGZUVQLGZUUCUWEUVKUWFYQUVQLUWEYLU 
VOYELAUVPUVRWSRAUVPUVRWTWHAUWGUUCJUWDAUWGYEUVQLGZUVOLGZUUCAYEUVOUVQABEUUGUU 
FUUHUEATUVNTUPOAXAPZABEUUGEUNOAXEPZUOZVLANYGNUPOAXPPUULVLXBAUWIMUVNLGZUVOLG 
ZUUCAUWHUWMUVOLAUWHYEEMYGLGZLGZLGZUWMAUVQUWPYELAEMLGZYGLGUVQUWPAUWRNYGLUWRN 
JAXCPSAEMYGUUFUUTUULXDWPRAUWQBUWOLGZUWMABEUWOUUGUUFAMYGUUTUULVLZUUHXFAUWOBL 
GZUWSUWMAUWOBUWTUUGXGAMYGBLGZLGZUXAUWMAUXAUXCAMYGBUUTUULUUGXDXHAUXBUVNMLAUV 
NBKHURGZIGUXBEUXDBIXIVCABKUUGUUKXJXKRWPWPQQSAUWNMTLGZUVNUVNLGZLGUUCAMUVNTUV 
NUUTUWLUWJUWLXLAUXEUUAUXFUUBLUXEUUAJATMUUAXAUTXMXNPAUUBBEEURGZIGUXFANUXGBIA 
UXGNUXGNJAXOPXHRABEEUUGUWKUWKXQXRWHQQQXSQXTYAXSQXTYB $.
$}