metamath/valid/mathd-algebra-455.mm

${
  mathd-algebra-455.0 $e |- ( ph -> X e. RR ) $.
  mathd-algebra-455.1 $e |- ( ph -> ( 2 x. ( 2 x. ( 2 x. ( 2 x. X ) ) ) ) = ; 4 
8 ) $.
  $( (Contributed by Kunhao Zheng, 1-Jun-2021.) $)
  mathd-algebra-455 $p |- ( ph -> X = 3 ) $=
( c2 cmul co c1 c6 cdiv c4 c8 c3 1nn0 a1i mulcld mulassd eqcomd wceq eqtrd cdc 
recnd wcel 6nn decnncl nncni cc0 wne nnne0i divcan3d 2cnd 2t2e4 oveq12d cc 
4t4e16 oveq1d 3eqtrrd eqtr3d 4nn0 8nn0 deccl 3nn0 6nn0 ax-frege54c caddc nn0cni 
mulid2i oveq1i 3p1e4 eqtri 6t3e18 decmul1c divmulii 3eqtrd ) ABEEEEB 
FGZFGZFGFGZHIUAZJGZKLUAZVRJGZMAVRBFGZVRJGBVSABVRABCUBZVRUNUCAVRHINUDUEZUFZO 
VRUGUHAVRWDUIZOUJAWBVQVRJAVQEEFGZVPFGZWGEFGZVOFGZWBAWHVQAEEVPAUKZWKAEVOWKAE 
BWKWCPZPQRAWJWHAWGEVOAEEWKWKPZWKWLQRAWJWIEFGZBFGZWBAWOWJAWIEBAWGEWMWKPWKWCQ 
RAWNVRBFAWNWGWGFGZVRAWGEEWMWKWKQAWPKKFGZVRAWGKWGKFWGKSAULOZWRUMWQVRSAUOOTTU 
PTUQUPURAVQVTVRJDUPWAMSAVTVRMVTKLUSUTVAVFWEMVBVFZWFHIKLMHVRVBNVCVRVDUTNHMFG 
ZHVEGMHVEGKWTMHVEMWSVGVHVIVJVKVLVMOVN $.
$}