Step | Hyp | Ref
| Expression |
1 | | climcauc.1 |
. . . 4
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | simpl 108 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) →
𝑀 ∈
ℤ) |
3 | | 1rp 9614 |
. . . . 5
⊢ 1 ∈
ℝ+ |
4 | 3 | a1i 9 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → 1
∈ ℝ+) |
5 | | eqidd 2171 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) ∧
𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
6 | | climdm 11258 |
. . . . . 6
⊢ (𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘𝐹)) |
7 | 6 | biimpi 119 |
. . . . 5
⊢ (𝐹 ∈ dom ⇝ → 𝐹 ⇝ ( ⇝ ‘𝐹)) |
8 | 7 | adantl 275 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) →
𝐹 ⇝ ( ⇝
‘𝐹)) |
9 | 1, 2, 4, 5, 8 | climi 11250 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) →
∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1)) |
10 | | simpl 108 |
. . . . 5
⊢ (((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1) → (𝐹‘𝑘) ∈ ℂ) |
11 | 10 | ralimi 2533 |
. . . 4
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1) → ∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) |
12 | 11 | reximi 2567 |
. . 3
⊢
(∃𝑛 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑛)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − ( ⇝ ‘𝐹))) < 1) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) |
13 | 9, 12 | syl 14 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) →
∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) |
14 | | eluzelz 9496 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → 𝑛 ∈ ℤ) |
15 | 14, 1 | eleq2s 2265 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
16 | | eqid 2170 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘𝑛) = (ℤ≥‘𝑛) |
17 | 16 | climcau 11310 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) →
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) |
18 | 15, 17 | sylan 281 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ 𝑍 ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) |
19 | 16 | r19.29uz 10956 |
. . . . . . . . . . . 12
⊢
((∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ ∧ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
20 | 19 | ex 114 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ → (∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 → ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
21 | 20 | ralimdv 2538 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ → (∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
22 | 18, 21 | mpan9 279 |
. . . . . . . . 9
⊢ (((𝑛 ∈ 𝑍 ∧ 𝐹 ∈ dom ⇝ ) ∧ ∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
23 | 22 | an32s 563 |
. . . . . . . 8
⊢ (((𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ) ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
24 | 23 | adantll 473 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) ∧ 𝐹 ∈ dom ⇝ ) → ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
25 | 24 | ex 114 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) → (𝐹 ∈ dom ⇝ → ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
26 | 1, 16 | cau4 11080 |
. . . . . . 7
⊢ (𝑛 ∈ 𝑍 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
27 | 26 | ad2antrl 487 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
28 | 25, 27 | sylibrd 168 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ)) → (𝐹 ∈ dom ⇝ → ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
29 | 28 | rexlimdvaa 2588 |
. . . 4
⊢ (𝑀 ∈ ℤ →
(∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ → (𝐹 ∈ dom ⇝ → ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)))) |
30 | 29 | com23 78 |
. . 3
⊢ (𝑀 ∈ ℤ → (𝐹 ∈ dom ⇝ →
(∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ → ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)))) |
31 | 30 | imp 123 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) →
(∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(𝐹‘𝑘) ∈ ℂ → ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
32 | 13, 31 | mpd 13 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) →
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |