Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  smupf Unicode version

Theorem smupf 12945
 Description: The sequence of partial sums of the sequence multiplication. (Contributed by Mario Carneiro, 9-Sep-2016.)
Hypotheses
Ref Expression
smuval.a
smuval.b
Assertion
Ref Expression
smupf
Distinct variable groups:   ,,,   ,   ,,,
Allowed substitution hints:   (,)   (,,)

Proof of Theorem smupf
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0nn0 10192 . . . . 5
2 iftrue 3705 . . . . . 6
3 eqid 2404 . . . . . 6
4 0ex 4299 . . . . . 6
52, 3, 4fvmpt 5765 . . . . 5
61, 5mp1i 12 . . . 4
7 0elpw 4329 . . . 4
86, 7syl6eqel 2492 . . 3
10 elpwi 3767 . . . . . . . . . . 11
1110adantr 452 . . . . . . . . . 10
12 ssrab2 3388 . . . . . . . . . 10
13 sadcl 12929 . . . . . . . . . 10 sadd
1411, 12, 13sylancl 644 . . . . . . . . 9 sadd
15 nn0ex 10183 . . . . . . . . . 10
1615elpw2 4324 . . . . . . . . 9 sadd sadd
1714, 16sylibr 204 . . . . . . . 8 sadd
1817rgen2 2762 . . . . . . 7 sadd
19 eqid 2404 . . . . . . . 8 sadd sadd
2118, 20mpbi 200 . . . . . 6 sadd
2221, 7f0cli 5839 . . . . 5 sadd
239, 22eqeltri 2474 . . . 4 sadd
2423a1i 11 . . 3 sadd
25 nn0uz 10476 . . 3
26 0z 10249 . . . 4
2726a1i 11 . . 3
28 fvex 5701 . . . 4
2928a1i 11 . . 3
308, 24, 25, 27, 29seqf2 11297 . 2 sadd
31 smuval.p . . 3 sadd