Step | Hyp | Ref
| Expression |
1 | | abscl 14874 |
. . . 4
⊢ ((𝐹‘𝑘) ∈ ℂ → (abs‘(𝐹‘𝑘)) ∈ ℝ) |
2 | 1 | ralimi 3087 |
. . 3
⊢
(∀𝑘 ∈
𝑍 (𝐹‘𝑘) ∈ ℂ → ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ) |
3 | | cau3.1 |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | 3 | r19.29uz 14946 |
. . . . . 6
⊢
((∀𝑘 ∈
𝑍 (𝐹‘𝑘) ∈ ℂ ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
5 | 4 | ex 416 |
. . . . 5
⊢
(∀𝑘 ∈
𝑍 (𝐹‘𝑘) ∈ ℂ → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
6 | 5 | ralimdv 3104 |
. . . 4
⊢
(∀𝑘 ∈
𝑍 (𝐹‘𝑘) ∈ ℂ → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
7 | 3 | caubnd2 14953 |
. . . 4
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑧 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧) |
8 | 6, 7 | syl6 35 |
. . 3
⊢
(∀𝑘 ∈
𝑍 (𝐹‘𝑘) ∈ ℂ → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 → ∃𝑧 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧)) |
9 | | fzssuz 13182 |
. . . . . . . 8
⊢ (𝑀...𝑗) ⊆ (ℤ≥‘𝑀) |
10 | 9, 3 | sseqtrri 3954 |
. . . . . . 7
⊢ (𝑀...𝑗) ⊆ 𝑍 |
11 | | ssralv 3983 |
. . . . . . 7
⊢ ((𝑀...𝑗) ⊆ 𝑍 → (∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ)) |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
⊢
(∀𝑘 ∈
𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ) |
13 | | fzfi 13576 |
. . . . . . . 8
⊢ (𝑀...𝑗) ∈ Fin |
14 | | fimaxre3 11807 |
. . . . . . . 8
⊢ (((𝑀...𝑗) ∈ Fin ∧ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ≤ 𝑥) |
15 | 13, 14 | mpan 690 |
. . . . . . 7
⊢
(∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ → ∃𝑥 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ≤ 𝑥) |
16 | | peano2re 11034 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ) |
17 | 16 | adantl 485 |
. . . . . . . . 9
⊢
((∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑥 + 1) ∈ ℝ) |
18 | | ltp1 11701 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → 𝑥 < (𝑥 + 1)) |
19 | 18 | adantl 485 |
. . . . . . . . . . . . . 14
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → 𝑥 < (𝑥 + 1)) |
20 | 16 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑥 + 1) ∈ ℝ) |
21 | | lelttr 10952 |
. . . . . . . . . . . . . . 15
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈ ℝ) →
(((abs‘(𝐹‘𝑘)) ≤ 𝑥 ∧ 𝑥 < (𝑥 + 1)) → (abs‘(𝐹‘𝑘)) < (𝑥 + 1))) |
22 | 20, 21 | mpd3an3 1464 |
. . . . . . . . . . . . . 14
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((abs‘(𝐹‘𝑘)) ≤ 𝑥 ∧ 𝑥 < (𝑥 + 1)) → (abs‘(𝐹‘𝑘)) < (𝑥 + 1))) |
23 | 19, 22 | mpan2d 694 |
. . . . . . . . . . . . 13
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((abs‘(𝐹‘𝑘)) ≤ 𝑥 → (abs‘(𝐹‘𝑘)) < (𝑥 + 1))) |
24 | 23 | expcom 417 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ →
((abs‘(𝐹‘𝑘)) ∈ ℝ →
((abs‘(𝐹‘𝑘)) ≤ 𝑥 → (abs‘(𝐹‘𝑘)) < (𝑥 + 1)))) |
25 | 24 | ralimdv 3104 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
(∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ → ∀𝑘 ∈ (𝑀...𝑗)((abs‘(𝐹‘𝑘)) ≤ 𝑥 → (abs‘(𝐹‘𝑘)) < (𝑥 + 1)))) |
26 | 25 | impcom 411 |
. . . . . . . . . 10
⊢
((∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ∀𝑘 ∈ (𝑀...𝑗)((abs‘(𝐹‘𝑘)) ≤ 𝑥 → (abs‘(𝐹‘𝑘)) < (𝑥 + 1))) |
27 | | ralim 3083 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
(𝑀...𝑗)((abs‘(𝐹‘𝑘)) ≤ 𝑥 → (abs‘(𝐹‘𝑘)) < (𝑥 + 1)) → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ≤ 𝑥 → ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < (𝑥 + 1))) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢
((∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ≤ 𝑥 → ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < (𝑥 + 1))) |
29 | | brralrspcev 5129 |
. . . . . . . . 9
⊢ (((𝑥 + 1) ∈ ℝ ∧
∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < (𝑥 + 1)) → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤) |
30 | 17, 28, 29 | syl6an 684 |
. . . . . . . 8
⊢
((∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ≤ 𝑥 → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤)) |
31 | 30 | rexlimdva 3213 |
. . . . . . 7
⊢
(∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ → (∃𝑥 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ≤ 𝑥 → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤)) |
32 | 15, 31 | mpd 15 |
. . . . . 6
⊢
(∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤) |
33 | 12, 32 | syl 17 |
. . . . 5
⊢
(∀𝑘 ∈
𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤) |
34 | | max1 12804 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑤 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) |
35 | 34 | 3adant3 1134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) → 𝑤 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) |
36 | | simp3 1140 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) →
(abs‘(𝐹‘𝑘)) ∈
ℝ) |
37 | | simp1 1138 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) → 𝑤 ∈
ℝ) |
38 | | ifcl 4500 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ) → if(𝑤 ≤ 𝑧, 𝑧, 𝑤) ∈ ℝ) |
39 | 38 | ancoms 462 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → if(𝑤 ≤ 𝑧, 𝑧, 𝑤) ∈ ℝ) |
40 | 39 | 3adant3 1134 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) →
if(𝑤 ≤ 𝑧, 𝑧, 𝑤) ∈ ℝ) |
41 | | ltletr 10953 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ if(𝑤 ≤ 𝑧, 𝑧, 𝑤) ∈ ℝ) → (((abs‘(𝐹‘𝑘)) < 𝑤 ∧ 𝑤 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
42 | 36, 37, 40, 41 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) →
(((abs‘(𝐹‘𝑘)) < 𝑤 ∧ 𝑤 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
43 | 35, 42 | mpan2d 694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) →
((abs‘(𝐹‘𝑘)) < 𝑤 → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
44 | | max2 12806 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) |
45 | 44 | 3adant3 1134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) → 𝑧 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) |
46 | | simp2 1139 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) → 𝑧 ∈
ℝ) |
47 | | ltletr 10953 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ if(𝑤 ≤ 𝑧, 𝑧, 𝑤) ∈ ℝ) → (((abs‘(𝐹‘𝑘)) < 𝑧 ∧ 𝑧 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
48 | 36, 46, 40, 47 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) →
(((abs‘(𝐹‘𝑘)) < 𝑧 ∧ 𝑧 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
49 | 45, 48 | mpan2d 694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) →
((abs‘(𝐹‘𝑘)) < 𝑧 → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
50 | 43, 49 | jaod 859 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) →
(((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
51 | 50 | 3expia 1123 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
((abs‘(𝐹‘𝑘)) ∈ ℝ →
(((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤)))) |
52 | 51 | ralimdv 3104 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → ∀𝑘 ∈ 𝑍 (((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤)))) |
53 | | ralim 3083 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
𝑍 (((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) → (∀𝑘 ∈ 𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
54 | 52, 53 | syl6 35 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (∀𝑘 ∈ 𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤)))) |
55 | | brralrspcev 5129 |
. . . . . . . . . . . . . 14
⊢
((if(𝑤 ≤ 𝑧, 𝑧, 𝑤) ∈ ℝ ∧ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦) |
56 | 55 | ex 416 |
. . . . . . . . . . . . 13
⊢ (if(𝑤 ≤ 𝑧, 𝑧, 𝑤) ∈ ℝ → (∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)) |
57 | 39, 56 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)) |
58 | 54, 57 | syl6d 75 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (∀𝑘 ∈ 𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦))) |
59 | | uzssz 12488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
60 | 3, 59 | eqsstri 3951 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑍 ⊆
ℤ |
61 | 60 | sseli 3913 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
62 | 60 | sseli 3913 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ) |
63 | | uztric 12491 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈
(ℤ≥‘𝑘) ∨ 𝑘 ∈ (ℤ≥‘𝑗))) |
64 | 61, 62, 63 | syl2anr 600 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → (𝑗 ∈ (ℤ≥‘𝑘) ∨ 𝑘 ∈ (ℤ≥‘𝑗))) |
65 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍) |
66 | 65, 3 | eleqtrdi 2850 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (ℤ≥‘𝑀)) |
67 | | elfzuzb 13135 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ (𝑀...𝑗) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑘))) |
68 | 67 | baib 539 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (𝑘 ∈ (𝑀...𝑗) ↔ 𝑗 ∈ (ℤ≥‘𝑘))) |
69 | 66, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → (𝑘 ∈ (𝑀...𝑗) ↔ 𝑗 ∈ (ℤ≥‘𝑘))) |
70 | 69 | orbi1d 917 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → ((𝑘 ∈ (𝑀...𝑗) ∨ 𝑘 ∈ (ℤ≥‘𝑗)) ↔ (𝑗 ∈ (ℤ≥‘𝑘) ∨ 𝑘 ∈ (ℤ≥‘𝑗)))) |
71 | 64, 70 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → (𝑘 ∈ (𝑀...𝑗) ∨ 𝑘 ∈ (ℤ≥‘𝑗))) |
72 | 71 | ex 416 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ 𝑍 → (𝑘 ∈ 𝑍 → (𝑘 ∈ (𝑀...𝑗) ∨ 𝑘 ∈ (ℤ≥‘𝑗)))) |
73 | | pm3.48 964 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧)) → ((𝑘 ∈ (𝑀...𝑗) ∨ 𝑘 ∈ (ℤ≥‘𝑗)) → ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧))) |
74 | 72, 73 | syl9 77 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ 𝑍 → (((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧)) → (𝑘 ∈ 𝑍 → ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧)))) |
75 | 74 | alimdv 1924 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ 𝑍 → (∀𝑘((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧)) → ∀𝑘(𝑘 ∈ 𝑍 → ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧)))) |
76 | | df-ral 3069 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 ↔ ∀𝑘(𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤)) |
77 | | df-ral 3069 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 ↔ ∀𝑘(𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧)) |
78 | 76, 77 | anbi12i 630 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧) ↔ (∀𝑘(𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤) ∧ ∀𝑘(𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧))) |
79 | | 19.26 1878 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑘((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧)) ↔ (∀𝑘(𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤) ∧ ∀𝑘(𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧))) |
80 | 78, 79 | bitr4i 281 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧) ↔ ∀𝑘((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧))) |
81 | | df-ral 3069 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑘 ∈
𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) ↔ ∀𝑘(𝑘 ∈ 𝑍 → ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧))) |
82 | 75, 80, 81 | 3imtr4g 299 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ 𝑍 → ((∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧) → ∀𝑘 ∈ 𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧))) |
83 | 82 | 3impib 1118 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧) → ∀𝑘 ∈ 𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧)) |
84 | 83 | imim1i 63 |
. . . . . . . . . . . 12
⊢
((∀𝑘 ∈
𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦) → ((𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)) |
85 | 84 | 3expd 1355 |
. . . . . . . . . . 11
⊢
((∀𝑘 ∈
𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦) → (𝑗 ∈ 𝑍 → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)))) |
86 | 58, 85 | syl6 35 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (𝑗 ∈ 𝑍 → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦))))) |
87 | 86 | com23 86 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑗 ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦))))) |
88 | 87 | expimpd 457 |
. . . . . . . 8
⊢ (𝑤 ∈ ℝ → ((𝑧 ∈ ℝ ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦))))) |
89 | 88 | com3r 87 |
. . . . . . 7
⊢
(∀𝑘 ∈
𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (𝑤 ∈ ℝ → ((𝑧 ∈ ℝ ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦))))) |
90 | 89 | com34 91 |
. . . . . 6
⊢
(∀𝑘 ∈
𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (𝑤 ∈ ℝ → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 → ((𝑧 ∈ ℝ ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦))))) |
91 | 90 | rexlimdv 3212 |
. . . . 5
⊢
(∀𝑘 ∈
𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 → ((𝑧 ∈ ℝ ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)))) |
92 | 33, 91 | mpd 15 |
. . . 4
⊢
(∀𝑘 ∈
𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → ((𝑧 ∈ ℝ ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦))) |
93 | 92 | rexlimdvv 3222 |
. . 3
⊢
(∀𝑘 ∈
𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (∃𝑧 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)) |
94 | 2, 8, 93 | sylsyld 61 |
. 2
⊢
(∀𝑘 ∈
𝑍 (𝐹‘𝑘) ∈ ℂ → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)) |
95 | 94 | imp 410 |
1
⊢
((∀𝑘 ∈
𝑍 (𝐹‘𝑘) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦) |