Metamath Proof Explorer


Theorem smupp1

Description: The initial element of the partial sum sequence. (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses smuval.a φ A 0
smuval.b φ B 0
smuval.p P = seq 0 p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1
smuval.n φ N 0
Assertion smupp1 φ P N + 1 = P N sadd n 0 | N A n N B

Proof

Step Hyp Ref Expression
1 smuval.a φ A 0
2 smuval.b φ B 0
3 smuval.p P = seq 0 p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1
4 smuval.n φ N 0
5 nn0uz 0 = 0
6 4 5 eleqtrdi φ N 0
7 seqp1 N 0 seq 0 p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1 N + 1 = seq 0 p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1 N p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1 N + 1
8 6 7 syl φ seq 0 p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1 N + 1 = seq 0 p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1 N p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1 N + 1
9 3 fveq1i P N + 1 = seq 0 p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1 N + 1
10 3 fveq1i P N = seq 0 p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1 N
11 10 oveq1i P N p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1 N + 1 = seq 0 p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1 N p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1 N + 1
12 8 9 11 3eqtr4g φ P N + 1 = P N p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1 N + 1
13 1nn0 1 0
14 13 a1i φ 1 0
15 4 14 nn0addcld φ N + 1 0
16 eqeq1 n = N + 1 n = 0 N + 1 = 0
17 oveq1 n = N + 1 n 1 = N + 1 - 1
18 16 17 ifbieq2d n = N + 1 if n = 0 n 1 = if N + 1 = 0 N + 1 - 1
19 eqid n 0 if n = 0 n 1 = n 0 if n = 0 n 1
20 0ex V
21 ovex N + 1 - 1 V
22 20 21 ifex if N + 1 = 0 N + 1 - 1 V
23 18 19 22 fvmpt N + 1 0 n 0 if n = 0 n 1 N + 1 = if N + 1 = 0 N + 1 - 1
24 15 23 syl φ n 0 if n = 0 n 1 N + 1 = if N + 1 = 0 N + 1 - 1
25 nn0p1nn N 0 N + 1
26 4 25 syl φ N + 1
27 26 nnne0d φ N + 1 0
28 ifnefalse N + 1 0 if N + 1 = 0 N + 1 - 1 = N + 1 - 1
29 27 28 syl φ if N + 1 = 0 N + 1 - 1 = N + 1 - 1
30 4 nn0cnd φ N
31 14 nn0cnd φ 1
32 30 31 pncand φ N + 1 - 1 = N
33 24 29 32 3eqtrd φ n 0 if n = 0 n 1 N + 1 = N
34 33 oveq2d φ P N p 𝒫 0 , m 0 p sadd n 0 | m A n m B n 0 if n = 0 n 1 N + 1 = P N p 𝒫 0 , m 0 p sadd n 0 | m A n m B N
35 1 2 3 smupf φ P : 0 𝒫 0
36 35 4 ffvelrnd φ P N 𝒫 0
37 simpl x = P N y = N x = P N
38 simpr x = P N y = N y = N
39 38 eleq1d x = P N y = N y A N A
40 38 oveq2d x = P N y = N k y = k N
41 40 eleq1d x = P N y = N k y B k N B
42 39 41 anbi12d x = P N y = N y A k y B N A k N B
43 42 rabbidv x = P N y = N k 0 | y A k y B = k 0 | N A k N B
44 oveq1 k = n k N = n N
45 44 eleq1d k = n k N B n N B
46 45 anbi2d k = n N A k N B N A n N B
47 46 cbvrabv k 0 | N A k N B = n 0 | N A n N B
48 43 47 eqtrdi x = P N y = N k 0 | y A k y B = n 0 | N A n N B
49 37 48 oveq12d x = P N y = N x sadd k 0 | y A k y B = P N sadd n 0 | N A n N B
50 oveq1 p = x p sadd n 0 | m A n m B = x sadd n 0 | m A n m B
51 eleq1w m = y m A y A
52 oveq2 m = y n m = n y
53 52 eleq1d m = y n m B n y B
54 51 53 anbi12d m = y m A n m B y A n y B
55 54 rabbidv m = y n 0 | m A n m B = n 0 | y A n y B
56 oveq1 k = n k y = n y
57 56 eleq1d k = n k y B n y B
58 57 anbi2d k = n y A k y B y A n y B
59 58 cbvrabv k 0 | y A k y B = n 0 | y A n y B
60 55 59 eqtr4di m = y n 0 | m A n m B = k 0 | y A k y B
61 60 oveq2d m = y x sadd n 0 | m A n m B = x sadd k 0 | y A k y B
62 50 61 cbvmpov p 𝒫 0 , m 0 p sadd n 0 | m A n m B = x 𝒫 0 , y 0 x sadd k 0 | y A k y B
63 ovex P N sadd n 0 | N A n N B V
64 49 62 63 ovmpoa P N 𝒫 0 N 0 P N p 𝒫 0 , m 0 p sadd n 0 | m A n m B N = P N sadd n 0 | N A n N B
65 36 4 64 syl2anc φ P N p 𝒫 0 , m 0 p sadd n 0 | m A n m B N = P N sadd n 0 | N A n N B
66 12 34 65 3eqtrd φ P N + 1 = P N sadd n 0 | N A n N B