Step | Hyp | Ref
| Expression |
1 | | nnuz 11599 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11285 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | stoweidlem7.7 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
4 | | stoweidlem7.2 |
. . . . . . 7
⊢ 𝐺 = (𝑖 ∈ ℕ0 ↦ (𝐵↑𝑖)) |
5 | 4 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐺 = (𝑖 ∈ ℕ0 ↦ (𝐵↑𝑖))) |
6 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑖 = 𝑘 → (𝐵↑𝑖) = (𝐵↑𝑘)) |
7 | 6 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑖 = 𝑘) → (𝐵↑𝑖) = (𝐵↑𝑘)) |
8 | | nnnn0 11176 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
9 | 8 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ0) |
10 | | stoweidlem7.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
11 | 10 | rpcnd 11750 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
12 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℂ) |
13 | 12, 9 | expcld 12870 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐵↑𝑘) ∈ ℂ) |
14 | 5, 7, 9, 13 | fvmptd 6197 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) = (𝐵↑𝑘)) |
15 | | 1red 9934 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
16 | 15 | renegcld 10336 |
. . . . . . . . 9
⊢ (𝜑 → -1 ∈
ℝ) |
17 | | 0red 9920 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
18 | 10 | rpred 11748 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℝ) |
19 | | neg1lt0 11004 |
. . . . . . . . . 10
⊢ -1 <
0 |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → -1 <
0) |
21 | 10 | rpgt0d 11751 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 𝐵) |
22 | 16, 17, 18, 20, 21 | lttrd 10077 |
. . . . . . . 8
⊢ (𝜑 → -1 < 𝐵) |
23 | | stoweidlem7.6 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 < 1) |
24 | 18, 15 | absltd 14016 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘𝐵) < 1 ↔ (-1 < 𝐵 ∧ 𝐵 < 1))) |
25 | 22, 23, 24 | mpbir2and 959 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝐵) < 1) |
26 | 11, 25 | expcnv 14435 |
. . . . . 6
⊢ (𝜑 → (𝑖 ∈ ℕ0 ↦ (𝐵↑𝑖)) ⇝ 0) |
27 | 4, 26 | syl5eqbr 4618 |
. . . . 5
⊢ (𝜑 → 𝐺 ⇝ 0) |
28 | 1, 2, 3, 14, 27 | climi 14089 |
. . . 4
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) |
29 | | r19.26 3046 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸) ↔ (∀𝑘 ∈ (ℤ≥‘𝑛)(𝐵↑𝑘) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘((𝐵↑𝑘) − 0)) < 𝐸)) |
30 | 29 | simprbi 479 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸) → ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((𝐵↑𝑘) − 0)) < 𝐸) |
31 | 30 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → ∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘((𝐵↑𝑘) − 0)) < 𝐸) |
32 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑖 → (𝐵↑𝑘) = (𝐵↑𝑖)) |
33 | 32 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑖 → ((𝐵↑𝑘) − 0) = ((𝐵↑𝑖) − 0)) |
34 | 33 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑖 → (abs‘((𝐵↑𝑘) − 0)) = (abs‘((𝐵↑𝑖) − 0))) |
35 | 34 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → ((abs‘((𝐵↑𝑘) − 0)) < 𝐸 ↔ (abs‘((𝐵↑𝑖) − 0)) < 𝐸)) |
36 | 35 | rspccva 3281 |
. . . . . . . . . . . 12
⊢
((∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘((𝐵↑𝑘) − 0)) < 𝐸 ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (abs‘((𝐵↑𝑖) − 0)) < 𝐸) |
37 | 31, 36 | sylancom 698 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (abs‘((𝐵↑𝑖) − 0)) < 𝐸) |
38 | | simplll 794 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝜑) |
39 | 38, 10 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝐵 ∈
ℝ+) |
40 | 39 | rpred 11748 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝐵 ∈ ℝ) |
41 | | simpllr 795 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝑛 ∈ ℕ) |
42 | | nnnn0 11176 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝑛 ∈ ℕ0) |
44 | | eluznn0 11633 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ0
∧ 𝑖 ∈
(ℤ≥‘𝑛)) → 𝑖 ∈ ℕ0) |
45 | 43, 44 | sylancom 698 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝑖 ∈ ℕ0) |
46 | 40, 45 | reexpcld 12887 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (𝐵↑𝑖) ∈ ℝ) |
47 | | rpre 11715 |
. . . . . . . . . . . . 13
⊢ (𝐸 ∈ ℝ+
→ 𝐸 ∈
ℝ) |
48 | 38, 3, 47 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝐸 ∈ ℝ) |
49 | | recn 9905 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵↑𝑖) ∈ ℝ → (𝐵↑𝑖) ∈ ℂ) |
50 | 49 | subid1d 10260 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵↑𝑖) ∈ ℝ → ((𝐵↑𝑖) − 0) = (𝐵↑𝑖)) |
51 | 50 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵↑𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((𝐵↑𝑖) − 0) = (𝐵↑𝑖)) |
52 | 51 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (((𝐵↑𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → (abs‘((𝐵↑𝑖) − 0)) = (abs‘(𝐵↑𝑖))) |
53 | 52 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (((𝐵↑𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((abs‘((𝐵↑𝑖) − 0)) < 𝐸 ↔ (abs‘(𝐵↑𝑖)) < 𝐸)) |
54 | | abslt 13902 |
. . . . . . . . . . . . 13
⊢ (((𝐵↑𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((abs‘(𝐵↑𝑖)) < 𝐸 ↔ (-𝐸 < (𝐵↑𝑖) ∧ (𝐵↑𝑖) < 𝐸))) |
55 | 53, 54 | bitrd 267 |
. . . . . . . . . . . 12
⊢ (((𝐵↑𝑖) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((abs‘((𝐵↑𝑖) − 0)) < 𝐸 ↔ (-𝐸 < (𝐵↑𝑖) ∧ (𝐵↑𝑖) < 𝐸))) |
56 | 46, 48, 55 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → ((abs‘((𝐵↑𝑖) − 0)) < 𝐸 ↔ (-𝐸 < (𝐵↑𝑖) ∧ (𝐵↑𝑖) < 𝐸))) |
57 | 37, 56 | mpbid 221 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (-𝐸 < (𝐵↑𝑖) ∧ (𝐵↑𝑖) < 𝐸)) |
58 | 57 | simprd 478 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (𝐵↑𝑖) < 𝐸) |
59 | | eluznn 11634 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧ 𝑖 ∈
(ℤ≥‘𝑛)) → 𝑖 ∈ ℕ) |
60 | 41, 59 | sylancom 698 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → 𝑖 ∈ ℕ) |
61 | 18 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐵 ∈ ℝ) |
62 | | nnnn0 11176 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ → 𝑖 ∈
ℕ0) |
63 | 62 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ0) |
64 | 61, 63 | reexpcld 12887 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐵↑𝑖) ∈ ℝ) |
65 | 3 | rpred 11748 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℝ) |
66 | 65 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐸 ∈ ℝ) |
67 | | 1red 9934 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 1 ∈
ℝ) |
68 | 64, 66, 67 | ltsub2d 10516 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐵↑𝑖) < 𝐸 ↔ (1 − 𝐸) < (1 − (𝐵↑𝑖)))) |
69 | 38, 60, 68 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → ((𝐵↑𝑖) < 𝐸 ↔ (1 − 𝐸) < (1 − (𝐵↑𝑖)))) |
70 | 58, 69 | mpbid 221 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) ∧ 𝑖 ∈ (ℤ≥‘𝑛)) → (1 − 𝐸) < (1 − (𝐵↑𝑖))) |
71 | 70 | ralrimiva 2949 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) → ∀𝑖 ∈ (ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑖))) |
72 | 32 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑘 = 𝑖 → (1 − (𝐵↑𝑘)) = (1 − (𝐵↑𝑖))) |
73 | 72 | breq2d 4595 |
. . . . . . . 8
⊢ (𝑘 = 𝑖 → ((1 − 𝐸) < (1 − (𝐵↑𝑘)) ↔ (1 − 𝐸) < (1 − (𝐵↑𝑖)))) |
74 | 73 | cbvralv 3147 |
. . . . . . 7
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑘)) ↔ ∀𝑖 ∈ (ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑖))) |
75 | 71, 74 | sylibr 223 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸)) → ∀𝑘 ∈ (ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑘))) |
76 | 75 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈
(ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸) → ∀𝑘 ∈ (ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑘)))) |
77 | 76 | reximdva 3000 |
. . . 4
⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐵↑𝑘) ∈ ℂ ∧ (abs‘((𝐵↑𝑘) − 0)) < 𝐸) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑘)))) |
78 | 28, 77 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑘))) |
79 | | stoweidlem7.1 |
. . . . . . 7
⊢ 𝐹 = (𝑖 ∈ ℕ0 ↦ ((1 /
𝐴)↑𝑖)) |
80 | 79 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹 = (𝑖 ∈ ℕ0 ↦ ((1 /
𝐴)↑𝑖))) |
81 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑖 = 𝑘 → ((1 / 𝐴)↑𝑖) = ((1 / 𝐴)↑𝑘)) |
82 | 81 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑖 = 𝑘) → ((1 / 𝐴)↑𝑖) = ((1 / 𝐴)↑𝑘)) |
83 | | stoweidlem7.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
84 | 83 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
85 | | 0lt1 10429 |
. . . . . . . . . . . 12
⊢ 0 <
1 |
86 | 85 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 1) |
87 | | stoweidlem7.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 < 𝐴) |
88 | 17, 15, 83, 86, 87 | lttrd 10077 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 𝐴) |
89 | 88 | gt0ne0d 10471 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≠ 0) |
90 | 84, 89 | reccld 10673 |
. . . . . . . 8
⊢ (𝜑 → (1 / 𝐴) ∈ ℂ) |
91 | 90 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝐴) ∈
ℂ) |
92 | 91, 9 | expcld 12870 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1 / 𝐴)↑𝑘) ∈ ℂ) |
93 | 80, 82, 9, 92 | fvmptd 6197 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = ((1 / 𝐴)↑𝑘)) |
94 | 83, 89 | rereccld 10731 |
. . . . . . . . 9
⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) |
95 | 83, 88 | recgt0d 10837 |
. . . . . . . . 9
⊢ (𝜑 → 0 < (1 / 𝐴)) |
96 | 16, 17, 94, 20, 95 | lttrd 10077 |
. . . . . . . 8
⊢ (𝜑 → -1 < (1 / 𝐴)) |
97 | | ltdiv23 10793 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ (𝐴
∈ ℝ ∧ 0 < 𝐴) ∧ (1 ∈ ℝ ∧ 0 < 1))
→ ((1 / 𝐴) < 1
↔ (1 / 1) < 𝐴)) |
98 | 15, 83, 88, 15, 86, 97 | syl122anc 1327 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 / 𝐴) < 1 ↔ (1 / 1) < 𝐴)) |
99 | | 1cnd 9935 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
100 | 99 | div1d 10672 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / 1) =
1) |
101 | 100 | breq1d 4593 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 / 1) < 𝐴 ↔ 1 < 𝐴)) |
102 | 98, 101 | bitrd 267 |
. . . . . . . . 9
⊢ (𝜑 → ((1 / 𝐴) < 1 ↔ 1 < 𝐴)) |
103 | 87, 102 | mpbird 246 |
. . . . . . . 8
⊢ (𝜑 → (1 / 𝐴) < 1) |
104 | 94, 15 | absltd 14016 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘(1 / 𝐴)) < 1 ↔ (-1 < (1 /
𝐴) ∧ (1 / 𝐴) < 1))) |
105 | 96, 103, 104 | mpbir2and 959 |
. . . . . . 7
⊢ (𝜑 → (abs‘(1 / 𝐴)) < 1) |
106 | 90, 105 | expcnv 14435 |
. . . . . 6
⊢ (𝜑 → (𝑖 ∈ ℕ0 ↦ ((1 /
𝐴)↑𝑖)) ⇝ 0) |
107 | 79, 106 | syl5eqbr 4618 |
. . . . 5
⊢ (𝜑 → 𝐹 ⇝ 0) |
108 | 1, 2, 3, 93, 107 | climi2 14090 |
. . . 4
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(((1 / 𝐴)↑𝑘) − 0)) < 𝐸) |
109 | | simpll 786 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝜑) |
110 | | uznnssnn 11611 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(ℤ≥‘𝑛) ⊆ ℕ) |
111 | 110 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) →
(ℤ≥‘𝑛) ⊆ ℕ) |
112 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ (ℤ≥‘𝑛)) |
113 | 111, 112 | sseldd 3569 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
114 | 92 | subid1d 10260 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((1 / 𝐴)↑𝑘) − 0) = ((1 / 𝐴)↑𝑘)) |
115 | 114 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(((1 /
𝐴)↑𝑘) − 0)) = (abs‘((1 / 𝐴)↑𝑘))) |
116 | 94 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1 / 𝐴) ∈
ℝ) |
117 | 116, 9 | reexpcld 12887 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1 / 𝐴)↑𝑘) ∈ ℝ) |
118 | 17, 94, 95 | ltled 10064 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ (1 / 𝐴)) |
119 | 118 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (1 / 𝐴)) |
120 | 116, 9, 119 | expge0d 12888 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ ((1 / 𝐴)↑𝑘)) |
121 | 117, 120 | absidd 14009 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘((1 /
𝐴)↑𝑘)) = ((1 / 𝐴)↑𝑘)) |
122 | 115, 121 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(((1 /
𝐴)↑𝑘) − 0)) = ((1 / 𝐴)↑𝑘)) |
123 | 122 | breq1d 4593 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((abs‘(((1 /
𝐴)↑𝑘) − 0)) < 𝐸 ↔ ((1 / 𝐴)↑𝑘) < 𝐸)) |
124 | 123 | biimpd 218 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((abs‘(((1 /
𝐴)↑𝑘) − 0)) < 𝐸 → ((1 / 𝐴)↑𝑘) < 𝐸)) |
125 | 109, 113,
124 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((abs‘(((1 /
𝐴)↑𝑘) − 0)) < 𝐸 → ((1 / 𝐴)↑𝑘) < 𝐸)) |
126 | 125 | ralimdva 2945 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘(((1 / 𝐴)↑𝑘) − 0)) < 𝐸 → ∀𝑘 ∈ (ℤ≥‘𝑛)((1 / 𝐴)↑𝑘) < 𝐸)) |
127 | 126 | reximdva 3000 |
. . . 4
⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(((1 / 𝐴)↑𝑘) − 0)) < 𝐸 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1 / 𝐴)↑𝑘) < 𝐸)) |
128 | 108, 127 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1 / 𝐴)↑𝑘) < 𝐸) |
129 | 1 | rexanuz2 13937 |
. . 3
⊢
(∃𝑛 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) ↔ (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1 / 𝐴)↑𝑘) < 𝐸)) |
130 | 78, 128, 129 | sylanbrc 695 |
. 2
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) |
131 | | simpr 476 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → ∀𝑘 ∈ (ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) |
132 | | nnz 11276 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
133 | | uzid 11578 |
. . . . . . . 8
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
(ℤ≥‘𝑛)) |
134 | 132, 133 | syl 17 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
(ℤ≥‘𝑛)) |
135 | 134 | ad2antlr 759 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → 𝑛 ∈ (ℤ≥‘𝑛)) |
136 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (𝐵↑𝑘) = (𝐵↑𝑛)) |
137 | 136 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (1 − (𝐵↑𝑘)) = (1 − (𝐵↑𝑛))) |
138 | 137 | breq2d 4595 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((1 − 𝐸) < (1 − (𝐵↑𝑘)) ↔ (1 − 𝐸) < (1 − (𝐵↑𝑛)))) |
139 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → ((1 / 𝐴)↑𝑘) = ((1 / 𝐴)↑𝑛)) |
140 | 139 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (((1 / 𝐴)↑𝑘) < 𝐸 ↔ ((1 / 𝐴)↑𝑛) < 𝐸)) |
141 | 138, 140 | anbi12d 743 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) ↔ ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ ((1 / 𝐴)↑𝑛) < 𝐸))) |
142 | 141 | rspccva 3281 |
. . . . . 6
⊢
((∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) ∧ 𝑛 ∈ (ℤ≥‘𝑛)) → ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ ((1 / 𝐴)↑𝑛) < 𝐸)) |
143 | 131, 135,
142 | syl2anc 691 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ ((1 / 𝐴)↑𝑛) < 𝐸)) |
144 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 1 ∈
ℂ) |
145 | 84, 89 | jca 553 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) |
146 | 145 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) |
147 | 42 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) |
148 | | expdiv 12773 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ (𝐴
∈ ℂ ∧ 𝐴 ≠
0) ∧ 𝑛 ∈
ℕ0) → ((1 / 𝐴)↑𝑛) = ((1↑𝑛) / (𝐴↑𝑛))) |
149 | 144, 146,
147, 148 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1 / 𝐴)↑𝑛) = ((1↑𝑛) / (𝐴↑𝑛))) |
150 | 132 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ) |
151 | | 1exp 12751 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ →
(1↑𝑛) =
1) |
152 | 150, 151 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1↑𝑛) = 1) |
153 | 152 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1↑𝑛) / (𝐴↑𝑛)) = (1 / (𝐴↑𝑛))) |
154 | 149, 153 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1 / 𝐴)↑𝑛) = (1 / (𝐴↑𝑛))) |
155 | 154 | breq1d 4593 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((1 / 𝐴)↑𝑛) < 𝐸 ↔ (1 / (𝐴↑𝑛)) < 𝐸)) |
156 | 155 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → (((1 / 𝐴)↑𝑛) < 𝐸 ↔ (1 / (𝐴↑𝑛)) < 𝐸)) |
157 | 156 | anbi2d 736 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → (((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ ((1 / 𝐴)↑𝑛) < 𝐸) ↔ ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ (1 / (𝐴↑𝑛)) < 𝐸))) |
158 | 143, 157 | mpbid 221 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸)) → ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ (1 / (𝐴↑𝑛)) < 𝐸)) |
159 | 158 | ex 449 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈
(ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) → ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ (1 / (𝐴↑𝑛)) < 𝐸))) |
160 | 159 | reximdva 3000 |
. 2
⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1 − 𝐸) < (1 − (𝐵↑𝑘)) ∧ ((1 / 𝐴)↑𝑘) < 𝐸) → ∃𝑛 ∈ ℕ ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ (1 / (𝐴↑𝑛)) < 𝐸))) |
161 | 130, 160 | mpd 15 |
1
⊢ (𝜑 → ∃𝑛 ∈ ℕ ((1 − 𝐸) < (1 − (𝐵↑𝑛)) ∧ (1 / (𝐴↑𝑛)) < 𝐸)) |