metamath/valid/amc12a-2002-p1.mm

${
  $d F x $.
  $d F y $.
  $d ph x $.
  $d ph y $.
  $d x z $.
  $d y z $.
  amc12a-2002-p1.0 $e |- ( ph -> F : CC --> CC ) $.
  amc12a-2002-p1.1 $e |- ( ph -> A. x e. CC ( F ` x ) = ( ( ( ( 2 x. x ) + 3 ) 
x. ( x - 4 ) ) + ( ( ( 2 x. x ) + 3 ) x. ( x - 6 ) ) ) ) $.
  $( (Contributed by Kunhao Zheng, 22-Apr-2021.) $)
  amc12a-2002-p1 $p |- ( ph -> sum_ y e. ( `' F " { 0 } ) y = ( 7 / 2 ) ) $=
( cc0 cc c2 cmul co c3 caddc c4 cmin c6 wceq oveq12d wcel a1i ccnv csn cima vz 
cv csu cmpt cdiv cfv feqmptd r19.21bi mpteq2dva eqtrd oveq2 oveq1d oveq1 c7 
cbvmptv syl6eq cnveqd imaeq1d sumeq1d cneg c1 cdc wa wo ax-frege54c ovex cpr 
fvmpt eqeq1d pm5.32i 2cnd simpr mulcld 3cn addcld 4cn subcld 6cn adddid eqcomd 
mul0ord 0cnd subcan2ad bicomd pncand df-neg eqeq12d wne negcli div11 wb 2ne0 
w3a syl112anc divcan3d bitrd 3bitrd addsub4d 2timesd 6p4e10b eqtr3d addcomli 
1nn0 0nn0 deccl nn0cni addcan2d npcand addid2d jca syl3anc orbi12d pm5.32da wi 
divcli eleq1 mpbiri jaod pm4.71rd bitr4d syl5bb fnmpti fniniseg 2cn wfn mp1i 
vex elpr 3bitr4d eqrdv id jctil 3re clt wbr 7cn eqtri renegcld cr rehalfcld 1nn 
decnncl2 nnred crp 2rp 0red 3pos lt0neg2 ax-mp mpbi nngt0d lttrd ltdiv1dd ltned 
sumpr divdiri addcomgi negsubi subaddrii oveq1i eqtr3i cn 7p3e10b ) 
ADUAZGUBZUCZCUEZCUFUDHIUDUEZJKZLMKZUVKNOKZJKZUVMUVKPOKZJKZMKZU 
GZUAZUVHUCZUVJCUFZUQIUHKZAUVIUWAUVJCAUVGUVTUVHADUVSADBHIBUEZJKZLMKZUWDNOKZJ 
KZUWFUWDPOKZJKZMKZUGZUVSADBHUWDDUIZUGUWLABHHDEUJABHUWMUWKAUWMUWKQBHFUKULUMB 
UDHUWKUVRUWDUVKQZUWHUVOUWJUVQMUWNUWFUVMUWGUVNJUWNUWEUVLLMUWDUVKIJUNUOZUWDUV 
KNOUPRUWNUWFUVMUWIUVPJUWOUWDUVKPOUPRRURUSUTVAVBAUWBLVCZIUHKZVDGVEZIUHKZVJZU 
VJCUFZUWCAUWAUWTUVJCABUWAUWTAUWDHSZUWDUVSUIZGQZVFZUWDUWQQZUWDUWSQZVGZUWDUWA 
SZUWDUWTSZUXEUXBUWKGQZVFZAUXHUXBUXDUXKUXBUXCUWKGUDUWDUVRUWKHUVSUVKUWDQZUVOU 
WHUVQUWJMUXMUVMUWFUVNUWGJUXMUVLUWELMUVKUWDIJUNUOZUVKUWDNOUPRUXMUVMUWFUVPUWI 
JUXNUVKUWDPOUPRRUVSVHZUWHUWJMVIVKVLVMAUXLUXBUXHVFUXHAUXBUXKUXHAUXBVFZUXKUWF 
UWGUWIMKZJKZGQUWFGQZUXQGQZVGUXHUXPUWKUXRGUXPUXRUWKUXPUWFUWGUWIUXPUWELUXPIUW 
DUXPVNZAUXBVOZVPZLHSUXPVQTZVRZUXPUWDNUYBNHSUXPVSTZVTZUXPUWDPUYBPHSUXPWATZVT 
ZWBWCVLUXPUWFUXQUYEUXPUWGUWIUYGUYIVRWDUXPUXSUXFUXTUXGUXPUXSUWFLOKZGLOKZQZUW 
EUWPQZUXFUXPUYLUXSUXPUWFGLUYEUXPWEZUYDWFWGUXPUYJUWEUYKUWPUXPUWELUYCUYDWHUXP 
UWPUYKUWPUYKQUXPLWITWCWJUXPUYMUWEIUHKZUWQQZUXFUXPUWEHSZUWPHSZIHSZIGWKZUYMUY 
PWNUYCUYRUXPLVQWLZTUYAUYTUXPWOTZUYQUYRUYSUYTVFZWPUYPUYMUWEUWPIWMWGWQUXPUYOU 
WDUWQUXPUWDIUYBUYAVUBWRZVLWSWTUXPUXTUWEUWROKZGQZVUEUWRMKZGUWRMKZQZUXGUXPUXQ 
VUEGUXPUWDUWDMKZNPMKZOKUXQVUEUXPUWDUWDNPUYBUYBUYFUYHXAUXPVUJUWEVUKUWROUXPUW 
EVUJUXPUWDUYBXBWCVUKUWRQUXPPNUWRWAVSXCXETRXDVLUXPVUIVUFUXPVUEGUWRUXPUWEUWRU 
YCUWRHSZUXPUWRVDGXFXGXHXIZTZVTUYNVUNXJWGUXPVUIUWEUWRQZUYOUWSQZUXGUXPVUGUWEV 
UHUWRUXPUWEUWRUYCVUNXKUXPUWRVUNXLWJUXPUYQVULVUCVUOVUPWNUYCVUNUXPUYSUYTUYAVU 
BXMUYQVULVUCWPVUPVUOUWEUWRIWMWGXNUXPUYOUWDUWSVUDVLWTWTXOWTXPAUXHUXBAUXFUXBU 
XGUXFUXBXQAUXFUXBUWQHSZUWPIVUAYGWOXRZUWDUWQHXSXTTUXGUXBXQAUXGUXBUWSHSZUWRIV 
UMYGWOXRZUWDUWSHXSXTTYAYBYCYDUVSHYHUXIUXEWNAUDHUVRUVSUVOUVQMVIUXOYEHGUWDUVS 
YFYIUXJUXHWNAUWDUWQUWSBYJYKTYLYMVBAUXAUWQUWSMKZUWCAUWQUWSUVJUWQCUWSHHUVJUWQ 
QYNUVJUWSQYNAVUSVUQVUSAVUTTVURYOZVVBAUWQUWSAUWPALLUUBSZAYPTUUAZUUCAUWPUWRIV 
VDAUWRUWRUVESAVDUUDUUETZUUFZIUUGSAUUHTAUWPGUWRVVDAUUIVVFUWPGYQYRZAGLYQYRZVV 
GUUJVVCVVHVVGWNYPLUUKUULUUMTAUWRVVEUUNUUOUUPUUQUURUWPUWRMKZIUHKVVAUWCUWPUWR 
IVUAVUMYGWOUUSVVIUQIUHVVIUWRUWPMKZUQUWPUWRUUTVVJUWRLOKUQUWRLVUMVQUVAUWRLUQV 
UMVQYSUQLUWRYSVQUVFXEUVBYTYTUVCUVDUSUMUM $.
$}