Metamath Proof Explorer

Theorem iscmet3lem3

Description: Lemma for iscmet3 . (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypothesis iscmet3.1 
|- Z = ( ZZ>= ` M )
Assertion iscmet3lem3 
|- ( ( M e. ZZ /\ R e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( 1 / 2 ) ^ k ) < R )

Proof

Step Hyp Ref Expression
1 iscmet3.1 
 |-  Z = ( ZZ>= ` M )
2 simpl 
 |-  ( ( M e. ZZ /\ R e. RR+ ) -> M e. ZZ )
3 simpr 
 |-  ( ( M e. ZZ /\ R e. RR+ ) -> R e. RR+ )
4 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
5 4 1 eleq2s 
 |-  ( k e. Z -> k e. ZZ )
6 5 adantl 
 |-  ( ( ( M e. ZZ /\ R e. RR+ ) /\ k e. Z ) -> k e. ZZ )
7 oveq2 
 |-  ( n = k -> ( ( 1 / 2 ) ^ n ) = ( ( 1 / 2 ) ^ k ) )
8 eqid 
 |-  ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) = ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) )
9 ovex 
 |-  ( ( 1 / 2 ) ^ k ) e. _V
10 7 8 9 fvmpt 
 |-  ( k e. ZZ -> ( ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) ` k ) = ( ( 1 / 2 ) ^ k ) )
11 6 10 syl 
 |-  ( ( ( M e. ZZ /\ R e. RR+ ) /\ k e. Z ) -> ( ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) ` k ) = ( ( 1 / 2 ) ^ k ) )
12 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
13 12 reseq2i 
 |-  ( ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) |` NN0 ) = ( ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) |` ( ZZ>= ` 0 ) )
14 nn0ssz 
 |-  NN0 C_ ZZ
15 resmpt 
 |-  ( NN0 C_ ZZ -> ( ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) |` NN0 ) = ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) )
16 14 15 ax-mp 
 |-  ( ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) |` NN0 ) = ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) )
17 13 16 eqtr3i 
 |-  ( ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) |` ( ZZ>= ` 0 ) ) = ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) )
18 halfcn 
 |-  ( 1 / 2 ) e. CC
19 18 a1i 
 |-  ( ( M e. ZZ /\ R e. RR+ ) -> ( 1 / 2 ) e. CC )
20 halfre 
 |-  ( 1 / 2 ) e. RR
21 halfge0 
 |-  0 <_ ( 1 / 2 )
22 absid 
 |-  ( ( ( 1 / 2 ) e. RR /\ 0 <_ ( 1 / 2 ) ) -> ( abs ` ( 1 / 2 ) ) = ( 1 / 2 ) )
23 20 21 22 mp2an 
 |-  ( abs ` ( 1 / 2 ) ) = ( 1 / 2 )
24 halflt1 
 |-  ( 1 / 2 ) < 1
25 23 24 eqbrtri 
 |-  ( abs ` ( 1 / 2 ) ) < 1
26 25 a1i 
 |-  ( ( M e. ZZ /\ R e. RR+ ) -> ( abs ` ( 1 / 2 ) ) < 1 )
27 19 26 expcnv 
 |-  ( ( M e. ZZ /\ R e. RR+ ) -> ( n e. NN0 |-> ( ( 1 / 2 ) ^ n ) ) ~~> 0 )
28 17 27 eqbrtrid 
 |-  ( ( M e. ZZ /\ R e. RR+ ) -> ( ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) |` ( ZZ>= ` 0 ) ) ~~> 0 )
29 0z 
 |-  0 e. ZZ
30 zex 
 |-  ZZ e. _V
31 30 mptex 
 |-  ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) e. _V
32 31 a1i 
 |-  ( ( M e. ZZ /\ R e. RR+ ) -> ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) e. _V )
33 climres 
 |-  ( ( 0 e. ZZ /\ ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) e. _V ) -> ( ( ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) |` ( ZZ>= ` 0 ) ) ~~> 0 <-> ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) ~~> 0 ) )
34 29 32 33 sylancr 
 |-  ( ( M e. ZZ /\ R e. RR+ ) -> ( ( ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) |` ( ZZ>= ` 0 ) ) ~~> 0 <-> ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) ~~> 0 ) )
35 28 34 mpbid 
 |-  ( ( M e. ZZ /\ R e. RR+ ) -> ( n e. ZZ |-> ( ( 1 / 2 ) ^ n ) ) ~~> 0 )
36 1 2 3 11 35 climi0 
 |-  ( ( M e. ZZ /\ R e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( 1 / 2 ) ^ k ) ) < R )
37 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
38 1rp 
 |-  1 e. RR+
39 rphalfcl 
 |-  ( 1 e. RR+ -> ( 1 / 2 ) e. RR+ )
40 38 39 ax-mp 
 |-  ( 1 / 2 ) e. RR+
41 rpexpcl 
 |-  ( ( ( 1 / 2 ) e. RR+ /\ k e. ZZ ) -> ( ( 1 / 2 ) ^ k ) e. RR+ )
42 40 6 41 sylancr 
 |-  ( ( ( M e. ZZ /\ R e. RR+ ) /\ k e. Z ) -> ( ( 1 / 2 ) ^ k ) e. RR+ )
43 rpre 
 |-  ( ( ( 1 / 2 ) ^ k ) e. RR+ -> ( ( 1 / 2 ) ^ k ) e. RR )
44 rpge0 
 |-  ( ( ( 1 / 2 ) ^ k ) e. RR+ -> 0 <_ ( ( 1 / 2 ) ^ k ) )
45 43 44 absidd 
 |-  ( ( ( 1 / 2 ) ^ k ) e. RR+ -> ( abs ` ( ( 1 / 2 ) ^ k ) ) = ( ( 1 / 2 ) ^ k ) )
46 42 45 syl 
 |-  ( ( ( M e. ZZ /\ R e. RR+ ) /\ k e. Z ) -> ( abs ` ( ( 1 / 2 ) ^ k ) ) = ( ( 1 / 2 ) ^ k ) )
47 46 breq1d 
 |-  ( ( ( M e. ZZ /\ R e. RR+ ) /\ k e. Z ) -> ( ( abs ` ( ( 1 / 2 ) ^ k ) ) < R <-> ( ( 1 / 2 ) ^ k ) < R ) )
48 37 47 sylan2 
 |-  ( ( ( M e. ZZ /\ R e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( ( 1 / 2 ) ^ k ) ) < R <-> ( ( 1 / 2 ) ^ k ) < R ) )
49 48 anassrs 
 |-  ( ( ( ( M e. ZZ /\ R e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( 1 / 2 ) ^ k ) ) < R <-> ( ( 1 / 2 ) ^ k ) < R ) )
50 49 ralbidva 
 |-  ( ( ( M e. ZZ /\ R e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( 1 / 2 ) ^ k ) ) < R <-> A. k e. ( ZZ>= ` j ) ( ( 1 / 2 ) ^ k ) < R ) )
51 50 rexbidva 
 |-  ( ( M e. ZZ /\ R e. RR+ ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( 1 / 2 ) ^ k ) ) < R <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( 1 / 2 ) ^ k ) < R ) )
52 36 51 mpbid 
 |-  ( ( M e. ZZ /\ R e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( 1 / 2 ) ^ k ) < R )