Step | Hyp | Ref
| Expression |
1 | | caures.1 |
. . . . . . . . . . 11
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | 1 | uztrn2 11705 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
3 | 2 | adantll 750 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
4 | 3 | biantrurd 529 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝑘 ∈ dom 𝐹 ↔ (𝑘 ∈ 𝑍 ∧ 𝑘 ∈ dom 𝐹))) |
5 | | dmres 5419 |
. . . . . . . . 9
⊢ dom
(𝐹 ↾ 𝑍) = (𝑍 ∩ dom 𝐹) |
6 | 5 | elin2 3801 |
. . . . . . . 8
⊢ (𝑘 ∈ dom (𝐹 ↾ 𝑍) ↔ (𝑘 ∈ 𝑍 ∧ 𝑘 ∈ dom 𝐹)) |
7 | 4, 6 | syl6bbr 278 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝑘 ∈ dom 𝐹 ↔ 𝑘 ∈ dom (𝐹 ↾ 𝑍))) |
8 | 7 | 3anbi1d 1403 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥) ↔ (𝑘 ∈ dom (𝐹 ↾ 𝑍) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥))) |
9 | 8 | ralbidva 2985 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐹 ↾ 𝑍) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥))) |
10 | 9 | rexbidva 3049 |
. . . 4
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥) ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐹 ↾ 𝑍) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥))) |
11 | 10 | ralbidv 2986 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐹 ↾ 𝑍) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥))) |
12 | | caures.5 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝑋 ↑pm
ℂ)) |
13 | 12 | biantrurd 529 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)))) |
14 | | caures.4 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
15 | | elfvdm 6220 |
. . . . . . 7
⊢ (𝐷 ∈ (Met‘𝑋) → 𝑋 ∈ dom Met) |
16 | 14, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ dom Met) |
17 | | cnex 10017 |
. . . . . 6
⊢ ℂ
∈ V |
18 | | ssid 3624 |
. . . . . . 7
⊢ 𝑋 ⊆ 𝑋 |
19 | | uzssz 11707 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
20 | | zsscn 11385 |
. . . . . . . . 9
⊢ ℤ
⊆ ℂ |
21 | 19, 20 | sstri 3612 |
. . . . . . . 8
⊢
(ℤ≥‘𝑀) ⊆ ℂ |
22 | 1, 21 | eqsstri 3635 |
. . . . . . 7
⊢ 𝑍 ⊆
ℂ |
23 | | pmss12g 7884 |
. . . . . . 7
⊢ (((𝑋 ⊆ 𝑋 ∧ 𝑍 ⊆ ℂ) ∧ (𝑋 ∈ dom Met ∧ ℂ ∈ V))
→ (𝑋
↑pm 𝑍) ⊆ (𝑋 ↑pm
ℂ)) |
24 | 18, 22, 23 | mpanl12 718 |
. . . . . 6
⊢ ((𝑋 ∈ dom Met ∧ ℂ
∈ V) → (𝑋
↑pm 𝑍) ⊆ (𝑋 ↑pm
ℂ)) |
25 | 16, 17, 24 | sylancl 694 |
. . . . 5
⊢ (𝜑 → (𝑋 ↑pm 𝑍) ⊆ (𝑋 ↑pm
ℂ)) |
26 | | fvex 6201 |
. . . . . . 7
⊢
(ℤ≥‘𝑀) ∈ V |
27 | 1, 26 | eqeltri 2697 |
. . . . . 6
⊢ 𝑍 ∈ V |
28 | | pmresg 7885 |
. . . . . 6
⊢ ((𝑍 ∈ V ∧ 𝐹 ∈ (𝑋 ↑pm ℂ)) →
(𝐹 ↾ 𝑍) ∈ (𝑋 ↑pm 𝑍)) |
29 | 27, 12, 28 | sylancr 695 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ 𝑍) ∈ (𝑋 ↑pm 𝑍)) |
30 | 25, 29 | sseldd 3604 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ 𝑍) ∈ (𝑋 ↑pm
ℂ)) |
31 | 30 | biantrurd 529 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐹 ↾ 𝑍) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥) ↔ ((𝐹 ↾ 𝑍) ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐹 ↾ 𝑍) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)))) |
32 | 11, 13, 31 | 3bitr3d 298 |
. 2
⊢ (𝜑 → ((𝐹 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)) ↔ ((𝐹 ↾ 𝑍) ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐹 ↾ 𝑍) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)))) |
33 | | metxmet 22139 |
. . . 4
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
34 | 14, 33 | syl 17 |
. . 3
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
35 | | caures.3 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
36 | | eqidd 2623 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
37 | | eqidd 2623 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) = (𝐹‘𝑗)) |
38 | 1, 34, 35, 36, 37 | iscau4 23077 |
. 2
⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)))) |
39 | | fvres 6207 |
. . . 4
⊢ (𝑘 ∈ 𝑍 → ((𝐹 ↾ 𝑍)‘𝑘) = (𝐹‘𝑘)) |
40 | 39 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐹 ↾ 𝑍)‘𝑘) = (𝐹‘𝑘)) |
41 | | fvres 6207 |
. . . 4
⊢ (𝑗 ∈ 𝑍 → ((𝐹 ↾ 𝑍)‘𝑗) = (𝐹‘𝑗)) |
42 | 41 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → ((𝐹 ↾ 𝑍)‘𝑗) = (𝐹‘𝑗)) |
43 | 1, 34, 35, 40, 42 | iscau4 23077 |
. 2
⊢ (𝜑 → ((𝐹 ↾ 𝑍) ∈ (Cau‘𝐷) ↔ ((𝐹 ↾ 𝑍) ∈ (𝑋 ↑pm ℂ) ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom (𝐹 ↾ 𝑍) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)))) |
44 | 32, 38, 43 | 3bitr4d 300 |
1
⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ↾ 𝑍) ∈ (Cau‘𝐷))) |