Metamath Proof Explorer

Theorem smupvallem

Description: If A only has elements less than N , then all elements of the partial sum sequence past N already equal the final value. (Contributed by Mario Carneiro, 20-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 )
smupvallem.a 
|- ( ph -> A C_ ( 0 ..^ N ) )
smupvallem.m 
|- ( ph -> M e. ( ZZ>= ` N ) )
Assertion smupvallem 
|- ( ph -> ( P ` M ) = ( A smul 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 smupvallem.a 
 |-  ( ph -> A C_ ( 0 ..^ N ) )
6 smupvallem.m 
 |-  ( ph -> M e. ( ZZ>= ` N ) )
7 1 2 3 smupf 
 |-  ( ph -> P : NN0 --> ~P NN0 )
8 eluznn0 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) ) -> M e. NN0 )
9 4 6 8 syl2anc 
 |-  ( ph -> M e. NN0 )
10 7 9 ffvelrnd 
 |-  ( ph -> ( P ` M ) e. ~P NN0 )
11 10 elpwid 
 |-  ( ph -> ( P ` M ) C_ NN0 )
12 11 sseld 
 |-  ( ph -> ( k e. ( P ` M ) -> k e. NN0 ) )
13 1 2 3 smufval 
 |-  ( ph -> ( A smul B ) = { k e. NN0 | k e. ( P ` ( k + 1 ) ) } )
14 ssrab2 
 |-  { k e. NN0 | k e. ( P ` ( k + 1 ) ) } C_ NN0
15 13 14 eqsstrdi 
 |-  ( ph -> ( A smul B ) C_ NN0 )
16 15 sseld 
 |-  ( ph -> ( k e. ( A smul B ) -> k e. NN0 ) )
17 1 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ N e. ( ZZ>= ` ( k + 1 ) ) ) -> A C_ NN0 )
18 2 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ N e. ( ZZ>= ` ( k + 1 ) ) ) -> B C_ NN0 )
19 simplr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ N e. ( ZZ>= ` ( k + 1 ) ) ) -> k e. NN0 )
20 6 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> M e. ( ZZ>= ` N ) )
21 uztrn 
 |-  ( ( M e. ( ZZ>= ` N ) /\ N e. ( ZZ>= ` ( k + 1 ) ) ) -> M e. ( ZZ>= ` ( k + 1 ) ) )
22 20 21 sylan 
 |-  ( ( ( ph /\ k e. NN0 ) /\ N e. ( ZZ>= ` ( k + 1 ) ) ) -> M e. ( ZZ>= ` ( k + 1 ) ) )
23 17 18 3 19 22 smuval2 
 |-  ( ( ( ph /\ k e. NN0 ) /\ N e. ( ZZ>= ` ( k + 1 ) ) ) -> ( k e. ( A smul B ) <-> k e. ( P ` M ) ) )
24 23 bicomd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ N e. ( ZZ>= ` ( k + 1 ) ) ) -> ( k e. ( P ` M ) <-> k e. ( A smul B ) ) )
25 6 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( k + 1 ) e. ( ZZ>= ` N ) ) -> M e. ( ZZ>= ` N ) )
26 simpll 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( k + 1 ) e. ( ZZ>= ` N ) ) -> ph )
27 fveqeq2 
 |-  ( x = N -> ( ( P ` x ) = ( P ` N ) <-> ( P ` N ) = ( P ` N ) ) )
28 27 imbi2d 
 |-  ( x = N -> ( ( ph -> ( P ` x ) = ( P ` N ) ) <-> ( ph -> ( P ` N ) = ( P ` N ) ) ) )
29 fveqeq2 
 |-  ( x = k -> ( ( P ` x ) = ( P ` N ) <-> ( P ` k ) = ( P ` N ) ) )
30 29 imbi2d 
 |-  ( x = k -> ( ( ph -> ( P ` x ) = ( P ` N ) ) <-> ( ph -> ( P ` k ) = ( P ` N ) ) ) )
31 fveqeq2 
 |-  ( x = ( k + 1 ) -> ( ( P ` x ) = ( P ` N ) <-> ( P ` ( k + 1 ) ) = ( P ` N ) ) )
32 31 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( ph -> ( P ` x ) = ( P ` N ) ) <-> ( ph -> ( P ` ( k + 1 ) ) = ( P ` N ) ) ) )
33 fveqeq2 
 |-  ( x = M -> ( ( P ` x ) = ( P ` N ) <-> ( P ` M ) = ( P ` N ) ) )
34 33 imbi2d 
 |-  ( x = M -> ( ( ph -> ( P ` x ) = ( P ` N ) ) <-> ( ph -> ( P ` M ) = ( P ` N ) ) ) )
35 eqidd 
 |-  ( ph -> ( P ` N ) = ( P ` N ) )
36 1 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> A C_ NN0 )
37 2 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> B C_ NN0 )
38 eluznn0 
 |-  ( ( N e. NN0 /\ k e. ( ZZ>= ` N ) ) -> k e. NN0 )
39 4 38 sylan 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> k e. NN0 )
40 36 37 3 39 smupp1 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( P ` ( k + 1 ) ) = ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) )
41 4 nn0red 
 |-  ( ph -> N e. RR )
42 41 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> N e. RR )
43 39 nn0red 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> k e. RR )
44 eluzle 
 |-  ( k e. ( ZZ>= ` N ) -> N <_ k )
45 44 adantl 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> N <_ k )
46 42 43 45 lensymd 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> -. k < N )
47 5 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> A C_ ( 0 ..^ N ) )
48 47 sseld 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( k e. A -> k e. ( 0 ..^ N ) ) )
49 elfzolt2 
 |-  ( k e. ( 0 ..^ N ) -> k < N )
50 48 49 syl6 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( k e. A -> k < N ) )
51 50 adantrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( k e. A /\ ( n - k ) e. B ) -> k < N ) )
52 46 51 mtod 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> -. ( k e. A /\ ( n - k ) e. B ) )
53 52 ralrimivw 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> A. n e. NN0 -. ( k e. A /\ ( n - k ) e. B ) )
54 rabeq0 
 |-  ( { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } = (/) <-> A. n e. NN0 -. ( k e. A /\ ( n - k ) e. B ) )
55 53 54 sylibr 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } = (/) )
56 55 oveq2d 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( P ` k ) sadd { n e. NN0 | ( k e. A /\ ( n - k ) e. B ) } ) = ( ( P ` k ) sadd (/) ) )
57 7 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> P : NN0 --> ~P NN0 )
58 57 39 ffvelrnd 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( P ` k ) e. ~P NN0 )
59 58 elpwid 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( P ` k ) C_ NN0 )
60 sadid1 
 |-  ( ( P ` k ) C_ NN0 -> ( ( P ` k ) sadd (/) ) = ( P ` k ) )
61 59 60 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( P ` k ) sadd (/) ) = ( P ` k ) )
62 40 56 61 3eqtrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( P ` ( k + 1 ) ) = ( P ` k ) )
63 62 eqeq1d 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( P ` ( k + 1 ) ) = ( P ` N ) <-> ( P ` k ) = ( P ` N ) ) )
64 63 biimprd 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( P ` k ) = ( P ` N ) -> ( P ` ( k + 1 ) ) = ( P ` N ) ) )
65 64 expcom 
 |-  ( k e. ( ZZ>= ` N ) -> ( ph -> ( ( P ` k ) = ( P ` N ) -> ( P ` ( k + 1 ) ) = ( P ` N ) ) ) )
66 65 a2d 
 |-  ( k e. ( ZZ>= ` N ) -> ( ( ph -> ( P ` k ) = ( P ` N ) ) -> ( ph -> ( P ` ( k + 1 ) ) = ( P ` N ) ) ) )
67 28 30 32 34 35 66 uzind4i 
 |-  ( M e. ( ZZ>= ` N ) -> ( ph -> ( P ` M ) = ( P ` N ) ) )
68 25 26 67 sylc 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( k + 1 ) e. ( ZZ>= ` N ) ) -> ( P ` M ) = ( P ` N ) )
69 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( k + 1 ) e. ( ZZ>= ` N ) ) -> ( k + 1 ) e. ( ZZ>= ` N ) )
70 28 30 32 32 35 66 uzind4i 
 |-  ( ( k + 1 ) e. ( ZZ>= ` N ) -> ( ph -> ( P ` ( k + 1 ) ) = ( P ` N ) ) )
71 69 26 70 sylc 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( k + 1 ) e. ( ZZ>= ` N ) ) -> ( P ` ( k + 1 ) ) = ( P ` N ) )
72 68 71 eqtr4d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( k + 1 ) e. ( ZZ>= ` N ) ) -> ( P ` M ) = ( P ` ( k + 1 ) ) )
73 72 eleq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( k + 1 ) e. ( ZZ>= ` N ) ) -> ( k e. ( P ` M ) <-> k e. ( P ` ( k + 1 ) ) ) )
74 1 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( k + 1 ) e. ( ZZ>= ` N ) ) -> A C_ NN0 )
75 2 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( k + 1 ) e. ( ZZ>= ` N ) ) -> B C_ NN0 )
76 simplr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( k + 1 ) e. ( ZZ>= ` N ) ) -> k e. NN0 )
77 74 75 3 76 smuval 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( k + 1 ) e. ( ZZ>= ` N ) ) -> ( k e. ( A smul B ) <-> k e. ( P ` ( k + 1 ) ) ) )
78 73 77 bitr4d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( k + 1 ) e. ( ZZ>= ` N ) ) -> ( k e. ( P ` M ) <-> k e. ( A smul B ) ) )
79 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
80 79 nn0zd 
 |-  ( ( ph /\ k e. NN0 ) -> k e. ZZ )
81 80 peano2zd 
 |-  ( ( ph /\ k e. NN0 ) -> ( k + 1 ) e. ZZ )
82 4 nn0zd 
 |-  ( ph -> N e. ZZ )
83 82 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> N e. ZZ )
84 uztric 
 |-  ( ( ( k + 1 ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( k + 1 ) ) \/ ( k + 1 ) e. ( ZZ>= ` N ) ) )
85 81 83 84 syl2anc 
 |-  ( ( ph /\ k e. NN0 ) -> ( N e. ( ZZ>= ` ( k + 1 ) ) \/ ( k + 1 ) e. ( ZZ>= ` N ) ) )
86 24 78 85 mpjaodan 
 |-  ( ( ph /\ k e. NN0 ) -> ( k e. ( P ` M ) <-> k e. ( A smul B ) ) )
87 86 ex 
 |-  ( ph -> ( k e. NN0 -> ( k e. ( P ` M ) <-> k e. ( A smul B ) ) ) )
88 12 16 87 pm5.21ndd 
 |-  ( ph -> ( k e. ( P ` M ) <-> k e. ( A smul B ) ) )
89 88 eqrdv 
 |-  ( ph -> ( P ` M ) = ( A smul B ) )