| Step | Hyp | Ref
| Expression |
| 1 | | climuz.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 2 | | climuz.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 3 | | climuz.f |
. . 3
⊢ (𝜑 → 𝐹:𝑍⟶ℂ) |
| 4 | 1, 2, 3 | climuzlem 45758 |
. 2
⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦))) |
| 5 | | breq2 5147 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ((abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦 ↔ (abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥)) |
| 6 | 5 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦 ↔ ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥)) |
| 7 | 6 | rexbidv 3179 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦 ↔ ∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥)) |
| 8 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (ℤ≥‘𝑖) =
(ℤ≥‘𝑗)) |
| 9 | 8 | raleqdv 3326 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → (∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 ↔ ∀𝑙 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥)) |
| 10 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘abs |
| 11 | | climuz.k |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘𝐹 |
| 12 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘𝑙 |
| 13 | 11, 12 | nffv 6916 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝐹‘𝑙) |
| 14 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘
− |
| 15 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘𝐴 |
| 16 | 13, 14, 15 | nfov 7461 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘((𝐹‘𝑙) − 𝐴) |
| 17 | 10, 16 | nffv 6916 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(abs‘((𝐹‘𝑙) − 𝐴)) |
| 18 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘
< |
| 19 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘𝑥 |
| 20 | 17, 18, 19 | nfbr 5190 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 |
| 21 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑙(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥 |
| 22 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑘 → (𝐹‘𝑙) = (𝐹‘𝑘)) |
| 23 | 22 | fvoveq1d 7453 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑘 → (abs‘((𝐹‘𝑙) − 𝐴)) = (abs‘((𝐹‘𝑘) − 𝐴))) |
| 24 | 23 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → ((abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 ↔ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)) |
| 25 | 20, 21, 24 | cbvralw 3306 |
. . . . . . . . . 10
⊢
(∀𝑙 ∈
(ℤ≥‘𝑗)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥) |
| 26 | 25 | a1i 11 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → (∀𝑙 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)) |
| 27 | 9, 26 | bitrd 279 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)) |
| 28 | 27 | cbvrexvw 3238 |
. . . . . . 7
⊢
(∃𝑖 ∈
𝑍 ∀𝑙 ∈
(ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥) |
| 29 | 28 | a1i 11 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)) |
| 30 | 7, 29 | bitrd 279 |
. . . . 5
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)) |
| 31 | 30 | cbvralvw 3237 |
. . . 4
⊢
(∀𝑦 ∈
ℝ+ ∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥) |
| 32 | 31 | anbi2i 623 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
∀𝑦 ∈
ℝ+ ∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦) ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)) |
| 33 | 32 | a1i 11 |
. 2
⊢ (𝜑 → ((𝐴 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦) ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥))) |
| 34 | 4, 33 | bitrd 279 |
1
⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥))) |