Step | Hyp | Ref
| Expression |
1 | | climuz.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
2 | | climuz.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
3 | | climuz.f |
. . 3
⊢ (𝜑 → 𝐹:𝑍⟶ℂ) |
4 | 1, 2, 3 | climuzlem 39975 |
. 2
⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦))) |
5 | | breq2 4657 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ((abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦 ↔ (abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥)) |
6 | 5 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦 ↔ ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥)) |
7 | 6 | rexbidv 3052 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦 ↔ ∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥)) |
8 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (ℤ≥‘𝑖) =
(ℤ≥‘𝑗)) |
9 | 8 | raleqdv 3144 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → (∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 ↔ ∀𝑙 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥)) |
10 | | nfcv 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘abs |
11 | | climuz.k |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘𝐹 |
12 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘𝑙 |
13 | 11, 12 | nffv 6198 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝐹‘𝑙) |
14 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘
− |
15 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘𝐴 |
16 | 13, 14, 15 | nfov 6676 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘((𝐹‘𝑙) − 𝐴) |
17 | 10, 16 | nffv 6198 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(abs‘((𝐹‘𝑙) − 𝐴)) |
18 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘
< |
19 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘𝑥 |
20 | 17, 18, 19 | nfbr 4699 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 |
21 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑙(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥 |
22 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑘 → (𝐹‘𝑙) = (𝐹‘𝑘)) |
23 | 22 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑘 → ((𝐹‘𝑙) − 𝐴) = ((𝐹‘𝑘) − 𝐴)) |
24 | 23 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑘 → (abs‘((𝐹‘𝑙) − 𝐴)) = (abs‘((𝐹‘𝑘) − 𝐴))) |
25 | 24 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑘 → ((abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 ↔ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)) |
26 | 20, 21, 25 | cbvral 3167 |
. . . . . . . . . 10
⊢
(∀𝑙 ∈
(ℤ≥‘𝑗)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥) |
27 | 26 | a1i 11 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → (∀𝑙 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)) |
28 | 9, 27 | bitrd 268 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)) |
29 | 28 | cbvrexv 3172 |
. . . . . . 7
⊢
(∃𝑖 ∈
𝑍 ∀𝑙 ∈
(ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥) |
30 | 29 | a1i 11 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑥 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)) |
31 | 7, 30 | bitrd 268 |
. . . . 5
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)) |
32 | 31 | cbvralv 3171 |
. . . 4
⊢
(∀𝑦 ∈
ℝ+ ∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥) |
33 | 32 | anbi2i 730 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
∀𝑦 ∈
ℝ+ ∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦) ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥)) |
34 | 33 | a1i 11 |
. 2
⊢ (𝜑 → ((𝐴 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑖 ∈ 𝑍 ∀𝑙 ∈ (ℤ≥‘𝑖)(abs‘((𝐹‘𝑙) − 𝐴)) < 𝑦) ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥))) |
35 | 4, 34 | bitrd 268 |
1
⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑥))) |