Step | Hyp | Ref
| Expression |
1 | | ulm2.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
2 | | ulmval 23938 |
. . 3
⊢ (𝑆 ∈ 𝑉 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥))) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥))) |
4 | | 3anan12 1044 |
. . . 4
⊢ ((𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝐺:𝑆⟶ℂ ∧ (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥))) |
5 | | ulm2.z |
. . . . . . . . . 10
⊢ 𝑍 =
(ℤ≥‘𝑀) |
6 | | ulm2.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚
𝑆)) |
7 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝐹:𝑍⟶(ℂ ↑𝑚
𝑆) → dom 𝐹 = 𝑍) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = 𝑍) |
9 | | fdm 5964 |
. . . . . . . . . . 11
⊢ (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) → dom 𝐹 = (ℤ≥‘𝑛)) |
10 | 8, 9 | sylan9req 2665 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) → 𝑍 = (ℤ≥‘𝑛)) |
11 | 5, 10 | syl5eqr 2658 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) →
(ℤ≥‘𝑀) = (ℤ≥‘𝑛)) |
12 | | ulm2.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
13 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) → 𝑀 ∈ ℤ) |
14 | | uz11 11586 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ →
((ℤ≥‘𝑀) = (ℤ≥‘𝑛) ↔ 𝑀 = 𝑛)) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) →
((ℤ≥‘𝑀) = (ℤ≥‘𝑛) ↔ 𝑀 = 𝑛)) |
16 | 11, 15 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) → 𝑀 = 𝑛) |
17 | 16 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) → 𝑛 = 𝑀) |
18 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑀 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑀)) |
19 | 18, 5 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑀 → (ℤ≥‘𝑛) = 𝑍) |
20 | 19 | feq2d 5944 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ↔ 𝐹:𝑍⟶(ℂ ↑𝑚
𝑆))) |
21 | 20 | biimparc 503 |
. . . . . . . 8
⊢ ((𝐹:𝑍⟶(ℂ ↑𝑚
𝑆) ∧ 𝑛 = 𝑀) → 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) |
22 | 6, 21 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) |
23 | 17, 22 | impbida 873 |
. . . . . 6
⊢ (𝜑 → (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ↔ 𝑛 = 𝑀)) |
24 | 23 | anbi1d 737 |
. . . . 5
⊢ (𝜑 → ((𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥))) |
25 | | ulm2.g |
. . . . . 6
⊢ (𝜑 → 𝐺:𝑆⟶ℂ) |
26 | 25 | biantrurd 528 |
. . . . 5
⊢ (𝜑 → ((𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝐺:𝑆⟶ℂ ∧ (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)))) |
27 | | simp-4l 802 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → 𝜑) |
28 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝑛 = 𝑀) |
29 | | uzid 11578 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
30 | 12, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
31 | 30, 5 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
32 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝑀 ∈ 𝑍) |
33 | 28, 32 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝑛 ∈ 𝑍) |
34 | 5 | uztrn2 11581 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ 𝑍) |
35 | 33, 34 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ 𝑍) |
36 | 5 | uztrn2 11581 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
37 | 35, 36 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → 𝑘 ∈ 𝑍) |
39 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
40 | | ulm2.b |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵) |
41 | 27, 38, 39, 40 | syl12anc 1316 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑘)‘𝑧) = 𝐵) |
42 | | ulm2.a |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴) |
43 | 27, 42 | sylancom 698 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴) |
44 | 41, 43 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)) = (𝐵 − 𝐴)) |
45 | 44 | fveq2d 6107 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) = (abs‘(𝐵 − 𝐴))) |
46 | 45 | breq1d 4593 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → ((abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ (abs‘(𝐵 − 𝐴)) < 𝑥)) |
47 | 46 | ralbidva 2968 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
48 | 47 | ralbidva 2968 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → (∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
49 | 48 | rexbidva 3031 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
50 | 49 | ralbidv 2969 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
51 | 50 | pm5.32da 671 |
. . . . 5
⊢ (𝜑 → ((𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))) |
52 | 24, 26, 51 | 3bitr3d 297 |
. . . 4
⊢ (𝜑 → ((𝐺:𝑆⟶ℂ ∧ (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))) |
53 | 4, 52 | syl5bb 271 |
. . 3
⊢ (𝜑 → ((𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))) |
54 | 53 | rexbidv 3034 |
. 2
⊢ (𝜑 → (∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ ∃𝑛 ∈ ℤ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))) |
55 | 19 | rexeqdv 3122 |
. . . . 5
⊢ (𝑛 = 𝑀 → (∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
56 | 55 | ralbidv 2969 |
. . . 4
⊢ (𝑛 = 𝑀 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
57 | 56 | ceqsrexv 3306 |
. . 3
⊢ (𝑀 ∈ ℤ →
(∃𝑛 ∈ ℤ
(𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
58 | 12, 57 | syl 17 |
. 2
⊢ (𝜑 → (∃𝑛 ∈ ℤ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
59 | 3, 54, 58 | 3bitrd 293 |
1
⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |