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 𝐹 = ( 𝑖 ∈ ℕ0 ↦ ( ( 1 / 𝐴 ) ↑ 𝑖 ) )
stoweidlem7.2 𝐺 = ( 𝑖 ∈ ℕ0 ↦ ( 𝐵𝑖 ) )
stoweidlem7.3 ( 𝜑𝐴 ∈ ℝ )
stoweidlem7.4 ( 𝜑 → 1 < 𝐴 )
stoweidlem7.5 ( 𝜑𝐵 ∈ ℝ+ )
stoweidlem7.6 ( 𝜑𝐵 < 1 )
stoweidlem7.7 ( 𝜑𝐸 ∈ ℝ+ )
Assertion stoweidlem7 ( 𝜑 → ∃ 𝑛 ∈ ℕ ( ( 1 − 𝐸 ) < ( 1 − ( 𝐵𝑛 ) ) ∧ ( 1 / ( 𝐴𝑛 ) ) < 𝐸 ) )

Proof

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