Step | Hyp | Ref
| Expression |
1 | | nnuz 12620 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 12351 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | stoweidlem7.7 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
4 | | stoweidlem7.2 |
. . . . . 6
⊢ 𝐺 = (𝑖 ∈ ℕ0 ↦ (𝐵↑𝑖)) |
5 | | oveq2 7279 |
. . . . . 6
⊢ (𝑖 = 𝑘 → (𝐵↑𝑖) = (𝐵↑𝑘)) |
6 | | nnnn0 12240 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
7 | 6 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ0) |
8 | | stoweidlem7.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
9 | 8 | rpcnd 12773 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
10 | 9 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℂ) |
11 | 10, 7 | expcld 13862 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐵↑𝑘) ∈ ℂ) |
12 | 4, 5, 7, 11 | fvmptd3 6895 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) = (𝐵↑𝑘)) |
13 | | 1red 10977 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
14 | 13 | renegcld 11402 |
. . . . . . . . 9
⊢ (𝜑 → -1 ∈
ℝ) |
15 | | 0red 10979 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
16 | 8 | rpred 12771 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℝ) |
17 | | neg1lt0 12090 |
. . . . . . . . . 10
⊢ -1 <
0 |
18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → -1 <
0) |
19 | 8 | rpgt0d 12774 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 𝐵) |
20 | 14, 15, 16, 18, 19 | lttrd 11136 |
. . . . . . . 8
⊢ (𝜑 → -1 < 𝐵) |
21 | | stoweidlem7.6 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 < 1) |
22 | 16, 13 | absltd 15139 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘𝐵) < 1 ↔ (-1 < 𝐵 ∧ 𝐵 < 1))) |
23 | 20, 21, 22 | mpbir2and 710 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝐵) < 1) |
24 | 9, 23 | expcnv 15574 |
. . . . . 6
⊢ (𝜑 → (𝑖 ∈ ℕ0 ↦ (𝐵↑𝑖)) ⇝ 0) |
25 | 4, 24 | eqbrtrid 5114 |
. . . . 5
⊢ (𝜑 → 𝐺 ⇝ 0) |
26 | 1, 2, 3, 12, 25 | climi 15217 |
. . . 4
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) |
27 | | r19.26 3097 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸) ↔ (∀𝑘 ∈ (ℤ≥‘𝑛)(𝐵↑𝑘) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘((𝐵↑𝑘) − 0)) < 𝐸)) |
28 | 27 | simprbi 497 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸) → ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((𝐵↑𝑘) − 0)) < 𝐸) |
29 | 28 | ad2antlr 724 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → ∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘((𝐵↑𝑘) − 0)) < 𝐸) |
30 | | oveq2 7279 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑖 → (𝐵↑𝑘) = (𝐵↑𝑖)) |
31 | 30 | oveq1d 7286 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑖 → ((𝐵↑𝑘) − 0) = ((𝐵↑𝑖) − 0)) |
32 | 31 | fveq2d 6775 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑖 → (abs‘((𝐵↑𝑘) − 0)) = (abs‘((𝐵↑𝑖) − 0))) |
33 | 32 | breq1d 5089 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → ((abs‘((𝐵↑𝑘) − 0)) < 𝐸 ↔ (abs‘((𝐵↑𝑖) − 0)) < 𝐸)) |
34 | 33 | rspccva 3560 |
. . . . . . . . . . . 12
⊢
((∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘((𝐵↑𝑘) − 0)) < 𝐸 ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (abs‘((𝐵↑𝑖) − 0)) < 𝐸) |
35 | 29, 34 | sylancom 588 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (abs‘((𝐵↑𝑖) − 0)) < 𝐸) |
36 | | simplll 772 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝜑) |
37 | 36, 8 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝐵 ∈
ℝ+) |
38 | 37 | rpred 12771 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝐵 ∈ ℝ) |
39 | | simpllr 773 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝑛 ∈ ℕ) |
40 | | nnnn0 12240 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝑛 ∈ ℕ0) |
42 | | eluznn0 12656 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ0
∧ 𝑖 ∈
(ℤ≥‘𝑛)) → 𝑖 ∈ ℕ0) |
43 | 41, 42 | sylancom 588 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝑖 ∈ ℕ0) |
44 | 38, 43 | reexpcld 13879 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (𝐵↑𝑖) ∈ ℝ) |
45 | | rpre 12737 |
. . . . . . . . . . . . 13
⊢ (𝐸 ∈ ℝ+
→ 𝐸 ∈
ℝ) |
46 | 36, 3, 45 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝐸 ∈ ℝ) |
47 | | recn 10962 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵↑𝑖) ∈ ℝ → (𝐵↑𝑖) ∈ ℂ) |
48 | 47 | subid1d 11321 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵↑𝑖) ∈ ℝ → ((𝐵↑𝑖) − 0) = (𝐵↑𝑖)) |
49 | 48 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵↑𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((𝐵↑𝑖) − 0) = (𝐵↑𝑖)) |
50 | 49 | fveq2d 6775 |
. . . . . . . . . . . . . 14
⊢ (((𝐵↑𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → (abs‘((𝐵↑𝑖) − 0)) = (abs‘(𝐵↑𝑖))) |
51 | 50 | breq1d 5089 |
. . . . . . . . . . . . 13
⊢ (((𝐵↑𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((abs‘((𝐵↑𝑖) − 0)) < 𝐸 ↔ (abs‘(𝐵↑𝑖)) < 𝐸)) |
52 | | abslt 15024 |
. . . . . . . . . . . . 13
⊢ (((𝐵↑𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((abs‘(𝐵↑𝑖)) < 𝐸 ↔ (-𝐸 < (𝐵↑𝑖) ∧ (𝐵↑𝑖) < 𝐸))) |
53 | 51, 52 | bitrd 278 |
. . . . . . . . . . . 12
⊢ (((𝐵↑𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((abs‘((𝐵↑𝑖) − 0)) < 𝐸 ↔ (-𝐸 < (𝐵↑𝑖) ∧ (𝐵↑𝑖) < 𝐸))) |
54 | 44, 46, 53 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → ((abs‘((𝐵↑𝑖) − 0)) < 𝐸 ↔ (-𝐸 < (𝐵↑𝑖) ∧ (𝐵↑𝑖) < 𝐸))) |
55 | 35, 54 | mpbid 231 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (-𝐸 < (𝐵↑𝑖) ∧ (𝐵↑𝑖) < 𝐸)) |
56 | 55 | simprd 496 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (𝐵↑𝑖) < 𝐸) |
57 | | eluznn 12657 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈
(ℤ≥‘𝑛)) → 𝑖 ∈ ℕ) |
58 | 39, 57 | sylancom 588 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝑖 ∈ ℕ) |
59 | 16 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐵 ∈ ℝ) |
60 | | nnnn0 12240 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ → 𝑖 ∈
ℕ0) |
61 | 60 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ0) |
62 | 59, 61 | reexpcld 13879 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐵↑𝑖) ∈ ℝ) |
63 | 3 | rpred 12771 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℝ) |
64 | 63 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐸 ∈ ℝ) |
65 | | 1red 10977 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 1 ∈
ℝ) |
66 | 62, 64, 65 | ltsub2d 11585 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐵↑𝑖) < 𝐸 ↔ (1 − 𝐸) < (1 − (𝐵↑𝑖)))) |
67 | 36, 58, 66 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → ((𝐵↑𝑖) < 𝐸 ↔ (1 − 𝐸) < (1 − (𝐵↑𝑖)))) |
68 | 56, 67 | mpbid 231 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (1 − 𝐸) < (1 − (𝐵↑𝑖))) |
69 | 68 | ralrimiva 3110 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) → ∀𝑖 ∈ (ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑖))) |
70 | 30 | oveq2d 7287 |
. . . . . . . . 9
⊢ (𝑘 = 𝑖 → (1 − (𝐵↑𝑘)) = (1 − (𝐵↑𝑖))) |
71 | 70 | breq2d 5091 |
. . . . . . . 8
⊢ (𝑘 = 𝑖 → ((1 − 𝐸) < (1 − (𝐵↑𝑘)) ↔ (1 − 𝐸) < (1 − (𝐵↑𝑖)))) |
72 | 71 | cbvralvw 3381 |
. . . . . . 7
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑘)) ↔ ∀𝑖 ∈ (ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑖))) |
73 | 69, 72 | sylibr 233 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) → ∀𝑘 ∈ (ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑘))) |
74 | 73 | ex 413 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸) → ∀𝑘 ∈ (ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑘)))) |
75 | 74 | reximdva 3205 |
. . . 4
⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑘)))) |
76 | 26, 75 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑘))) |
77 | | stoweidlem7.1 |
. . . . . 6
⊢ 𝐹 = (𝑖 ∈ ℕ0 ↦ ((1 /
𝐴)↑𝑖)) |
78 | | oveq2 7279 |
. . . . . 6
⊢ (𝑖 = 𝑘 → ((1 / 𝐴)↑𝑖) = ((1 / 𝐴)↑𝑘)) |
79 | | stoweidlem7.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
80 | 79 | recnd 11004 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
81 | | 0lt1 11497 |
. . . . . . . . . . . 12
⊢ 0 <
1 |
82 | 81 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 1) |
83 | | stoweidlem7.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 < 𝐴) |
84 | 15, 13, 79, 82, 83 | lttrd 11136 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 𝐴) |
85 | 84 | gt0ne0d 11539 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≠ 0) |
86 | 80, 85 | reccld 11744 |
. . . . . . . 8
⊢ (𝜑 → (1 / 𝐴) ∈ ℂ) |
87 | 86 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝐴) ∈
ℂ) |
88 | 87, 7 | expcld 13862 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1 / 𝐴)↑𝑘) ∈ ℂ) |
89 | 77, 78, 7, 88 | fvmptd3 6895 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = ((1 / 𝐴)↑𝑘)) |
90 | 79, 85 | rereccld 11802 |
. . . . . . . . 9
⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) |
91 | 79, 84 | recgt0d 11909 |
. . . . . . . . 9
⊢ (𝜑 → 0 < (1 / 𝐴)) |
92 | 14, 15, 90, 18, 91 | lttrd 11136 |
. . . . . . . 8
⊢ (𝜑 → -1 < (1 / 𝐴)) |
93 | | ltdiv23 11866 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ (𝐴
∈ ℝ ∧ 0 < 𝐴) ∧ (1 ∈ ℝ ∧ 0 < 1))
→ ((1 / 𝐴) < 1
↔ (1 / 1) < 𝐴)) |
94 | 13, 79, 84, 13, 82, 93 | syl122anc 1378 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 / 𝐴) < 1 ↔ (1 / 1) < 𝐴)) |
95 | | 1cnd 10971 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
96 | 95 | div1d 11743 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / 1) =
1) |
97 | 96 | breq1d 5089 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 / 1) < 𝐴 ↔ 1 < 𝐴)) |
98 | 94, 97 | bitrd 278 |
. . . . . . . . 9
⊢ (𝜑 → ((1 / 𝐴) < 1 ↔ 1 < 𝐴)) |
99 | 83, 98 | mpbird 256 |
. . . . . . . 8
⊢ (𝜑 → (1 / 𝐴) < 1) |
100 | 90, 13 | absltd 15139 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘(1 / 𝐴)) < 1 ↔ (-1 < (1 /
𝐴) ∧ (1 / 𝐴) < 1))) |
101 | 92, 99, 100 | mpbir2and 710 |
. . . . . . 7
⊢ (𝜑 → (abs‘(1 / 𝐴)) < 1) |
102 | 86, 101 | expcnv 15574 |
. . . . . 6
⊢ (𝜑 → (𝑖 ∈ ℕ0 ↦ ((1 /
𝐴)↑𝑖)) ⇝ 0) |
103 | 77, 102 | eqbrtrid 5114 |
. . . . 5
⊢ (𝜑 → 𝐹 ⇝ 0) |
104 | 1, 2, 3, 89, 103 | climi2 15218 |
. . . 4
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(((1 / 𝐴)↑𝑘) − 0)) < 𝐸) |
105 | | simpll 764 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝜑) |
106 | | uznnssnn 12634 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(ℤ≥‘𝑛) ⊆ ℕ) |
107 | 106 | ad2antlr 724 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) →
(ℤ≥‘𝑛) ⊆ ℕ) |
108 | | simpr 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ (ℤ≥‘𝑛)) |
109 | 107, 108 | sseldd 3927 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
110 | 88 | subid1d 11321 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((1 / 𝐴)↑𝑘) − 0) = ((1 / 𝐴)↑𝑘)) |
111 | 110 | fveq2d 6775 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(((1 /
𝐴)↑𝑘) − 0)) = (abs‘((1 / 𝐴)↑𝑘))) |
112 | 90 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝐴) ∈
ℝ) |
113 | 112, 7 | reexpcld 13879 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1 / 𝐴)↑𝑘) ∈ ℝ) |
114 | 15, 90, 91 | ltled 11123 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ (1 / 𝐴)) |
115 | 114 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (1 / 𝐴)) |
116 | 112, 7, 115 | expge0d 13880 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ ((1 / 𝐴)↑𝑘)) |
117 | 113, 116 | absidd 15132 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘((1 /
𝐴)↑𝑘)) = ((1 / 𝐴)↑𝑘)) |
118 | 111, 117 | eqtrd 2780 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(((1 /
𝐴)↑𝑘) − 0)) = ((1 / 𝐴)↑𝑘)) |
119 | 118 | breq1d 5089 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((abs‘(((1 /
𝐴)↑𝑘) − 0)) < 𝐸 ↔ ((1 / 𝐴)↑𝑘) < 𝐸)) |
120 | 119 | biimpd 228 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((abs‘(((1 /
𝐴)↑𝑘) − 0)) < 𝐸 → ((1 / 𝐴)↑𝑘) < 𝐸)) |
121 | 105, 109,
120 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((abs‘(((1 /
𝐴)↑𝑘) − 0)) < 𝐸 → ((1 / 𝐴)↑𝑘) < 𝐸)) |
122 | 121 | ralimdva 3105 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘(((1 / 𝐴)↑𝑘) − 0)) < 𝐸 → ∀𝑘 ∈ (ℤ≥‘𝑛)((1 / 𝐴)↑𝑘) < 𝐸)) |
123 | 122 | reximdva 3205 |
. . . 4
⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(((1 / 𝐴)↑𝑘) − 0)) < 𝐸 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1 / 𝐴)↑𝑘) < 𝐸)) |
124 | 104, 123 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1 / 𝐴)↑𝑘) < 𝐸) |
125 | 1 | rexanuz2 15059 |
. . 3
⊢
(∃𝑛 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) ↔ (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1 / 𝐴)↑𝑘) < 𝐸)) |
126 | 76, 124, 125 | sylanbrc 583 |
. 2
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) |
127 | | simpr 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → ∀𝑘 ∈ (ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) |
128 | | nnz 12342 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
129 | | uzid 12596 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
(ℤ≥‘𝑛)) |
130 | 128, 129 | syl 17 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
(ℤ≥‘𝑛)) |
131 | 130 | ad2antlr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → 𝑛 ∈ (ℤ≥‘𝑛)) |
132 | | oveq2 7279 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (𝐵↑𝑘) = (𝐵↑𝑛)) |
133 | 132 | oveq2d 7287 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (1 − (𝐵↑𝑘)) = (1 − (𝐵↑𝑛))) |
134 | 133 | breq2d 5091 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((1 − 𝐸) < (1 − (𝐵↑𝑘)) ↔ (1 − 𝐸) < (1 − (𝐵↑𝑛)))) |
135 | | oveq2 7279 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → ((1 / 𝐴)↑𝑘) = ((1 / 𝐴)↑𝑛)) |
136 | 135 | breq1d 5089 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (((1 / 𝐴)↑𝑘) < 𝐸 ↔ ((1 / 𝐴)↑𝑛) < 𝐸)) |
137 | 134, 136 | anbi12d 631 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) ↔ ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ ((1 / 𝐴)↑𝑛) < 𝐸))) |
138 | 137 | rspccva 3560 |
. . . . . 6
⊢
((∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) ∧ 𝑛 ∈ (ℤ≥‘𝑛)) → ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ ((1 / 𝐴)↑𝑛) < 𝐸)) |
139 | 127, 131,
138 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ ((1 / 𝐴)↑𝑛) < 𝐸)) |
140 | | 1cnd 10971 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 1 ∈
ℂ) |
141 | 80, 85 | jca 512 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) |
142 | 141 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) |
143 | 40 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) |
144 | | expdiv 13832 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ (𝐴
∈ ℂ ∧ 𝐴 ≠
0) ∧ 𝑛 ∈
ℕ0) → ((1 / 𝐴)↑𝑛) = ((1↑𝑛) / (𝐴↑𝑛))) |
145 | 140, 142,
143, 144 | syl3anc 1370 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1 / 𝐴)↑𝑛) = ((1↑𝑛) / (𝐴↑𝑛))) |
146 | 128 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ) |
147 | | 1exp 13810 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ →
(1↑𝑛) =
1) |
148 | 146, 147 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1↑𝑛) = 1) |
149 | 148 | oveq1d 7286 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1↑𝑛) / (𝐴↑𝑛)) = (1 / (𝐴↑𝑛))) |
150 | 145, 149 | eqtrd 2780 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1 / 𝐴)↑𝑛) = (1 / (𝐴↑𝑛))) |
151 | 150 | breq1d 5089 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((1 / 𝐴)↑𝑛) < 𝐸 ↔ (1 / (𝐴↑𝑛)) < 𝐸)) |
152 | 151 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → (((1 / 𝐴)↑𝑛) < 𝐸 ↔ (1 / (𝐴↑𝑛)) < 𝐸)) |
153 | 152 | anbi2d 629 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → (((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ ((1 / 𝐴)↑𝑛) < 𝐸) ↔ ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ (1 / (𝐴↑𝑛)) < 𝐸))) |
154 | 139, 153 | mpbid 231 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ (1 / (𝐴↑𝑛)) < 𝐸)) |
155 | 154 | ex 413 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) → ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ (1 / (𝐴↑𝑛)) < 𝐸))) |
156 | 155 | reximdva 3205 |
. 2
⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) → ∃𝑛 ∈ ℕ ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ (1 / (𝐴↑𝑛)) < 𝐸))) |
157 | 126, 156 | mpd 15 |
1
⊢ (𝜑 → ∃𝑛 ∈ ℕ ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ (1 / (𝐴↑𝑛)) < 𝐸)) |