metamath/valid/amc12-2000-p15.mm (10 lines of code) (raw):

${ $d F x y $. $d ph t z $. $d ph x y $. $d y z $. amc12-2000-p15.0 $e |- ( ph -> F : CC --> CC ) $. amc12-2000-p15.1 $e |- ( ph -> A. x e. CC ( F ` ( x / 3 ) ) = ( ( ( x ^ 2 ) + x ) + 1 ) ) $. $( (Contributed by Kunhao Zheng, 22-Apr-2021.) $) amc12-2000-p15 $p |- ( ph -> sum_ y e. ( `' F " { 7 } ) ( y / 3 ) = -u ( 1 / 9 ) ) $= ( c3 cdiv co cc c9 c2 cmul caddc c6 cc0 c1 wcel wceq a1i vz vt ccnv c7 cima csn cv csu cexp cmin cmpt cneg cfv wa simpr 3cn 3ne0 divcan3d eqcomd fveq2d wne eqeq1d wral adantr mulcld oveq1 oveq1d oveq12d wb sqcld addcld 1cnd 7cn ax-1cn 6cn negsubi subaddrii eqtri oveq2d negsubd eqtrd sqmuld eqcomi bitrd sq3 pm5.32da wfn fniniseg ovex ax-frege54c mp1i 3bitr4d eqrdv sumeq1d wo c5 cdc 9cn negcld eqtr3d 9nn nnne0i 1nn0 5nn0 nn0cni c4 5cn mulcomli 0nn0 2nn0 deccl dec0h 2cn 4cn addcomli decadd mulneg2d 3eqtrd c8 0p1e1 oveq12i 6t2e12 3nn0 pm3.2i 0re mp3an eqeq2d mp2an negeqi eleq1 syl5ibrcom divcld 3t3e9 jca 6nn0 neg1rr clt wbr 2re 3re adantl eqeq12d rspcdv mpd subeq0 sylancl bicomd addsubassd negcli 6p1e7 oveq1i syl6reqr mpteq2dva subcld fvmptd ffnd fnmpti syl cpr oveq2 fvmpt pm5.32i addassd 5t3e15 sqvali 5t5e25 4nn0 addid2i 4p1e5 6t4e24 3eqtr2d adddid mulid1d mul12d subnegd quad2 addcomgi negsubib 9t2e18 3p2e5 df-3 6p2e8 decaddi 4t3lem 6pos gtneii divcan5 5p3e8 8nn decnncl nncni negdi2 divneg dividi 3eqtri orbi12d 3bitrd 2cnd jaod pm4.71rd bitr4d syl5bb orcom vex elpr divdiv1 oveq2i cn nnne0d neg1lt0 2pos 3pos divgt0ii redivcli lttri ltneii sumpr divcan5rd mulm1d addcomd negsubdi2i 2p1e3 eqtr3i 3eqtr3a divdird divnegd 3eqtr3d ) ADUCUDUFUEZCUGZGHIZCUHUAJKUAUGZLUIIZMIZGUYKMIZNIZ OUJIZUKZUCPUFUEZUYJCUHZQKHIULZAUYHUYRUYJCACUYHUYRAUYIJRZUYIDUMZUDSZUNZVUAUY IUYQUMZPSZUNZUYIUYHRZUYIUYRRZAVUAVUCVUFAVUAUNZVUCGUYIMIZGHIZDUMZUDSZVUFVUJV UBVUMUDVUJUYIVULDVUJVULUYIVUJUYIGAVUAUOZGJRZVUJUPTZGPVAZVUJUQTURUSUTVBVUJVU NVUKLUIIZVUKNIZQNIZUDSZVUFVUJVUMVVAUDVUJBUGZGHIZDUMZVVCLUIIZVVCNIZQNIZSZBJV CZVUMVVASZAVVJVUAFVDVUJVVIVVKBVUKJVUJGUYIVUQVUOVEZVUJVVCVUKSZUNZVVEVUMVVHVV AVVMVVEVUMSVUJVVMVVDVULDVVCVUKGHVFUTUUAVVNVVGVUTQNVVNVVFVUSVVCVUKNVVNVVCVUK LUIVUJVVMUOZVGVVOVHVGUUBUUCUUDVBVUJVVBVVAUDUJIZPSZVUFVUJVVQVVBVUJVVAJRUDJRZ VVQVVBVIVUJVUTQVUJVUSVUKVUJVUKVVLVJVVLVKZVUJVLZVKVMVVAUDUUEUUFUUGVUJVVPVUEP VUJVVPVUTQUDUJIZNIZVUEVUJVUTQUDVVSVVTVVRVUJVMTUUHVUJVWBVUTOUJIZVUEVUJVWBVUT OULZNIVWCVUJVWAVWDVUTNVWAVWDSVUJQUDVWDVNVMOVOUUIUDVWDNIUDOUJIQUDOVMVOVPUDOQ VMVOVNUUJVQVRVQTVSVUJVUTOVVSOJRZVUJVOTZVTWAVUJVUEVWCVUJUAUYIUYNLUIIZUYNNIZO UJIZVWCJUYQJVUJUAJUYPVWIVUJUYKJRZUNZUYOVWHOUJVWKUYMVWGUYNNVWKVWGGLUIIZUYLMI UYMVWKGUYKVUPVWKUPTVUJVWJUOWBKVWLUYLMVWLKWEWCUUKUULVGVGUUMVUJUYKUYISZUNZVWH VUTOUJVWNVWGVUSUYNVUKNVWNUYNVUKLUIVWNUYKUYIGMVUJVWMUOVSZVGVWOVHVGVUOVUJVUTO VVSVWFUUNUUOUSWAWAVBWDWDWDWFADJWGVUHVUDVIAJJDEUUPJUDUYIDWHUURUYQJWGZVUIVUGV IAUAJUYPUYQUYOOUJWIUYQWJZUUQZJPUYIUYQWHWKWLWMWNAUYSQULZLGHIZUUSZUYJCUHZUYTA UYRVXAUYJCAUBUYRVXAAUBUGZJRZVXCUYQUMZPSZUNZVXCVWSSZVXCVWTSZWOZVXCUYRRZVXCVX ARZVXGVXDKVXCLUIIZMIZGVXCMIZNIZOUJIZPSZUNZAVXJVXDVXFVXRVXDVXEVXQPUAVXCUYPVX QJUYQUYKVXCSZUYOVXPOUJVXTUYMVXNUYNVXONVXTUYLVXMKMUYKVXCLUIVFVSUYKVXCGMUUTVH VGVWQVXPOUJWIUVAVBUVBAVXSVXDVXJUNVXJAVXDVXRVXJAVXDUNZVXRVXNVXOVWDNINIZPSVXC GULZQWPWQZNIZLKMIZHIZSZVXCVYCVYDUJIZVYFHIZSZWOZVXJVYAVXQVYBPVYAVXPVWDNIVXQV YBVYAVXPOVYAVXNVXOVYAKVXMKJRZVYAWRTZVYAVXCAVXDUOZVJVEZVYAGVXCVUPVYAUPTZVYOV EZVKVWEVYAVOTZVTVYAVXNVXOVWDVYPVYRVYAOVYSWSZUVCWTVBVYAKGVWDVYDVXCVYNKPVAVYA KXAXBTVYQVYTVYOVYDJRZVYAVYDQWPXCXDXKXEZTVYAVYDLUIIZVWLWPLUIIZMIZVWLQXFOMIZN IZMIZVWLXFKVWDMIZMIZUJIZVYAWUCGWPMIZLUIIWUEVYAVYDWULLUIVYAWULVYDWULVYDSVYAW PGVYDXGUPUVDXHTUSVGVYAGWPVYQWPJRVYAXGTWBWAVYAWUDWUGVWLMVYAWUDLWPWQZQLXFWQZN IZWUGWUDWUMSVYAWUDWPWPMIWUMWPXGUVEUVFVRTWUOWUMSVYAPQLXFLWPQWUNXIXCXJUVGQXCX LWUNWJLXMUVHXFQWPXNVNUVIXOXPTVYAWUNWUFQNVYAWUFWUNWUFWUNSVYAOXFWUNVOXNUVJXHT USVSUVKVSVYAWUHVWLQMIZVWLWUFMIZNIVWLXFKOMIZMIZNIZWUKVYAVWLQWUFVYAGVYQVJZVYA VLVYAXFOXFJRVYAXNTZVYSVEUVLVYAWUPVWLWUQWUSNVYAVWLWVAUVMVYAWUQKWUFMIWUSVYAVW LKWUFMVWLKSVYAWETVGVYAKXFOVYNWVBVYSUVNWAVHVYAVWLWUSULZUJIWUTWUKVYAVWLWUSWVA VYAXFWURWVBVYAKOVYNVYSVEZVEUVOVYAWVCWUJVWLUJVYAXFWURULZMIWVCWUJVYAXFWURWVBW VDXQVYAWVEWUIXFMVYAWUIWVEVYAKOVYNVYSXQUSVSWTVSWTXRXRUVPVYAVYLVXIVXHWOZVXJVY AVYHVXIVYKVXHVYAVYGVWTVXCVYGVWTSVYAVYGQLWQZQXSWQZHIZVWTVYEWVGVYFWVHHVYEVYDV YCNIWVGVYCVYDUVQVYDGWVGWUBUPWVGQLXCXJXKXEZVYDGWVGWUBUPWVJPGQLQWPGWVGXIYCXCX JGYCXLZWVGWJZXTUVTXPVQUVRVRKLWVHWRXMUVSXHZYAWVIOLMIZOGMIZHIZVWTWVGWVNWVHWVO HWVNWVGYBWCWVOWVHOLGWVGWVHYOXJUWAYBQLXSWVGOXCXJYOWVLOLXSVOXMUWBXOUWCUWDWCYA LJRZVUPVURUNZVWEOPVAZUNWVPVWTSXMVUPVURUPUQYDZVWEWVSVOPOYEUWEUWFYDLGOUWGYFVR VRTYGVYAVYJVWSVXCVYJVWSSVYAVYJWVHULZWVHHIZWVHWVHHIZULZVWSVYIWWAVYFWVHHVYIGV YDNIZULZWWAWWFVYIVUPWUAWWFVYISUPWUBGVYDUWLYHWCWWEWVHPGQWPQXSGVYDXIYCXCXDWVK VYDWJXTWPGXSXGUPUWHXOXPYIVRWVMYAWWDWWBWVHJRZWWGWVHPVAWWDWWBSWVHQXSXCUWIUWJZ UWKZWWIWVHWWHXBZWVHWVHUWMYFWCWWCQWVHWWIWWJUWNYIUWOTYGUWPWVFVXJVIVYAVXIVXHUX CTWDUWQWFAVXJVXDAVXHVXDVXIAVXDVXHVWSJRZAQAVLZWSZVXCVWSJYJYKAVXDVXIVWTJRZALG AUWRZVUPAUPTZVURAUQTZYLZVXCVWTJYJYKUWSUWTUXAUXBVWPVXKVXGVIAVWRJPVXCUYQWHWKV XLVXJVIAVXCVWSVWTUBUXDUXETWLWMWNAVXBVWSGHIZLKHIZNIZUYTAVWSVWTUYJWWSCWWTJJUY IVWSGHVFUYIVWTSZUYJVWTGHIZWWTUYIVWTGHVFWXCWWTSWXBWXCLGGMIZHIZWWTWVQWVRWVRWX CWXESXMWVTWVTLGGUXFYFWXDKLHYMUXGVRTWAAWWSJRWWTJRAVWSGWWMWWPWWQYLALKWWOVYMAW RTZAKKUXHRAXATUXIZYLYNAWWKWWNWWMWWRYNVWSVWTVAAVWSVWTYPVWSPYQYRPVWTYQYRVWSVW TYQYRUXJLGYSYTUXKUXLUXMVWSPVWTYPYELGYSYTUQUXNUXOYHUXPTUXQAWXAVYCKHIZWWTNIZU YTAWWSWXHWWTNAVWSGMIZWXDHIWWSWXHAVWSGGWWMWWPWWPWWQWWQUXRAWXJVYCWXDKHAGWWPUX SWXDKSAYMTVHWTVGAVYCLNIZKHIVWSKHIZWXIUYTAWXKVWSKHALVYCNILGUJIZWXKVWSLGXMUPV PALVYCWWOAGWWPWSZUXTWXMVWSSAGLUJIZULWXMVWSGLUPXMUYAWXOQGLQUPXMVNUYBVQYIUYCT UYDVGAVYCLKWXNWWOWXFWXGUYEAUYTWXLAQKWWLWXFWXGUYFUSUYGWAWAWAWA $. $}