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 
|- ( ph -> A C_ NN0 )
smuval.b 
|- ( ph -> B C_ NN0 )
smuval.p 
|- P = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
smuval.n 
|- ( ph -> N e. NN0 )
Assertion smupp1 
|- ( ph -> ( P ` ( N + 1 ) ) = ( ( P ` N ) sadd { n e. NN0 | ( N e. A /\ ( n - N ) e. B ) } ) )

Proof

Step Hyp Ref Expression
1 smuval.a 
 |-  ( ph -> A C_ NN0 )
2 smuval.b 
 |-  ( ph -> B C_ NN0 )
3 smuval.p 
 |-  P = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
4 smuval.n 
 |-  ( ph -> N e. NN0 )
5 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
6 4 5 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
7 seqp1 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( N + 1 ) ) = ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` N ) ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` ( N + 1 ) ) ) )
8 6 7 syl 
 |-  ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( N + 1 ) ) = ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` N ) ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` ( N + 1 ) ) ) )
9 3 fveq1i 
 |-  ( P ` ( N + 1 ) ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( N + 1 ) )
10 3 fveq1i 
 |-  ( P ` N ) = ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` N )
11 10 oveq1i 
 |-  ( ( P ` N ) ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` ( N + 1 ) ) ) = ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` N ) ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` ( N + 1 ) ) )
12 8 9 11 3eqtr4g 
 |-  ( ph -> ( P ` ( N + 1 ) ) = ( ( P ` N ) ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` ( N + 1 ) ) ) )
13 1nn0 
 |-  1 e. NN0
14 13 a1i 
 |-  ( ph -> 1 e. NN0 )
15 4 14 nn0addcld 
 |-  ( ph -> ( N + 1 ) e. NN0 )
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 e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) = ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) )
20 0ex 
 |-  (/) e. _V
21 ovex 
 |-  ( ( N + 1 ) - 1 ) e. _V
22 20 21 ifex 
 |-  if ( ( N + 1 ) = 0 , (/) , ( ( N + 1 ) - 1 ) ) e. _V
23 18 19 22 fvmpt 
 |-  ( ( N + 1 ) e. NN0 -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` ( N + 1 ) ) = if ( ( N + 1 ) = 0 , (/) , ( ( N + 1 ) - 1 ) ) )
24 15 23 syl 
 |-  ( ph -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` ( N + 1 ) ) = if ( ( N + 1 ) = 0 , (/) , ( ( N + 1 ) - 1 ) ) )
25 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
26 4 25 syl 
 |-  ( ph -> ( N + 1 ) e. NN )
27 26 nnne0d 
 |-  ( ph -> ( N + 1 ) =/= 0 )
28 ifnefalse 
 |-  ( ( N + 1 ) =/= 0 -> if ( ( N + 1 ) = 0 , (/) , ( ( N + 1 ) - 1 ) ) = ( ( N + 1 ) - 1 ) )
29 27 28 syl 
 |-  ( ph -> if ( ( N + 1 ) = 0 , (/) , ( ( N + 1 ) - 1 ) ) = ( ( N + 1 ) - 1 ) )
30 4 nn0cnd 
 |-  ( ph -> N e. CC )
31 14 nn0cnd 
 |-  ( ph -> 1 e. CC )
32 30 31 pncand 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
33 24 29 32 3eqtrd 
 |-  ( ph -> ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` ( N + 1 ) ) = N )
34 33 oveq2d 
 |-  ( ph -> ( ( P ` N ) ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) ( ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ` ( N + 1 ) ) ) = ( ( P ` N ) ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) N ) )
35 1 2 3 smupf 
 |-  ( ph -> P : NN0 --> ~P NN0 )
36 35 4 ffvelcdmd 
 |-  ( ph -> ( P ` N ) e. ~P NN0 )
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 e. A <-> N e. A ) )
40 38 oveq2d 
 |-  ( ( x = ( P ` N ) /\ y = N ) -> ( k - y ) = ( k - N ) )
41 40 eleq1d 
 |-  ( ( x = ( P ` N ) /\ y = N ) -> ( ( k - y ) e. B <-> ( k - N ) e. B ) )
42 39 41 anbi12d 
 |-  ( ( x = ( P ` N ) /\ y = N ) -> ( ( y e. A /\ ( k - y ) e. B ) <-> ( N e. A /\ ( k - N ) e. B ) ) )
43 42 rabbidv 
 |-  ( ( x = ( P ` N ) /\ y = N ) -> { k e. NN0 | ( y e. A /\ ( k - y ) e. B ) } = { k e. NN0 | ( N e. A /\ ( k - N ) e. B ) } )
44 oveq1 
 |-  ( k = n -> ( k - N ) = ( n - N ) )
45 44 eleq1d 
 |-  ( k = n -> ( ( k - N ) e. B <-> ( n - N ) e. B ) )
46 45 anbi2d 
 |-  ( k = n -> ( ( N e. A /\ ( k - N ) e. B ) <-> ( N e. A /\ ( n - N ) e. B ) ) )
47 46 cbvrabv 
 |-  { k e. NN0 | ( N e. A /\ ( k - N ) e. B ) } = { n e. NN0 | ( N e. A /\ ( n - N ) e. B ) }
48 43 47 eqtrdi 
 |-  ( ( x = ( P ` N ) /\ y = N ) -> { k e. NN0 | ( y e. A /\ ( k - y ) e. B ) } = { n e. NN0 | ( N e. A /\ ( n - N ) e. B ) } )
49 37 48 oveq12d 
 |-  ( ( x = ( P ` N ) /\ y = N ) -> ( x sadd { k e. NN0 | ( y e. A /\ ( k - y ) e. B ) } ) = ( ( P ` N ) sadd { n e. NN0 | ( N e. A /\ ( n - N ) e. B ) } ) )
50 oveq1 
 |-  ( p = x -> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) = ( x sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) )
51 eleq1w 
 |-  ( m = y -> ( m e. A <-> y e. A ) )
52 oveq2 
 |-  ( m = y -> ( n - m ) = ( n - y ) )
53 52 eleq1d 
 |-  ( m = y -> ( ( n - m ) e. B <-> ( n - y ) e. B ) )
54 51 53 anbi12d 
 |-  ( m = y -> ( ( m e. A /\ ( n - m ) e. B ) <-> ( y e. A /\ ( n - y ) e. B ) ) )
55 54 rabbidv 
 |-  ( m = y -> { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } = { n e. NN0 | ( y e. A /\ ( n - y ) e. B ) } )
56 oveq1 
 |-  ( k = n -> ( k - y ) = ( n - y ) )
57 56 eleq1d 
 |-  ( k = n -> ( ( k - y ) e. B <-> ( n - y ) e. B ) )
58 57 anbi2d 
 |-  ( k = n -> ( ( y e. A /\ ( k - y ) e. B ) <-> ( y e. A /\ ( n - y ) e. B ) ) )
59 58 cbvrabv 
 |-  { k e. NN0 | ( y e. A /\ ( k - y ) e. B ) } = { n e. NN0 | ( y e. A /\ ( n - y ) e. B ) }
60 55 59 eqtr4di 
 |-  ( m = y -> { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } = { k e. NN0 | ( y e. A /\ ( k - y ) e. B ) } )
61 60 oveq2d 
 |-  ( m = y -> ( x sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) = ( x sadd { k e. NN0 | ( y e. A /\ ( k - y ) e. B ) } ) )
62 50 61 cbvmpov 
 |-  ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) = ( x e. ~P NN0 , y e. NN0 |-> ( x sadd { k e. NN0 | ( y e. A /\ ( k - y ) e. B ) } ) )
63 ovex 
 |-  ( ( P ` N ) sadd { n e. NN0 | ( N e. A /\ ( n - N ) e. B ) } ) e. _V
64 49 62 63 ovmpoa 
 |-  ( ( ( P ` N ) e. ~P NN0 /\ N e. NN0 ) -> ( ( P ` N ) ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) N ) = ( ( P ` N ) sadd { n e. NN0 | ( N e. A /\ ( n - N ) e. B ) } ) )
65 36 4 64 syl2anc 
 |-  ( ph -> ( ( P ` N ) ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) N ) = ( ( P ` N ) sadd { n e. NN0 | ( N e. A /\ ( n - N ) e. B ) } ) )
66 12 34 65 3eqtrd 
 |-  ( ph -> ( P ` ( N + 1 ) ) = ( ( P ` N ) sadd { n e. NN0 | ( N e. A /\ ( n - N ) e. B ) } ) )