metamath/valid/amc12b-2003-p9.mm

${
  $d A x $.
  $d B x $.
  $d F x $.
  $d ph x $.
  amc12b-2003-p9.0 $e |- ( ph -> A e. RR ) $.
  amc12b-2003-p9.1 $e |- ( ph -> B e. RR ) $.
  amc12b-2003-p9.2 $e |- ( ph -> A. x e. RR ( F ` x ) = ( ( A x. x ) + B ) ) $.
  amc12b-2003-p9.3 $e |- ( ph -> ( ( F ` 6 ) - ( F ` 2 ) ) = ; 1 2 ) $.
  amc12b-2003-p9.4 $e |- ( ph -> F : RR --> RR ) $.
  $( (Contributed by Stanislas Polu, 26-Nov-2020.) $)
  amc12b-2003-p9 $p |- ( ph -> ( ( F ` ; 1 2 ) - ( F ` 2 ) ) = ; 3 0 ) $=
( c2 co cmul c3 cc0 cr wceq eqtrd a1i c6 c1 cdc cfv cmin caddc cmpt feqmptd cv 
r19.21bi mpteq2dva oveq2 oveq1d adantl wcel 1nn0 2nn decnncl nnrei recnd cc 
nncni mulcld addcld fvmptd 2re remulcld readdcld oveq12d subdid pnpcan2d 2cnd 
eqcomd recni 0nn0 deccl 2nn0 dec0h ax-frege54c 0p1e1 addid1i subaddrii nn0cni 
decadd oveq2d mulcomd cdiv 3nn0 3cn decnncl2 nnne0i mulid2i decm1mma 1nn mul02i 
divmulii 6cn subcld wne 4cn 4p2e6 addcomli 4ne0 eqnetri divcan4d c4 wral fveq2 
eqeq12d rspcv mpsyl 4t3e12 divmuli mpbir nn0rei divmuld mpbid 6re ) 
AUAKUBZEUCZKEUCZUDLZCXRKUDLZMLZNOUBZAYACXRMLZDUELZCKMLZDUELZUDLZYCAXS 
YFXTYHUDABXRCBUHZMLZDUELZYFPEUTAEBPYJEUCZUFBPYLUFABPPEJUGABPYMYLAYMYLQZBPHU 
IUJRZYJXRQZYLYFQAYPYKYEDUEYJXRCMUKULUMXRPUNAXRUAKUOUPUQZURSAYEDACXRACFUSZXR 
UTUNAXRYQVAZSZVBZADGUSZVCVDABKYLYHPEPYOYJKQZYLYHQAUUCYKYGDUEYJKCMUKULUMKPUN 
AVESZAYGDACKFUUDVFGVGVDZVHAYCYIAYCYEYGUDLZYIACXRKYRYTAVKZVIAYIUUFAYEYGDUUAA 
CKYRUUGVBZUUBVJVLRVLRAYCCUAOUBZMLZYDAYBUUICMYBUUIQAXRKUUIYSKVEVMZUUIUAOUOVN 
VOWBZOKUAOUAKKUUIVNVPUOVNKVPVQUUIVRZVSKUUKVTWCWASWDAUUJUUICMLZYDACUUIYRUUIU 
TUNAUULSZWEAYDUUIWFLZCQUUNYDQAUUPNCUUPNQAYDUUINYDNOWGVNVOZWBUULWHUUIUAWMWIW 
JZUUINNOUAONOOWGVNUOVNVNUUMOVNVQNWHWKNWHWNNWHVTWLWOSACNACTEUCZXTUDLZTKUDLZW 
FLZNACCTMLZDUELZYHUDLZUVAWFLZUVBACUVCYGUDLZUVAWFLZUVFACCUVAMLZUVAWFLZUVHAUV 
JCACUVAYRATKTUTUNAWPSZUUGWQUVAOWRAUVAXEOTKXEWPUUKWSXEKTWSUUKWTXAWAZXBXCSXDV 
LAUVIUVGUVAWFACTKYRUVKUUGVIULRAUVGUVEUVAWFAUVEUVGAUVCYGDACTYRUVKVBUUHUUBVJV 
LULRAUVEUUTUVAWFAUVDUUSYHXTUDAUUSUVDTPUNAYNBPXFUUSUVDQZXQHYNUVMBTPYJTQZYMUU 
SYLUVDYJTEXGUVNYKUVCDUEYJTCMUKULXHXIXJVLAXTYHUUEVLVHULRAUVBUUTXEWFLZNAUVAXE 
UUTWFUVAXEQAUVLSWDAUVOXRXEWFLZNAUUTXRXEWFIULUVPNQZAUVQXENMLXRQXKXRXENYSWSWH 
XBXLXMSRRRVLRAYDUUICAYDYDPUNAYDUUQXNSUSUUOYRUUIOWRAUURSXOXPRRR $.
$}