Metamath Proof Explorer

Theorem stoweidlem7

Description: This lemma is used to prove that q_n as in the proof of Lemma 1 in BrosowskiDeutsh p. 91, (at the top of page 91), is such that q_n < ε on T \ U , and q_n > 1 - ε on V . Here it is proven that, for n large enough, 1-(k*δ/2)^n > 1 - ε , and 1/(k*δ)^n < ε. The variable A is used to represent (k*δ) in the paper, and B is used to represent (k*δ/2). (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem7.1 
|- F = ( i e. NN0 |-> ( ( 1 / A ) ^ i ) )
stoweidlem7.2 
|- G = ( i e. NN0 |-> ( B ^ i ) )
stoweidlem7.3 
|- ( ph -> A e. RR )
stoweidlem7.4 
|- ( ph -> 1 < A )
stoweidlem7.5 
|- ( ph -> B e. RR+ )
stoweidlem7.6 
|- ( ph -> B < 1 )
stoweidlem7.7 
|- ( ph -> E e. RR+ )
Assertion stoweidlem7 
|- ( ph -> E. n e. NN ( ( 1 - E ) < ( 1 - ( B ^ n ) ) /\ ( 1 / ( A ^ n ) ) < E ) )

Proof

Step Hyp Ref Expression
1 stoweidlem7.1 
 |-  F = ( i e. NN0 |-> ( ( 1 / A ) ^ i ) )
2 stoweidlem7.2 
 |-  G = ( i e. NN0 |-> ( B ^ i ) )
3 stoweidlem7.3 
 |-  ( ph -> A e. RR )
4 stoweidlem7.4 
 |-  ( ph -> 1 < A )
5 stoweidlem7.5 
 |-  ( ph -> B e. RR+ )
6 stoweidlem7.6 
 |-  ( ph -> B < 1 )
7 stoweidlem7.7 
 |-  ( ph -> E e. RR+ )
8 nnuz 
 |-  NN = ( ZZ>= ` 1 )
9 1zzd 
 |-  ( ph -> 1 e. ZZ )
10 oveq2 
 |-  ( i = k -> ( B ^ i ) = ( B ^ k ) )
11 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
12 11 adantl 
 |-  ( ( ph /\ k e. NN ) -> k e. NN0 )
13 5 rpcnd 
 |-  ( ph -> B e. CC )
14 13 adantr 
 |-  ( ( ph /\ k e. NN ) -> B e. CC )
15 14 12 expcld 
 |-  ( ( ph /\ k e. NN ) -> ( B ^ k ) e. CC )
16 2 10 12 15 fvmptd3 
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) = ( B ^ k ) )
17 1red 
 |-  ( ph -> 1 e. RR )
18 17 renegcld 
 |-  ( ph -> -u 1 e. RR )
19 0red 
 |-  ( ph -> 0 e. RR )
20 5 rpred 
 |-  ( ph -> B e. RR )
21 neg1lt0 
 |-  -u 1 < 0
22 21 a1i 
 |-  ( ph -> -u 1 < 0 )
23 5 rpgt0d 
 |-  ( ph -> 0 < B )
24 18 19 20 22 23 lttrd 
 |-  ( ph -> -u 1 < B )
25 20 17 absltd 
 |-  ( ph -> ( ( abs ` B ) < 1 <-> ( -u 1 < B /\ B < 1 ) ) )
26 24 6 25 mpbir2and 
 |-  ( ph -> ( abs ` B ) < 1 )
27 13 26 expcnv 
 |-  ( ph -> ( i e. NN0 |-> ( B ^ i ) ) ~~> 0 )
28 2 27 eqbrtrid 
 |-  ( ph -> G ~~> 0 )
29 8 9 7 16 28 climi 
 |-  ( ph -> E. n e. NN A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) )
30 r19.26 
 |-  ( A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) <-> ( A. k e. ( ZZ>= ` n ) ( B ^ k ) e. CC /\ A. k e. ( ZZ>= ` n ) ( abs ` ( ( B ^ k ) - 0 ) ) < E ) )
31 30 simprbi 
 |-  ( A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) -> A. k e. ( ZZ>= ` n ) ( abs ` ( ( B ^ k ) - 0 ) ) < E )
32 31 ad2antlr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> A. k e. ( ZZ>= ` n ) ( abs ` ( ( B ^ k ) - 0 ) ) < E )
33 oveq2 
 |-  ( k = i -> ( B ^ k ) = ( B ^ i ) )
34 33 oveq1d 
 |-  ( k = i -> ( ( B ^ k ) - 0 ) = ( ( B ^ i ) - 0 ) )
35 34 fveq2d 
 |-  ( k = i -> ( abs ` ( ( B ^ k ) - 0 ) ) = ( abs ` ( ( B ^ i ) - 0 ) ) )
36 35 breq1d 
 |-  ( k = i -> ( ( abs ` ( ( B ^ k ) - 0 ) ) < E <-> ( abs ` ( ( B ^ i ) - 0 ) ) < E ) )
37 36 rspccva 
 |-  ( ( A. k e. ( ZZ>= ` n ) ( abs ` ( ( B ^ k ) - 0 ) ) < E /\ i e. ( ZZ>= ` n ) ) -> ( abs ` ( ( B ^ i ) - 0 ) ) < E )
38 32 37 sylancom 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> ( abs ` ( ( B ^ i ) - 0 ) ) < E )
39 simplll 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> ph )
40 39 5 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> B e. RR+ )
41 40 rpred 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> B e. RR )
42 simpllr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> n e. NN )
43 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
44 42 43 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> n e. NN0 )
45 eluznn0 
 |-  ( ( n e. NN0 /\ i e. ( ZZ>= ` n ) ) -> i e. NN0 )
46 44 45 sylancom 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> i e. NN0 )
47 41 46 reexpcld 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> ( B ^ i ) e. RR )
48 rpre 
 |-  ( E e. RR+ -> E e. RR )
49 39 7 48 3syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> E e. RR )
50 recn 
 |-  ( ( B ^ i ) e. RR -> ( B ^ i ) e. CC )
51 50 subid1d 
 |-  ( ( B ^ i ) e. RR -> ( ( B ^ i ) - 0 ) = ( B ^ i ) )
52 51 adantr 
 |-  ( ( ( B ^ i ) e. RR /\ E e. RR ) -> ( ( B ^ i ) - 0 ) = ( B ^ i ) )
53 52 fveq2d 
 |-  ( ( ( B ^ i ) e. RR /\ E e. RR ) -> ( abs ` ( ( B ^ i ) - 0 ) ) = ( abs ` ( B ^ i ) ) )
54 53 breq1d 
 |-  ( ( ( B ^ i ) e. RR /\ E e. RR ) -> ( ( abs ` ( ( B ^ i ) - 0 ) ) < E <-> ( abs ` ( B ^ i ) ) < E ) )
55 abslt 
 |-  ( ( ( B ^ i ) e. RR /\ E e. RR ) -> ( ( abs ` ( B ^ i ) ) < E <-> ( -u E < ( B ^ i ) /\ ( B ^ i ) < E ) ) )
56 54 55 bitrd 
 |-  ( ( ( B ^ i ) e. RR /\ E e. RR ) -> ( ( abs ` ( ( B ^ i ) - 0 ) ) < E <-> ( -u E < ( B ^ i ) /\ ( B ^ i ) < E ) ) )
57 47 49 56 syl2anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> ( ( abs ` ( ( B ^ i ) - 0 ) ) < E <-> ( -u E < ( B ^ i ) /\ ( B ^ i ) < E ) ) )
58 38 57 mpbid 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> ( -u E < ( B ^ i ) /\ ( B ^ i ) < E ) )
59 58 simprd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> ( B ^ i ) < E )
60 eluznn 
 |-  ( ( n e. NN /\ i e. ( ZZ>= ` n ) ) -> i e. NN )
61 42 60 sylancom 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> i e. NN )
62 20 adantr 
 |-  ( ( ph /\ i e. NN ) -> B e. RR )
63 nnnn0 
 |-  ( i e. NN -> i e. NN0 )
64 63 adantl 
 |-  ( ( ph /\ i e. NN ) -> i e. NN0 )
65 62 64 reexpcld 
 |-  ( ( ph /\ i e. NN ) -> ( B ^ i ) e. RR )
66 7 rpred 
 |-  ( ph -> E e. RR )
67 66 adantr 
 |-  ( ( ph /\ i e. NN ) -> E e. RR )
68 1red 
 |-  ( ( ph /\ i e. NN ) -> 1 e. RR )
69 65 67 68 ltsub2d 
 |-  ( ( ph /\ i e. NN ) -> ( ( B ^ i ) < E <-> ( 1 - E ) < ( 1 - ( B ^ i ) ) ) )
70 39 61 69 syl2anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> ( ( B ^ i ) < E <-> ( 1 - E ) < ( 1 - ( B ^ i ) ) ) )
71 59 70 mpbid 
 |-  ( ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) /\ i e. ( ZZ>= ` n ) ) -> ( 1 - E ) < ( 1 - ( B ^ i ) ) )
72 71 ralrimiva 
 |-  ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) -> A. i e. ( ZZ>= ` n ) ( 1 - E ) < ( 1 - ( B ^ i ) ) )
73 33 oveq2d 
 |-  ( k = i -> ( 1 - ( B ^ k ) ) = ( 1 - ( B ^ i ) ) )
74 73 breq2d 
 |-  ( k = i -> ( ( 1 - E ) < ( 1 - ( B ^ k ) ) <-> ( 1 - E ) < ( 1 - ( B ^ i ) ) ) )
75 74 cbvralvw 
 |-  ( A. k e. ( ZZ>= ` n ) ( 1 - E ) < ( 1 - ( B ^ k ) ) <-> A. i e. ( ZZ>= ` n ) ( 1 - E ) < ( 1 - ( B ^ i ) ) )
76 72 75 sylibr 
 |-  ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) ) -> A. k e. ( ZZ>= ` n ) ( 1 - E ) < ( 1 - ( B ^ k ) ) )
77 76 ex 
 |-  ( ( ph /\ n e. NN ) -> ( A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) -> A. k e. ( ZZ>= ` n ) ( 1 - E ) < ( 1 - ( B ^ k ) ) ) )
78 77 reximdva 
 |-  ( ph -> ( E. n e. NN A. k e. ( ZZ>= ` n ) ( ( B ^ k ) e. CC /\ ( abs ` ( ( B ^ k ) - 0 ) ) < E ) -> E. n e. NN A. k e. ( ZZ>= ` n ) ( 1 - E ) < ( 1 - ( B ^ k ) ) ) )
79 29 78 mpd 
 |-  ( ph -> E. n e. NN A. k e. ( ZZ>= ` n ) ( 1 - E ) < ( 1 - ( B ^ k ) ) )
80 oveq2 
 |-  ( i = k -> ( ( 1 / A ) ^ i ) = ( ( 1 / A ) ^ k ) )
81 3 recnd 
 |-  ( ph -> A e. CC )
82 0lt1 
 |-  0 < 1
83 82 a1i 
 |-  ( ph -> 0 < 1 )
84 19 17 3 83 4 lttrd 
 |-  ( ph -> 0 < A )
85 84 gt0ne0d 
 |-  ( ph -> A =/= 0 )
86 81 85 reccld 
 |-  ( ph -> ( 1 / A ) e. CC )
87 86 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( 1 / A ) e. CC )
88 87 12 expcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( 1 / A ) ^ k ) e. CC )
89 1 80 12 88 fvmptd3 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) = ( ( 1 / A ) ^ k ) )
90 3 85 rereccld 
 |-  ( ph -> ( 1 / A ) e. RR )
91 3 84 recgt0d 
 |-  ( ph -> 0 < ( 1 / A ) )
92 18 19 90 22 91 lttrd 
 |-  ( ph -> -u 1 < ( 1 / A ) )
93 ltdiv23 
 |-  ( ( 1 e. RR /\ ( A e. RR /\ 0 < A ) /\ ( 1 e. RR /\ 0 < 1 ) ) -> ( ( 1 / A ) < 1 <-> ( 1 / 1 ) < A ) )
94 17 3 84 17 83 93 syl122anc 
 |-  ( ph -> ( ( 1 / A ) < 1 <-> ( 1 / 1 ) < A ) )
95 1cnd 
 |-  ( ph -> 1 e. CC )
96 95 div1d 
 |-  ( ph -> ( 1 / 1 ) = 1 )
97 96 breq1d 
 |-  ( ph -> ( ( 1 / 1 ) < A <-> 1 < A ) )
98 94 97 bitrd 
 |-  ( ph -> ( ( 1 / A ) < 1 <-> 1 < A ) )
99 4 98 mpbird 
 |-  ( ph -> ( 1 / A ) < 1 )
100 90 17 absltd 
 |-  ( ph -> ( ( abs ` ( 1 / A ) ) < 1 <-> ( -u 1 < ( 1 / A ) /\ ( 1 / A ) < 1 ) ) )
101 92 99 100 mpbir2and 
 |-  ( ph -> ( abs ` ( 1 / A ) ) < 1 )
102 86 101 expcnv 
 |-  ( ph -> ( i e. NN0 |-> ( ( 1 / A ) ^ i ) ) ~~> 0 )
103 1 102 eqbrtrid 
 |-  ( ph -> F ~~> 0 )
104 8 9 7 89 103 climi2 
 |-  ( ph -> E. n e. NN A. k e. ( ZZ>= ` n ) ( abs ` ( ( ( 1 / A ) ^ k ) - 0 ) ) < E )
105 simpll 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ZZ>= ` n ) ) -> ph )
106 uznnssnn 
 |-  ( n e. NN -> ( ZZ>= ` n ) C_ NN )
107 106 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ZZ>= ` n ) ) -> ( ZZ>= ` n ) C_ NN )
108 simpr 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ZZ>= ` n ) ) -> k e. ( ZZ>= ` n ) )
109 107 108 sseldd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ZZ>= ` n ) ) -> k e. NN )
110 88 subid1d 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( 1 / A ) ^ k ) - 0 ) = ( ( 1 / A ) ^ k ) )
111 110 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( abs ` ( ( ( 1 / A ) ^ k ) - 0 ) ) = ( abs ` ( ( 1 / A ) ^ k ) ) )
112 90 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( 1 / A ) e. RR )
113 112 12 reexpcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( 1 / A ) ^ k ) e. RR )
114 19 90 91 ltled 
 |-  ( ph -> 0 <_ ( 1 / A ) )
115 114 adantr 
 |-  ( ( ph /\ k e. NN ) -> 0 <_ ( 1 / A ) )
116 112 12 115 expge0d 
 |-  ( ( ph /\ k e. NN ) -> 0 <_ ( ( 1 / A ) ^ k ) )
117 113 116 absidd 
 |-  ( ( ph /\ k e. NN ) -> ( abs ` ( ( 1 / A ) ^ k ) ) = ( ( 1 / A ) ^ k ) )
118 111 117 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( abs ` ( ( ( 1 / A ) ^ k ) - 0 ) ) = ( ( 1 / A ) ^ k ) )
119 118 breq1d 
 |-  ( ( ph /\ k e. NN ) -> ( ( abs ` ( ( ( 1 / A ) ^ k ) - 0 ) ) < E <-> ( ( 1 / A ) ^ k ) < E ) )
120 119 biimpd 
 |-  ( ( ph /\ k e. NN ) -> ( ( abs ` ( ( ( 1 / A ) ^ k ) - 0 ) ) < E -> ( ( 1 / A ) ^ k ) < E ) )
121 105 109 120 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ZZ>= ` n ) ) -> ( ( abs ` ( ( ( 1 / A ) ^ k ) - 0 ) ) < E -> ( ( 1 / A ) ^ k ) < E ) )
122 121 ralimdva 
 |-  ( ( ph /\ n e. NN ) -> ( A. k e. ( ZZ>= ` n ) ( abs ` ( ( ( 1 / A ) ^ k ) - 0 ) ) < E -> A. k e. ( ZZ>= ` n ) ( ( 1 / A ) ^ k ) < E ) )
123 122 reximdva 
 |-  ( ph -> ( E. n e. NN A. k e. ( ZZ>= ` n ) ( abs ` ( ( ( 1 / A ) ^ k ) - 0 ) ) < E -> E. n e. NN A. k e. ( ZZ>= ` n ) ( ( 1 / A ) ^ k ) < E ) )
124 104 123 mpd 
 |-  ( ph -> E. n e. NN A. k e. ( ZZ>= ` n ) ( ( 1 / A ) ^ k ) < E )
125 8 rexanuz2 
 |-  ( E. n e. NN A. k e. ( ZZ>= ` n ) ( ( 1 - E ) < ( 1 - ( B ^ k ) ) /\ ( ( 1 / A ) ^ k ) < E ) <-> ( E. n e. NN A. k e. ( ZZ>= ` n ) ( 1 - E ) < ( 1 - ( B ^ k ) ) /\ E. n e. NN A. k e. ( ZZ>= ` n ) ( ( 1 / A ) ^ k ) < E ) )
126 79 124 125 sylanbrc 
 |-  ( ph -> E. n e. NN A. k e. ( ZZ>= ` n ) ( ( 1 - E ) < ( 1 - ( B ^ k ) ) /\ ( ( 1 / A ) ^ k ) < E ) )
127 simpr 
 |-  ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( 1 - E ) < ( 1 - ( B ^ k ) ) /\ ( ( 1 / A ) ^ k ) < E ) ) -> A. k e. ( ZZ>= ` n ) ( ( 1 - E ) < ( 1 - ( B ^ k ) ) /\ ( ( 1 / A ) ^ k ) < E ) )
128 nnz 
 |-  ( n e. NN -> n e. ZZ )
129 uzid 
 |-  ( n e. ZZ -> n e. ( ZZ>= ` n ) )
130 128 129 syl 
 |-  ( n e. NN -> n e. ( ZZ>= ` n ) )
131 130 ad2antlr 
 |-  ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( 1 - E ) < ( 1 - ( B ^ k ) ) /\ ( ( 1 / A ) ^ k ) < E ) ) -> n e. ( ZZ>= ` n ) )
132 oveq2 
 |-  ( k = n -> ( B ^ k ) = ( B ^ n ) )
133 132 oveq2d 
 |-  ( k = n -> ( 1 - ( B ^ k ) ) = ( 1 - ( B ^ n ) ) )
134 133 breq2d 
 |-  ( k = n -> ( ( 1 - E ) < ( 1 - ( B ^ k ) ) <-> ( 1 - E ) < ( 1 - ( B ^ n ) ) ) )
135 oveq2 
 |-  ( k = n -> ( ( 1 / A ) ^ k ) = ( ( 1 / A ) ^ n ) )
136 135 breq1d 
 |-  ( k = n -> ( ( ( 1 / A ) ^ k ) < E <-> ( ( 1 / A ) ^ n ) < E ) )
137 134 136 anbi12d 
 |-  ( k = n -> ( ( ( 1 - E ) < ( 1 - ( B ^ k ) ) /\ ( ( 1 / A ) ^ k ) < E ) <-> ( ( 1 - E ) < ( 1 - ( B ^ n ) ) /\ ( ( 1 / A ) ^ n ) < E ) ) )
138 137 rspccva 
 |-  ( ( A. k e. ( ZZ>= ` n ) ( ( 1 - E ) < ( 1 - ( B ^ k ) ) /\ ( ( 1 / A ) ^ k ) < E ) /\ n e. ( ZZ>= ` n ) ) -> ( ( 1 - E ) < ( 1 - ( B ^ n ) ) /\ ( ( 1 / A ) ^ n ) < E ) )
139 127 131 138 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( 1 - E ) < ( 1 - ( B ^ k ) ) /\ ( ( 1 / A ) ^ k ) < E ) ) -> ( ( 1 - E ) < ( 1 - ( B ^ n ) ) /\ ( ( 1 / A ) ^ n ) < E ) )
140 1cnd 
 |-  ( ( ph /\ n e. NN ) -> 1 e. CC )
141 81 85 jca 
 |-  ( ph -> ( A e. CC /\ A =/= 0 ) )
142 141 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( A e. CC /\ A =/= 0 ) )
143 43 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. NN0 )
144 expdiv 
 |-  ( ( 1 e. CC /\ ( A e. CC /\ A =/= 0 ) /\ n e. NN0 ) -> ( ( 1 / A ) ^ n ) = ( ( 1 ^ n ) / ( A ^ n ) ) )
145 140 142 143 144 syl3anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1 / A ) ^ n ) = ( ( 1 ^ n ) / ( A ^ n ) ) )
146 128 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. ZZ )
147 1exp 
 |-  ( n e. ZZ -> ( 1 ^ n ) = 1 )
148 146 147 syl 
 |-  ( ( ph /\ n e. NN ) -> ( 1 ^ n ) = 1 )
149 148 oveq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1 ^ n ) / ( A ^ n ) ) = ( 1 / ( A ^ n ) ) )
150 145 149 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1 / A ) ^ n ) = ( 1 / ( A ^ n ) ) )
151 150 breq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( 1 / A ) ^ n ) < E <-> ( 1 / ( A ^ n ) ) < E ) )
152 151 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( 1 - E ) < ( 1 - ( B ^ k ) ) /\ ( ( 1 / A ) ^ k ) < E ) ) -> ( ( ( 1 / A ) ^ n ) < E <-> ( 1 / ( A ^ n ) ) < E ) )
153 152 anbi2d 
 |-  ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( 1 - E ) < ( 1 - ( B ^ k ) ) /\ ( ( 1 / A ) ^ k ) < E ) ) -> ( ( ( 1 - E ) < ( 1 - ( B ^ n ) ) /\ ( ( 1 / A ) ^ n ) < E ) <-> ( ( 1 - E ) < ( 1 - ( B ^ n ) ) /\ ( 1 / ( A ^ n ) ) < E ) ) )
154 139 153 mpbid 
 |-  ( ( ( ph /\ n e. NN ) /\ A. k e. ( ZZ>= ` n ) ( ( 1 - E ) < ( 1 - ( B ^ k ) ) /\ ( ( 1 / A ) ^ k ) < E ) ) -> ( ( 1 - E ) < ( 1 - ( B ^ n ) ) /\ ( 1 / ( A ^ n ) ) < E ) )
155 154 ex 
 |-  ( ( ph /\ n e. NN ) -> ( A. k e. ( ZZ>= ` n ) ( ( 1 - E ) < ( 1 - ( B ^ k ) ) /\ ( ( 1 / A ) ^ k ) < E ) -> ( ( 1 - E ) < ( 1 - ( B ^ n ) ) /\ ( 1 / ( A ^ n ) ) < E ) ) )
156 155 reximdva 
 |-  ( ph -> ( E. n e. NN A. k e. ( ZZ>= ` n ) ( ( 1 - E ) < ( 1 - ( B ^ k ) ) /\ ( ( 1 / A ) ^ k ) < E ) -> E. n e. NN ( ( 1 - E ) < ( 1 - ( B ^ n ) ) /\ ( 1 / ( A ^ n ) ) < E ) ) )
157 126 156 mpd 
 |-  ( ph -> E. n e. NN ( ( 1 - E ) < ( 1 - ( B ^ n ) ) /\ ( 1 / ( A ^ n ) ) < E ) )