This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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