Step | Hyp | Ref
| Expression |
1 | | abscl 14018 |
. . . 4
⊢ ((𝐹‘𝑘) ∈ ℂ → (abs‘(𝐹‘𝑘)) ∈ ℝ) |
2 | 1 | ralimi 2952 |
. . 3
⊢
(∀𝑘 ∈
𝑍 (𝐹‘𝑘) ∈ ℂ → ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ) |
3 | | cau3.1 |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | 3 | r19.29uz 14090 |
. . . . . 6
⊢
((∀𝑘 ∈
𝑍 (𝐹‘𝑘) ∈ ℂ ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥)) |
5 | 4 | ex 450 |
. . . . 5
⊢
(∀𝑘 ∈
𝑍 (𝐹‘𝑘) ∈ ℂ → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
6 | 5 | ralimdv 2963 |
. . . 4
⊢
(∀𝑘 ∈
𝑍 (𝐹‘𝑘) ∈ ℂ → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥))) |
7 | 3 | caubnd2 14097 |
. . . 4
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑧 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧) |
8 | 6, 7 | syl6 35 |
. . 3
⊢
(∀𝑘 ∈
𝑍 (𝐹‘𝑘) ∈ ℂ → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 → ∃𝑧 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧)) |
9 | | fzssuz 12382 |
. . . . . . . 8
⊢ (𝑀...𝑗) ⊆ (ℤ≥‘𝑀) |
10 | 9, 3 | sseqtr4i 3638 |
. . . . . . 7
⊢ (𝑀...𝑗) ⊆ 𝑍 |
11 | | ssralv 3666 |
. . . . . . 7
⊢ ((𝑀...𝑗) ⊆ 𝑍 → (∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ)) |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
⊢
(∀𝑘 ∈
𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ) |
13 | | fzfi 12771 |
. . . . . . . 8
⊢ (𝑀...𝑗) ∈ Fin |
14 | | fimaxre3 10970 |
. . . . . . . 8
⊢ (((𝑀...𝑗) ∈ Fin ∧ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ≤ 𝑥) |
15 | 13, 14 | mpan 706 |
. . . . . . 7
⊢
(∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ → ∃𝑥 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ≤ 𝑥) |
16 | | peano2re 10209 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ) |
17 | 16 | adantl 482 |
. . . . . . . . 9
⊢
((∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑥 + 1) ∈ ℝ) |
18 | | ltp1 10861 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → 𝑥 < (𝑥 + 1)) |
19 | 18 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → 𝑥 < (𝑥 + 1)) |
20 | 16 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑥 + 1) ∈ ℝ) |
21 | | lelttr 10128 |
. . . . . . . . . . . . . . 15
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈ ℝ) →
(((abs‘(𝐹‘𝑘)) ≤ 𝑥 ∧ 𝑥 < (𝑥 + 1)) → (abs‘(𝐹‘𝑘)) < (𝑥 + 1))) |
22 | 20, 21 | mpd3an3 1425 |
. . . . . . . . . . . . . 14
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((abs‘(𝐹‘𝑘)) ≤ 𝑥 ∧ 𝑥 < (𝑥 + 1)) → (abs‘(𝐹‘𝑘)) < (𝑥 + 1))) |
23 | 19, 22 | mpan2d 710 |
. . . . . . . . . . . . 13
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((abs‘(𝐹‘𝑘)) ≤ 𝑥 → (abs‘(𝐹‘𝑘)) < (𝑥 + 1))) |
24 | 23 | expcom 451 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ →
((abs‘(𝐹‘𝑘)) ∈ ℝ →
((abs‘(𝐹‘𝑘)) ≤ 𝑥 → (abs‘(𝐹‘𝑘)) < (𝑥 + 1)))) |
25 | 24 | ralimdv 2963 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
(∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ → ∀𝑘 ∈ (𝑀...𝑗)((abs‘(𝐹‘𝑘)) ≤ 𝑥 → (abs‘(𝐹‘𝑘)) < (𝑥 + 1)))) |
26 | 25 | impcom 446 |
. . . . . . . . . 10
⊢
((∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ∀𝑘 ∈ (𝑀...𝑗)((abs‘(𝐹‘𝑘)) ≤ 𝑥 → (abs‘(𝐹‘𝑘)) < (𝑥 + 1))) |
27 | | ralim 2948 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
(𝑀...𝑗)((abs‘(𝐹‘𝑘)) ≤ 𝑥 → (abs‘(𝐹‘𝑘)) < (𝑥 + 1)) → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ≤ 𝑥 → ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < (𝑥 + 1))) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢
((∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ≤ 𝑥 → ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < (𝑥 + 1))) |
29 | | breq2 4657 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑥 + 1) → ((abs‘(𝐹‘𝑘)) < 𝑤 ↔ (abs‘(𝐹‘𝑘)) < (𝑥 + 1))) |
30 | 29 | ralbidv 2986 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑥 + 1) → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 ↔ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < (𝑥 + 1))) |
31 | 30 | rspcev 3309 |
. . . . . . . . 9
⊢ (((𝑥 + 1) ∈ ℝ ∧
∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < (𝑥 + 1)) → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤) |
32 | 17, 28, 31 | syl6an 568 |
. . . . . . . 8
⊢
((∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ≤ 𝑥 → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤)) |
33 | 32 | rexlimdva 3031 |
. . . . . . 7
⊢
(∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ → (∃𝑥 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) ≤ 𝑥 → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤)) |
34 | 15, 33 | mpd 15 |
. . . . . 6
⊢
(∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) ∈ ℝ → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤) |
35 | 12, 34 | syl 17 |
. . . . 5
⊢
(∀𝑘 ∈
𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → ∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤) |
36 | | max1 12016 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑤 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) |
37 | 36 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) → 𝑤 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) |
38 | | simp3 1063 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) →
(abs‘(𝐹‘𝑘)) ∈
ℝ) |
39 | | simp1 1061 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) → 𝑤 ∈
ℝ) |
40 | | ifcl 4130 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ) → if(𝑤 ≤ 𝑧, 𝑧, 𝑤) ∈ ℝ) |
41 | 40 | ancoms 469 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → if(𝑤 ≤ 𝑧, 𝑧, 𝑤) ∈ ℝ) |
42 | 41 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) →
if(𝑤 ≤ 𝑧, 𝑧, 𝑤) ∈ ℝ) |
43 | | ltletr 10129 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ if(𝑤 ≤ 𝑧, 𝑧, 𝑤) ∈ ℝ) → (((abs‘(𝐹‘𝑘)) < 𝑤 ∧ 𝑤 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
44 | 38, 39, 42, 43 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) →
(((abs‘(𝐹‘𝑘)) < 𝑤 ∧ 𝑤 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
45 | 37, 44 | mpan2d 710 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) →
((abs‘(𝐹‘𝑘)) < 𝑤 → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
46 | | max2 12018 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → 𝑧 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) |
47 | 46 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) → 𝑧 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) |
48 | | simp2 1062 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) → 𝑧 ∈
ℝ) |
49 | | ltletr 10129 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘(𝐹‘𝑘)) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ if(𝑤 ≤ 𝑧, 𝑧, 𝑤) ∈ ℝ) → (((abs‘(𝐹‘𝑘)) < 𝑧 ∧ 𝑧 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
50 | 38, 48, 42, 49 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) →
(((abs‘(𝐹‘𝑘)) < 𝑧 ∧ 𝑧 ≤ if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
51 | 47, 50 | mpan2d 710 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) →
((abs‘(𝐹‘𝑘)) < 𝑧 → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
52 | 45, 51 | jaod 395 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧
(abs‘(𝐹‘𝑘)) ∈ ℝ) →
(((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
53 | 52 | 3expia 1267 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
((abs‘(𝐹‘𝑘)) ∈ ℝ →
(((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤)))) |
54 | 53 | ralimdv 2963 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → ∀𝑘 ∈ 𝑍 (((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤)))) |
55 | | ralim 2948 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
𝑍 (((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) → (∀𝑘 ∈ 𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
56 | 54, 55 | syl6 35 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (∀𝑘 ∈ 𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤)))) |
57 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = if(𝑤 ≤ 𝑧, 𝑧, 𝑤) → ((abs‘(𝐹‘𝑘)) < 𝑦 ↔ (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
58 | 57 | ralbidv 2986 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = if(𝑤 ≤ 𝑧, 𝑧, 𝑤) → (∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦 ↔ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤))) |
59 | 58 | rspcev 3309 |
. . . . . . . . . . . . . 14
⊢
((if(𝑤 ≤ 𝑧, 𝑧, 𝑤) ∈ ℝ ∧ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤)) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦) |
60 | 59 | ex 450 |
. . . . . . . . . . . . 13
⊢ (if(𝑤 ≤ 𝑧, 𝑧, 𝑤) ∈ ℝ → (∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)) |
61 | 41, 60 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < if(𝑤 ≤ 𝑧, 𝑧, 𝑤) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)) |
62 | 56, 61 | syl6d 75 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (∀𝑘 ∈ 𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦))) |
63 | | uzssz 11707 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
64 | 3, 63 | eqsstri 3635 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑍 ⊆
ℤ |
65 | 64 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
66 | 64 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ) |
67 | | uztric 11709 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈
(ℤ≥‘𝑘) ∨ 𝑘 ∈ (ℤ≥‘𝑗))) |
68 | 65, 66, 67 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → (𝑗 ∈ (ℤ≥‘𝑘) ∨ 𝑘 ∈ (ℤ≥‘𝑗))) |
69 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍) |
70 | 69, 3 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (ℤ≥‘𝑀)) |
71 | | elfzuzb 12336 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ (𝑀...𝑗) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑘))) |
72 | 71 | baib 944 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (𝑘 ∈ (𝑀...𝑗) ↔ 𝑗 ∈ (ℤ≥‘𝑘))) |
73 | 70, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → (𝑘 ∈ (𝑀...𝑗) ↔ 𝑗 ∈ (ℤ≥‘𝑘))) |
74 | 73 | orbi1d 739 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → ((𝑘 ∈ (𝑀...𝑗) ∨ 𝑘 ∈ (ℤ≥‘𝑗)) ↔ (𝑗 ∈ (ℤ≥‘𝑘) ∨ 𝑘 ∈ (ℤ≥‘𝑗)))) |
75 | 68, 74 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍) → (𝑘 ∈ (𝑀...𝑗) ∨ 𝑘 ∈ (ℤ≥‘𝑗))) |
76 | 75 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ 𝑍 → (𝑘 ∈ 𝑍 → (𝑘 ∈ (𝑀...𝑗) ∨ 𝑘 ∈ (ℤ≥‘𝑗)))) |
77 | | pm3.48 878 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧)) → ((𝑘 ∈ (𝑀...𝑗) ∨ 𝑘 ∈ (ℤ≥‘𝑗)) → ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧))) |
78 | 76, 77 | syl9 77 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ 𝑍 → (((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧)) → (𝑘 ∈ 𝑍 → ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧)))) |
79 | 78 | alimdv 1845 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ 𝑍 → (∀𝑘((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧)) → ∀𝑘(𝑘 ∈ 𝑍 → ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧)))) |
80 | | df-ral 2917 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 ↔ ∀𝑘(𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤)) |
81 | | df-ral 2917 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 ↔ ∀𝑘(𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧)) |
82 | 80, 81 | anbi12i 733 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧) ↔ (∀𝑘(𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤) ∧ ∀𝑘(𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧))) |
83 | | 19.26 1798 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑘((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧)) ↔ (∀𝑘(𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤) ∧ ∀𝑘(𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧))) |
84 | 82, 83 | bitr4i 267 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑘 ∈
(𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧) ↔ ∀𝑘((𝑘 ∈ (𝑀...𝑗) → (abs‘(𝐹‘𝑘)) < 𝑤) ∧ (𝑘 ∈ (ℤ≥‘𝑗) → (abs‘(𝐹‘𝑘)) < 𝑧))) |
85 | | df-ral 2917 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑘 ∈
𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) ↔ ∀𝑘(𝑘 ∈ 𝑍 → ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧))) |
86 | 79, 84, 85 | 3imtr4g 285 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ 𝑍 → ((∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧) → ∀𝑘 ∈ 𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧))) |
87 | 86 | 3impib 1262 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧) → ∀𝑘 ∈ 𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧)) |
88 | 87 | imim1i 63 |
. . . . . . . . . . . 12
⊢
((∀𝑘 ∈
𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦) → ((𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)) |
89 | 88 | 3expd 1284 |
. . . . . . . . . . 11
⊢
((∀𝑘 ∈
𝑍 ((abs‘(𝐹‘𝑘)) < 𝑤 ∨ (abs‘(𝐹‘𝑘)) < 𝑧) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦) → (𝑗 ∈ 𝑍 → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)))) |
90 | 62, 89 | syl6 35 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) →
(∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (𝑗 ∈ 𝑍 → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦))))) |
91 | 90 | com23 86 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑗 ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦))))) |
92 | 91 | expimpd 629 |
. . . . . . . 8
⊢ (𝑤 ∈ ℝ → ((𝑧 ∈ ℝ ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦))))) |
93 | 92 | com3r 87 |
. . . . . . 7
⊢
(∀𝑘 ∈
𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (𝑤 ∈ ℝ → ((𝑧 ∈ ℝ ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦))))) |
94 | 93 | com34 91 |
. . . . . 6
⊢
(∀𝑘 ∈
𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (𝑤 ∈ ℝ → (∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 → ((𝑧 ∈ ℝ ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦))))) |
95 | 94 | rexlimdv 3030 |
. . . . 5
⊢
(∀𝑘 ∈
𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (∃𝑤 ∈ ℝ ∀𝑘 ∈ (𝑀...𝑗)(abs‘(𝐹‘𝑘)) < 𝑤 → ((𝑧 ∈ ℝ ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)))) |
96 | 35, 95 | mpd 15 |
. . . 4
⊢
(∀𝑘 ∈
𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → ((𝑧 ∈ ℝ ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦))) |
97 | 96 | rexlimdvv 3037 |
. . 3
⊢
(∀𝑘 ∈
𝑍 (abs‘(𝐹‘𝑘)) ∈ ℝ → (∃𝑧 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(𝐹‘𝑘)) < 𝑧 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)) |
98 | 2, 8, 97 | sylsyld 61 |
. 2
⊢
(∀𝑘 ∈
𝑍 (𝐹‘𝑘) ∈ ℂ → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦)) |
99 | 98 | imp 445 |
1
⊢
((∀𝑘 ∈
𝑍 (𝐹‘𝑘) ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − (𝐹‘𝑗))) < 𝑥) → ∃𝑦 ∈ ℝ ∀𝑘 ∈ 𝑍 (abs‘(𝐹‘𝑘)) < 𝑦) |