metamath/valid/mathd-algebra-192.mm

${
  mathd-algebra-192.0 $e |- ( ph -> Q = ( ; 1 1 - ( 5 x. _i ) ) ) $.
  mathd-algebra-192.1 $e |- ( ph -> E = ( ; 1 1 + ( 5 x. _i ) ) ) $.
  mathd-algebra-192.2 $e |- ( ph -> D = ( 2 x. _i ) ) $.
  $( (Contributed by Kunhao Zheng, 15-Apr-2021.) $)
  mathd-algebra-192 $p |- ( ph -> ( ( Q x. E ) x. D ) = ( ; ; 2 9 2 x. _i ) ) $=
( cmul co c1 cdc c2 ci c5 1nn0 deccl ax-frege54c eqtri 2nn0 cc c4 cmin cexp c6 
c9 caddc nn0cni sqvali mulid1i 1p1e2 decsuc decm2mma2i 5cn ax-icn sqmuli cneg 
oveq2i sqcli ax-1cn mulneg2ib 5t5e25 negeqi oveq12i 5nn0 subnegi 2p2e4 i2 
decaddi 5p1e6 addcomli decadd wcel wceq mulcli subsq mp2an eqtr3i addcli subcli 
mulcomd oveq12d eqcomd eqtrd syl5req oveq1d oveq2d 4nn0 6nn0 mulassd a1i 2cnd 
c8 8nn0 8p1e9 cc0 0nn0 dec0h mulid2i 4t2e8 addid1i decm1mma 6t2e12 2cn decmul1c 
eqtr3d 3eqtrd ) ACDHIZBHIJUAKZUDKZBHIXILMHIZHIZLUEKZLKZMHIZAXG 
XIBHAXIJJKZNMHIZUFIZXOXPUBIZHIZXGXOLUCIZXPLUCIZUBIZXIXSYBJLKZJKZLNKZUPZUBIZ 
XIXTYDYAYFUBXTXOXOHIYDXOXOJJOOPZUGZUHXOJJYCJXOJYHOOOOXOYIUIZYJJJLXOOOUJXOQU 
KULRYANLUCIZUPZYFYAYKMLUCIZHIZYLNMUMUNUOYNYKJUPZHIYLYMYOYKHVGUQYKJYKNUMURZU 
SYPYKYPUIUTRRYKYEYKNNHIYENUMUHVARVBRVCYGYDYEUFIXIYDYEYDYCJJLOSPZOPUGYELNSVD 
PUGVEYCJLNXHUDYDYEYQOSVDYDQYEQJLUAYCLOSSYCQVFVHNJUDUMUSVIVJVKRRXOTVLXPTVLYB 
XSVMYINMUMUNVNZXOXPVOVPVQAXSXRXQHIZXGAXQXRXQTVLAXOXPYIYRVRWJXRTVLAXOXPYIYRV 
SWJVTAXGYSACXRDXQHEFWAWBWCWDWEABXJXIHGWFAXILHIZMHIXKXNAXILMXITVLAXIXHUDJUAO 
WGPZWHPUGWJAWKMTVLAUNWJWIAYTXMMHYTXMVMAXHUDXLLLJXISUUAWHXIQSOLWLUEXHLHISWMW 
NXHLLWLJUALWOWLSWMOWGWPXHQWLWMWQLXCWRWSLXCWTXAUKXBXDWJWEXEXF $.
$}