Step | Hyp | Ref
| Expression |
1 | | ulm2.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
2 | | ulmval 24687 |
. . 3
⊢ (𝑆 ∈ 𝑉 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥))) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥))) |
4 | | 3anan12 1078 |
. . . 4
⊢ ((𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝐺:𝑆⟶ℂ ∧ (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥))) |
5 | | ulm2.z |
. . . . . . . . . 10
⊢ 𝑍 =
(ℤ≥‘𝑀) |
6 | | ulm2.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚
𝑆)) |
7 | 6 | fdmd 6351 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = 𝑍) |
8 | | fdm 6350 |
. . . . . . . . . . 11
⊢ (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) → dom 𝐹 = (ℤ≥‘𝑛)) |
9 | 7, 8 | sylan9req 2830 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) → 𝑍 = (ℤ≥‘𝑛)) |
10 | 5, 9 | syl5eqr 2823 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) →
(ℤ≥‘𝑀) = (ℤ≥‘𝑛)) |
11 | | ulm2.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
12 | 11 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) → 𝑀 ∈ ℤ) |
13 | | uz11 12080 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ →
((ℤ≥‘𝑀) = (ℤ≥‘𝑛) ↔ 𝑀 = 𝑛)) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) →
((ℤ≥‘𝑀) = (ℤ≥‘𝑛) ↔ 𝑀 = 𝑛)) |
15 | 10, 14 | mpbid 224 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) → 𝑀 = 𝑛) |
16 | 15 | eqcomd 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) → 𝑛 = 𝑀) |
17 | | fveq2 6497 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑀 → (ℤ≥‘𝑛) =
(ℤ≥‘𝑀)) |
18 | 17, 5 | syl6eqr 2827 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑀 → (ℤ≥‘𝑛) = 𝑍) |
19 | 18 | feq2d 6328 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ↔ 𝐹:𝑍⟶(ℂ ↑𝑚
𝑆))) |
20 | 19 | biimparc 472 |
. . . . . . . 8
⊢ ((𝐹:𝑍⟶(ℂ ↑𝑚
𝑆) ∧ 𝑛 = 𝑀) → 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) |
21 | 6, 20 | sylan 572 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆)) |
22 | 16, 21 | impbida 789 |
. . . . . 6
⊢ (𝜑 → (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ↔ 𝑛 = 𝑀)) |
23 | 22 | anbi1d 621 |
. . . . 5
⊢ (𝜑 → ((𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥))) |
24 | | ulm2.g |
. . . . . 6
⊢ (𝜑 → 𝐺:𝑆⟶ℂ) |
25 | 24 | biantrurd 525 |
. . . . 5
⊢ (𝜑 → ((𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝐺:𝑆⟶ℂ ∧ (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)))) |
26 | | simp-4l 771 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → 𝜑) |
27 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝑛 = 𝑀) |
28 | | uzid 12072 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
29 | 11, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
30 | 29, 5 | syl6eleqr 2872 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
31 | 30 | adantr 473 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝑀 ∈ 𝑍) |
32 | 27, 31 | eqeltrd 2861 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝑛 ∈ 𝑍) |
33 | 5 | uztrn2 12075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ 𝑍) |
34 | 32, 33 | sylan 572 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ 𝑍) |
35 | 5 | uztrn2 12075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
36 | 34, 35 | sylan 572 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
37 | 36 | adantr 473 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → 𝑘 ∈ 𝑍) |
38 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
39 | | ulm2.b |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵) |
40 | 26, 37, 38, 39 | syl12anc 825 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑘)‘𝑧) = 𝐵) |
41 | | ulm2.a |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴) |
42 | 26, 41 | sylancom 580 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴) |
43 | 40, 42 | oveq12d 6993 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)) = (𝐵 − 𝐴)) |
44 | 43 | fveq2d 6501 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) = (abs‘(𝐵 − 𝐴))) |
45 | 44 | breq1d 4936 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → ((abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ (abs‘(𝐵 − 𝐴)) < 𝑥)) |
46 | 45 | ralbidva 3141 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
47 | 46 | ralbidva 3141 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → (∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
48 | 47 | rexbidva 3236 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
49 | 48 | ralbidv 3142 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
50 | 49 | pm5.32da 571 |
. . . . 5
⊢ (𝜑 → ((𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))) |
51 | 23, 25, 50 | 3bitr3d 301 |
. . . 4
⊢ (𝜑 → ((𝐺:𝑆⟶ℂ ∧ (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))) |
52 | 4, 51 | syl5bb 275 |
. . 3
⊢ (𝜑 → ((𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))) |
53 | 52 | rexbidv 3237 |
. 2
⊢ (𝜑 → (∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ
↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ ∃𝑛 ∈ ℤ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))) |
54 | 18 | rexeqdv 3351 |
. . . . 5
⊢ (𝑛 = 𝑀 → (∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
55 | 54 | ralbidv 3142 |
. . . 4
⊢ (𝑛 = 𝑀 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
56 | 55 | ceqsrexv 3558 |
. . 3
⊢ (𝑀 ∈ ℤ →
(∃𝑛 ∈ ℤ
(𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
57 | 11, 56 | syl 17 |
. 2
⊢ (𝜑 → (∃𝑛 ∈ ℤ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈
(ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |
58 | 3, 53, 57 | 3bitrd 297 |
1
⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)) |