Metamath Proof Explorer

Theorem rpnnen2lem10

Description: Lemma for rpnnen2 . (Contributed by Mario Carneiro, 13-May-2013) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Hypotheses rpnnen2.1 
|- F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
rpnnen2.2 
|- ( ph -> A C_ NN )
rpnnen2.3 
|- ( ph -> B C_ NN )
rpnnen2.4 
|- ( ph -> m e. ( A \ B ) )
rpnnen2.5 
|- ( ph -> A. n e. NN ( n < m -> ( n e. A <-> n e. B ) ) )
rpnnen2.6 
|- ( ps <-> sum_ k e. NN ( ( F ` A ) ` k ) = sum_ k e. NN ( ( F ` B ) ` k ) )
Assertion rpnnen2lem10 
|- ( ( ph /\ ps ) -> sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) = sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) )

Proof

Step Hyp Ref Expression
1 rpnnen2.1 
 |-  F = ( x e. ~P NN |-> ( n e. NN |-> if ( n e. x , ( ( 1 / 3 ) ^ n ) , 0 ) ) )
2 rpnnen2.2 
 |-  ( ph -> A C_ NN )
3 rpnnen2.3 
 |-  ( ph -> B C_ NN )
4 rpnnen2.4 
 |-  ( ph -> m e. ( A \ B ) )
5 rpnnen2.5 
 |-  ( ph -> A. n e. NN ( n < m -> ( n e. A <-> n e. B ) ) )
6 rpnnen2.6 
 |-  ( ps <-> sum_ k e. NN ( ( F ` A ) ` k ) = sum_ k e. NN ( ( F ` B ) ` k ) )
7 6 bilani 
 |-  ( ( ph /\ ps ) -> sum_ k e. NN ( ( F ` A ) ` k ) = sum_ k e. NN ( ( F ` B ) ` k ) )
8 eldifi 
 |-  ( m e. ( A \ B ) -> m e. A )
9 ssel2 
 |-  ( ( A C_ NN /\ m e. A ) -> m e. NN )
10 8 9 sylan2 
 |-  ( ( A C_ NN /\ m e. ( A \ B ) ) -> m e. NN )
11 2 4 10 syl2anc 
 |-  ( ph -> m e. NN )
12 1 rpnnen2lem8 
 |-  ( ( A C_ NN /\ m e. NN ) -> sum_ k e. NN ( ( F ` A ) ` k ) = ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` A ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) ) )
13 2 11 12 syl2anc 
 |-  ( ph -> sum_ k e. NN ( ( F ` A ) ` k ) = ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` A ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) ) )
14 1z 
 |-  1 e. ZZ
15 nnz 
 |-  ( m e. NN -> m e. ZZ )
16 elfzm11 
 |-  ( ( 1 e. ZZ /\ m e. ZZ ) -> ( k e. ( 1 ... ( m - 1 ) ) <-> ( k e. ZZ /\ 1 <_ k /\ k < m ) ) )
17 14 15 16 sylancr 
 |-  ( m e. NN -> ( k e. ( 1 ... ( m - 1 ) ) <-> ( k e. ZZ /\ 1 <_ k /\ k < m ) ) )
18 17 biimpa 
 |-  ( ( m e. NN /\ k e. ( 1 ... ( m - 1 ) ) ) -> ( k e. ZZ /\ 1 <_ k /\ k < m ) )
19 11 18 sylan 
 |-  ( ( ph /\ k e. ( 1 ... ( m - 1 ) ) ) -> ( k e. ZZ /\ 1 <_ k /\ k < m ) )
20 19 simp3d 
 |-  ( ( ph /\ k e. ( 1 ... ( m - 1 ) ) ) -> k < m )
21 elfznn 
 |-  ( k e. ( 1 ... ( m - 1 ) ) -> k e. NN )
22 breq1 
 |-  ( n = k -> ( n < m <-> k < m ) )
23 eleq1w 
 |-  ( n = k -> ( n e. A <-> k e. A ) )
24 eleq1w 
 |-  ( n = k -> ( n e. B <-> k e. B ) )
25 23 24 bibi12d 
 |-  ( n = k -> ( ( n e. A <-> n e. B ) <-> ( k e. A <-> k e. B ) ) )
26 22 25 imbi12d 
 |-  ( n = k -> ( ( n < m -> ( n e. A <-> n e. B ) ) <-> ( k < m -> ( k e. A <-> k e. B ) ) ) )
27 26 rspccva 
 |-  ( ( A. n e. NN ( n < m -> ( n e. A <-> n e. B ) ) /\ k e. NN ) -> ( k < m -> ( k e. A <-> k e. B ) ) )
28 5 21 27 syl2an 
 |-  ( ( ph /\ k e. ( 1 ... ( m - 1 ) ) ) -> ( k < m -> ( k e. A <-> k e. B ) ) )
29 20 28 mpd 
 |-  ( ( ph /\ k e. ( 1 ... ( m - 1 ) ) ) -> ( k e. A <-> k e. B ) )
30 29 ifbid 
 |-  ( ( ph /\ k e. ( 1 ... ( m - 1 ) ) ) -> if ( k e. A , ( ( 1 / 3 ) ^ k ) , 0 ) = if ( k e. B , ( ( 1 / 3 ) ^ k ) , 0 ) )
31 1 rpnnen2lem1 
 |-  ( ( A C_ NN /\ k e. NN ) -> ( ( F ` A ) ` k ) = if ( k e. A , ( ( 1 / 3 ) ^ k ) , 0 ) )
32 2 21 31 syl2an 
 |-  ( ( ph /\ k e. ( 1 ... ( m - 1 ) ) ) -> ( ( F ` A ) ` k ) = if ( k e. A , ( ( 1 / 3 ) ^ k ) , 0 ) )
33 1 rpnnen2lem1 
 |-  ( ( B C_ NN /\ k e. NN ) -> ( ( F ` B ) ` k ) = if ( k e. B , ( ( 1 / 3 ) ^ k ) , 0 ) )
34 3 21 33 syl2an 
 |-  ( ( ph /\ k e. ( 1 ... ( m - 1 ) ) ) -> ( ( F ` B ) ` k ) = if ( k e. B , ( ( 1 / 3 ) ^ k ) , 0 ) )
35 30 32 34 3eqtr4d 
 |-  ( ( ph /\ k e. ( 1 ... ( m - 1 ) ) ) -> ( ( F ` A ) ` k ) = ( ( F ` B ) ` k ) )
36 35 sumeq2dv 
 |-  ( ph -> sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` A ) ` k ) = sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) )
37 36 oveq1d 
 |-  ( ph -> ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` A ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) ) = ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) ) )
38 13 37 eqtrd 
 |-  ( ph -> sum_ k e. NN ( ( F ` A ) ` k ) = ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) ) )
39 38 adantr 
 |-  ( ( ph /\ ps ) -> sum_ k e. NN ( ( F ` A ) ` k ) = ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) ) )
40 1 rpnnen2lem8 
 |-  ( ( B C_ NN /\ m e. NN ) -> sum_ k e. NN ( ( F ` B ) ` k ) = ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) ) )
41 3 11 40 syl2anc 
 |-  ( ph -> sum_ k e. NN ( ( F ` B ) ` k ) = ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) ) )
42 41 adantr 
 |-  ( ( ph /\ ps ) -> sum_ k e. NN ( ( F ` B ) ` k ) = ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) ) )
43 7 39 42 3eqtr3d 
 |-  ( ( ph /\ ps ) -> ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) ) = ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) ) )
44 1 rpnnen2lem6 
 |-  ( ( A C_ NN /\ m e. NN ) -> sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) e. RR )
45 2 11 44 syl2anc 
 |-  ( ph -> sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) e. RR )
46 1 rpnnen2lem6 
 |-  ( ( B C_ NN /\ m e. NN ) -> sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) e. RR )
47 3 11 46 syl2anc 
 |-  ( ph -> sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) e. RR )
48 fzfid 
 |-  ( ph -> ( 1 ... ( m - 1 ) ) e. Fin )
49 1 rpnnen2lem2 
 |-  ( B C_ NN -> ( F ` B ) : NN --> RR )
50 3 49 syl 
 |-  ( ph -> ( F ` B ) : NN --> RR )
51 ffvelcdm 
 |-  ( ( ( F ` B ) : NN --> RR /\ k e. NN ) -> ( ( F ` B ) ` k ) e. RR )
52 50 21 51 syl2an 
 |-  ( ( ph /\ k e. ( 1 ... ( m - 1 ) ) ) -> ( ( F ` B ) ` k ) e. RR )
53 48 52 fsumrecl 
 |-  ( ph -> sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) e. RR )
54 readdcan 
 |-  ( ( sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) e. RR /\ sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) e. RR /\ sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) e. RR ) -> ( ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) ) = ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) ) <-> sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) = sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) ) )
55 45 47 53 54 syl3anc 
 |-  ( ph -> ( ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) ) = ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) ) <-> sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) = sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) ) )
56 55 adantr 
 |-  ( ( ph /\ ps ) -> ( ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) ) = ( sum_ k e. ( 1 ... ( m - 1 ) ) ( ( F ` B ) ` k ) + sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) ) <-> sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) = sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) ) )
57 43 56 mpbid 
 |-  ( ( ph /\ ps ) -> sum_ k e. ( ZZ>= ` m ) ( ( F ` A ) ` k ) = sum_ k e. ( ZZ>= ` m ) ( ( F ` B ) ` k ) )