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 / ( 𝐴 ↑ 𝑛 ) ) < 𝐸 ) )