metamath/valid/amc12-2001-p9.mm

${
  $d F x y $.
  amc12-2001-p9.0 $e |- ( ph -> F : RR --> RR ) $.
  amc12-2001-p9.1 $e |- ( ph -> A. x e. RR+ A. y e. RR+ ( F ` ( x x. y ) ) = ( 
( F ` x ) / y ) ) $.
  amc12-2001-p9.2 $e |- ( ph -> ( F ` ; ; 5 0 0 ) = 3 ) $.
  $( (Contributed by Kunhao Zheng, 25-Mar-2021.) $)
  amc12-2001-p9 $p |- ( ph -> ( F ` ; ; 6 0 0 ) = ( 5 / 2 ) ) $=
( c6 cc0 c5 cdiv co c2 cmul 0nn0 a1i 5cn wcel crp c3 cdc cfv wceq 6nn0 1nn0 c1 
deccl ax-frege54c 6cn mulid2i mul02i addid1i decm1mma nn0cni eqcomi 5nn0 dec0h 
nnne0i mulid1i mul01i decm2mma divmulii oveq1d eqtrd cc div32d fveq2d 5nn wne 
6re 6pos elrpii 5re 5pos rpdivcld wa cv wral nn0rei decnncl2 nngt0i anim1i 
adantr oveq1 fveq2 eqeq12d oveq2 rspc2v sylc 3cn 6nn divdiv2d div23i mpdan 2cn 
2ne0 divreci halfcn mulcomi 3t2e6 oveq1i divcan4i eqtr3i mvllmuli eqtri 
3eqtr2ri syl6eq ) AHIUAZIUAZDUBZJIUAZIUAZDUBZHJKLZKLZJMKLZAXJXLXNNLZD 
UBZXOAXIXQDAXIXLJKLZHNLZXQAXIUFIUAZIUAZHNLZXTXIYCUCAYCXIYBHXHIYAIXHIIUDOUFI 
UEOUGZOOYBUHZIOUQZYAHHIUFIHIIUDOUEOOYAUHZYFHUIUJHUIUKZHUIULUMYHXHXHHIUDOUGU 
NULUMUOPAYBXSHNYBXSUCAXSYBXLJYBXLXKIJIUPOUGZOUGZUNZQYBYAIYDOUGUNJVHURZJYBXK 
IYAIXKIIUPOYDOOYEYFJYAJIUFIJIIUPOUEOOYGYFJQUSJQUTZJQULVAYMXKXKYIUNULVAVBUOP 
VCVDAXLJHXLVERAYKPJVERAQPZHVERAUIPZJIVIAYLPZVFVDVGAXNSRZXRXOUCZAHJHSRAHVJVK 
VLPJSRAJVMVNVLPVOAYQVPXLSRZYQVPBVQZCVQZNLZDUBZYTDUBZUUAKLZUCZCSVRBSVRZYRAYS 
YQYSAXLXLYJVSXLXKJVHVTVTWAVLPWBAUUGYQFWCUUFYRXLUUANLZDUBZXMUUAKLZUCBCXLXNSS 
YTXLUCZUUCUUIUUEUUJUUKUUBUUHDYTXLUUANWDVGUUKUUDXMUUAKYTXLDWEVCWFUUAXNUCZUUI 
XRUUJXOUULUUHXQDUUAXNXLNWGVGUUAXNXMKWGWFWHWIWNVDAXOTXNKLZXPAXMTXNKGVCAUUMTJ 
NLHKLZXPATHJTVERAWJPYOYNHIVIAHWKURZPYPWLUUNTHKLZJNLZXPTJHWJQUIUUOWMXPJUFMKL 
ZNLUURJNLUUQJMQWOWPWQUURJWRQWSUURUUPJNHUURTUIWRUUOHUURNLZHMKLZTUUTUUSHMUIWO 
WPWQUOTMNLZMKLUUTTUVAHMKWTXATMWJWOWPXBXCXEXDXAXFXEXGVDVD $.
$}