metamath/valid/mathd-algebra-159.mm

${
  $d B x $.
  $d F x $.
  $d ph x $.
  mathd-algebra-159.0 $e |- ( ph -> F : RR --> RR ) $.
  mathd-algebra-159.1 $e |- ( ( ph /\ x e. RR ) -> ( F ` x ) = ( ( ( ( ( 3 x. ( 
x ^ 4 ) ) - ( 7 x. ( x ^ 3 ) ) ) + ( 2 x. ( x ^ 2 ) ) ) - ( B x. x ) ) + 1 ) ) 
$.
  mathd-algebra-159.2 $e |- ( ph -> B e. RR ) $.
  mathd-algebra-159.3 $e |- ( ph -> ( F ` 1 ) = 1 ) $.
  $( (Contributed by Kunhao Zheng, 31-May-2021.) $)
  mathd-algebra-159 $p |- ( ph -> B = -u 2 ) $=
( c3 c1 c4 co cmul c7 cmin c2 caddc wceq wcel a1i cexp cneg cv cmpt feqmptd cfv 
cr mpteq2dva eqtrd wa simpr oveq1d oveq2d oveq12d 1red cn 3nn nnred cn0 4nn0 
reexpcld remulcld 7nn0 nn0red 3nn0 resubcld 2nn0 readdcld fvmptd cz 4z eqtr3d 
1exp syl cc 3cn mulid1d eqtr2d mp1i 7cn sq1 2cnd recnd eqcomd eqeq1d biimpar 
4cn negcli 4p3e7 subaddrii negsubib oveq1i addcomgi 2cn 2p2e4 eqtri 3z biimpa 
adantr 0p1e1 syl6eqr wb subcld 0cnd 1cnd addcan2d subeq0d adantlr cc0 mpdan ) 
AIJKUALZMLZNJIUALZMLZOLZPJPUALZMLZQLZCJMLZOLZJQLZJRZCPUBZRZAJDU 
FYAJABJIBUCZKUALZMLZNYEIUALZMLZOLZPYEPUALZMLZQLZCYEMLZOLZJQLZYAUGDUGADBUGYE 
DUFZUDBUGYPUDABUGUGDEUEABUGYQYPFUHUIAYEJRZUJZYOXTJQYSYMXRYNXSOYSYJXOYLXQQYS 
YGXLYIXNOYSYFXKIMYSYEJKUAAYRUKZULUMYSYHXMNMYSYEJIUAYTULUMUNYSYKXPPMYSYEJPUA 
YTULUMUNYSYEJCMYTUMUNULAUOZAXTJAXRXSAXOXQAXLXNAIXKAIIUPSAUQTURAJKUUAKUSSAUT 
TVAVBANXMANNUSSAVCTVDAJIUUAIUSSAVETVAVBVFAPXPAPPUSSAVGTZVDAJPUUAUUBVAVBVHAC 
JGUUAVBVFUUAVHVIHVLAYBUJINOLZPQLZCOLZJQLZJRZYDAUUGYBAUUFYAJAUUEXTJQAUUDXRCX 
SOAUUCXOPXQQAIXLNXNOAXLIJMLIAXKJIMAKVJSZXKJRUUHAVKTKVMVNUMAIIVOSAVPTVQVRAXN 
NJMLNAXMJNMIVJSXMJRAWQIVMVSUMANNVOSAVTTVQVRUNAXQPJMLPAXPJPMXPJRAWATUMAPAWBV 
QVRUNAXSCACACGWCZVQWDUNULWEWFAUUGYDYBAUUGUJYCCOLZJQLZJRZYDAUUGUULAUUFUUKJAU 
UEUUJJQAUUDYCCOUUDYCRAUUDKUBZPQLZYCUUCUUMPQINUUMVPVTKWGWHNKIVTWGVPNKIVTWGVP 
WIWJWKWJWLUUNPUUMQLYCUUMPWMPKYCWNWGPWNWHZPKYCWNWGUUOKPPWGWNWNKPPWGWNWNWOWJW 
KWJWKWPWPTULULWEWRAUULYDUUGAUULUJZYCCUUPYCCYCVOSZUUPUUOTACVOSUULUUIWSUUPUUK 
XIJQLZRZUUJXIRZUUPUUKJUURAUULUKWTXAUUPUUSUUTAUUSUUTXBUULAUUJXIJAYCCUUQAUUOT 
UUIXCAXDAXEXFWSWRXJXGWDXHXJXHXJXJ $.
$}