Step | Hyp | Ref
| Expression |
1 | | cncfshift.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ)) |
2 | | cncff 22696 |
. . . . . 6
⊢ (𝐹 ∈ (𝐴–cn→ℂ) → 𝐹:𝐴⟶ℂ) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
4 | 3 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐹:𝐴⟶ℂ) |
5 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
6 | | cncfshift.b |
. . . . . . . 8
⊢ 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)} |
7 | 5, 6 | syl6eleq 2711 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)}) |
8 | | rabid 3116 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)} ↔ (𝑥 ∈ ℂ ∧ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇))) |
9 | 7, 8 | sylib 208 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ ℂ ∧ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇))) |
10 | 9 | simprd 479 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)) |
11 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 + 𝑇) → (𝑥 − 𝑇) = ((𝑦 + 𝑇) − 𝑇)) |
12 | 11 | 3ad2ant3 1084 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 = (𝑦 + 𝑇)) → (𝑥 − 𝑇) = ((𝑦 + 𝑇) − 𝑇)) |
13 | | cncfshift.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
14 | 13 | sselda 3603 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ) |
15 | | cncfshift.t |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ ℂ) |
16 | 15 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑇 ∈ ℂ) |
17 | 14, 16 | pncand 10393 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝑦 + 𝑇) − 𝑇) = 𝑦) |
18 | 17 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐴) → ((𝑦 + 𝑇) − 𝑇) = 𝑦) |
19 | 18 | 3adant3 1081 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 = (𝑦 + 𝑇)) → ((𝑦 + 𝑇) − 𝑇) = 𝑦) |
20 | 12, 19 | eqtrd 2656 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 = (𝑦 + 𝑇)) → (𝑥 − 𝑇) = 𝑦) |
21 | | simp2 1062 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 = (𝑦 + 𝑇)) → 𝑦 ∈ 𝐴) |
22 | 20, 21 | eqeltrd 2701 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 = (𝑦 + 𝑇)) → (𝑥 − 𝑇) ∈ 𝐴) |
23 | 22 | rexlimdv3a 3033 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇) → (𝑥 − 𝑇) ∈ 𝐴)) |
24 | 10, 23 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 − 𝑇) ∈ 𝐴) |
25 | 4, 24 | ffvelrnd 6360 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹‘(𝑥 − 𝑇)) ∈ ℂ) |
26 | | cncfshift.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐹‘(𝑥 − 𝑇))) |
27 | 25, 26 | fmptd 6385 |
. 2
⊢ (𝜑 → 𝐺:𝐵⟶ℂ) |
28 | 1 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐹 ∈ (𝐴–cn→ℂ)) |
29 | 13 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ⊆ ℂ) |
30 | | ssid 3624 |
. . . . . . . . . 10
⊢ ℂ
⊆ ℂ |
31 | | elcncf 22692 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝐹
∈ (𝐴–cn→ℂ) ↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑎 ∈ 𝐴 ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑏 ∈ 𝐴 ((abs‘(𝑎 − 𝑏)) < 𝑧 → (abs‘((𝐹‘𝑎) − (𝐹‘𝑏))) < 𝑤)))) |
32 | 29, 30, 31 | sylancl 694 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹 ∈ (𝐴–cn→ℂ) ↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑎 ∈ 𝐴 ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑏 ∈ 𝐴 ((abs‘(𝑎 − 𝑏)) < 𝑧 → (abs‘((𝐹‘𝑎) − (𝐹‘𝑏))) < 𝑤)))) |
33 | 28, 32 | mpbid 222 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹:𝐴⟶ℂ ∧ ∀𝑎 ∈ 𝐴 ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑏 ∈ 𝐴 ((abs‘(𝑎 − 𝑏)) < 𝑧 → (abs‘((𝐹‘𝑎) − (𝐹‘𝑏))) < 𝑤))) |
34 | 33 | simprd 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑎 ∈ 𝐴 ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑏 ∈ 𝐴 ((abs‘(𝑎 − 𝑏)) < 𝑧 → (abs‘((𝐹‘𝑎) − (𝐹‘𝑏))) < 𝑤)) |
35 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (𝑥 − 𝑇) → (𝑎 − 𝑏) = ((𝑥 − 𝑇) − 𝑏)) |
36 | 35 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑥 − 𝑇) → (abs‘(𝑎 − 𝑏)) = (abs‘((𝑥 − 𝑇) − 𝑏))) |
37 | 36 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑥 − 𝑇) → ((abs‘(𝑎 − 𝑏)) < 𝑧 ↔ (abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧)) |
38 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑥 − 𝑇) → (𝐹‘𝑎) = (𝐹‘(𝑥 − 𝑇))) |
39 | 38 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (𝑥 − 𝑇) → ((𝐹‘𝑎) − (𝐹‘𝑏)) = ((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) |
40 | 39 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑥 − 𝑇) → (abs‘((𝐹‘𝑎) − (𝐹‘𝑏))) = (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏)))) |
41 | 40 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑥 − 𝑇) → ((abs‘((𝐹‘𝑎) − (𝐹‘𝑏))) < 𝑤 ↔ (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) |
42 | 37, 41 | imbi12d 334 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑥 − 𝑇) → (((abs‘(𝑎 − 𝑏)) < 𝑧 → (abs‘((𝐹‘𝑎) − (𝐹‘𝑏))) < 𝑤) ↔ ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤))) |
43 | 42 | rexralbidv 3058 |
. . . . . . . . 9
⊢ (𝑎 = (𝑥 − 𝑇) → (∃𝑧 ∈ ℝ+ ∀𝑏 ∈ 𝐴 ((abs‘(𝑎 − 𝑏)) < 𝑧 → (abs‘((𝐹‘𝑎) − (𝐹‘𝑏))) < 𝑤) ↔ ∃𝑧 ∈ ℝ+ ∀𝑏 ∈ 𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤))) |
44 | 43 | ralbidv 2986 |
. . . . . . . 8
⊢ (𝑎 = (𝑥 − 𝑇) → (∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑏 ∈ 𝐴 ((abs‘(𝑎 − 𝑏)) < 𝑧 → (abs‘((𝐹‘𝑎) − (𝐹‘𝑏))) < 𝑤) ↔ ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑏 ∈ 𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤))) |
45 | 44 | rspcva 3307 |
. . . . . . 7
⊢ (((𝑥 − 𝑇) ∈ 𝐴 ∧ ∀𝑎 ∈ 𝐴 ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑏 ∈ 𝐴 ((abs‘(𝑎 − 𝑏)) < 𝑧 → (abs‘((𝐹‘𝑎) − (𝐹‘𝑏))) < 𝑤)) → ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑏 ∈ 𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) |
46 | 24, 34, 45 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑏 ∈ 𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) |
47 | 46 | adantrr 753 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) →
∀𝑤 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑏 ∈ 𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) |
48 | | simprr 796 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) → 𝑤 ∈
ℝ+) |
49 | | rspa 2930 |
. . . . 5
⊢
((∀𝑤 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑏 ∈ 𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤) ∧ 𝑤 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ ∀𝑏 ∈ 𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) |
50 | 47, 48, 49 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) →
∃𝑧 ∈
ℝ+ ∀𝑏 ∈ 𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) |
51 | | simpl1l 1112 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) ∧ 𝑣 ∈ 𝐵) → 𝜑) |
52 | 51 | adantr 481 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → 𝜑) |
53 | | simp1rl 1126 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) → 𝑥 ∈ 𝐵) |
54 | 53 | ad2antrr 762 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → 𝑥 ∈ 𝐵) |
55 | | simplr 792 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → 𝑣 ∈ 𝐵) |
56 | 26 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐵 ∧ (𝐹‘(𝑥 − 𝑇)) ∈ ℂ) → (𝐺‘𝑥) = (𝐹‘(𝑥 − 𝑇))) |
57 | 5, 25, 56 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = (𝐹‘(𝑥 − 𝑇))) |
58 | 57 | 3adant3 1081 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝐺‘𝑥) = (𝐹‘(𝑥 − 𝑇))) |
59 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐵) → 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐹‘(𝑥 − 𝑇)))) |
60 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑣 → (𝑥 − 𝑇) = (𝑣 − 𝑇)) |
61 | 60 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑣 → (𝐹‘(𝑥 − 𝑇)) = (𝐹‘(𝑣 − 𝑇))) |
62 | 61 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 = 𝑣) → (𝐹‘(𝑥 − 𝑇)) = (𝐹‘(𝑣 − 𝑇))) |
63 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ 𝐵) |
64 | 3 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐵) → 𝐹:𝐴⟶ℂ) |
65 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑣 → (𝑥 ∈ 𝐵 ↔ 𝑣 ∈ 𝐵)) |
66 | 65 | anbi2d 740 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑣 → ((𝜑 ∧ 𝑥 ∈ 𝐵) ↔ (𝜑 ∧ 𝑣 ∈ 𝐵))) |
67 | 60 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑣 → ((𝑥 − 𝑇) ∈ 𝐴 ↔ (𝑣 − 𝑇) ∈ 𝐴)) |
68 | 66, 67 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 − 𝑇) ∈ 𝐴) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐵) → (𝑣 − 𝑇) ∈ 𝐴))) |
69 | 68, 24 | chvarv 2263 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐵) → (𝑣 − 𝑇) ∈ 𝐴) |
70 | 64, 69 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐵) → (𝐹‘(𝑣 − 𝑇)) ∈ ℂ) |
71 | 59, 62, 63, 70 | fvmptd 6288 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐵) → (𝐺‘𝑣) = (𝐹‘(𝑣 − 𝑇))) |
72 | 71 | 3adant2 1080 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝐺‘𝑣) = (𝐹‘(𝑣 − 𝑇))) |
73 | 58, 72 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → ((𝐺‘𝑥) − (𝐺‘𝑣)) = ((𝐹‘(𝑥 − 𝑇)) − (𝐹‘(𝑣 − 𝑇)))) |
74 | 73 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) = (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘(𝑣 − 𝑇))))) |
75 | 52, 54, 55, 74 | syl3anc 1326 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) = (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘(𝑣 − 𝑇))))) |
76 | 52, 54, 55 | jca31 557 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → ((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵)) |
77 | | simpr 477 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → (abs‘(𝑥 − 𝑣)) < 𝑧) |
78 | 9 | simpld 475 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ℂ) |
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) → 𝑥 ∈ ℂ) |
80 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑥 ∈ ℂ ∣
∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)} ⊆ ℂ |
81 | 6, 80 | eqsstri 3635 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐵 ⊆
ℂ |
82 | 81 | sseli 3599 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ 𝐵 → 𝑣 ∈ ℂ) |
83 | 82 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) → 𝑣 ∈ ℂ) |
84 | 15 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) → 𝑇 ∈ ℂ) |
85 | 79, 83, 84 | nnncan2d 10427 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) → ((𝑥 − 𝑇) − (𝑣 − 𝑇)) = (𝑥 − 𝑣)) |
86 | 85 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) → (abs‘((𝑥 − 𝑇) − (𝑣 − 𝑇))) = (abs‘(𝑥 − 𝑣))) |
87 | 86 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → (abs‘((𝑥 − 𝑇) − (𝑣 − 𝑇))) = (abs‘(𝑥 − 𝑣))) |
88 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → (abs‘(𝑥 − 𝑣)) < 𝑧) |
89 | 87, 88 | eqbrtrd 4675 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → (abs‘((𝑥 − 𝑇) − (𝑣 − 𝑇))) < 𝑧) |
90 | 76, 77, 89 | syl2anc 693 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → (abs‘((𝑥 − 𝑇) − (𝑣 − 𝑇))) < 𝑧) |
91 | 52, 55, 69 | syl2anc 693 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → (𝑣 − 𝑇) ∈ 𝐴) |
92 | | simpll3 1102 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → ∀𝑏 ∈ 𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) |
93 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑣 − 𝑇) → ((𝑥 − 𝑇) − 𝑏) = ((𝑥 − 𝑇) − (𝑣 − 𝑇))) |
94 | 93 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑣 − 𝑇) → (abs‘((𝑥 − 𝑇) − 𝑏)) = (abs‘((𝑥 − 𝑇) − (𝑣 − 𝑇)))) |
95 | 94 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑣 − 𝑇) → ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 ↔ (abs‘((𝑥 − 𝑇) − (𝑣 − 𝑇))) < 𝑧)) |
96 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑣 − 𝑇) → (𝐹‘𝑏) = (𝐹‘(𝑣 − 𝑇))) |
97 | 96 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑣 − 𝑇) → ((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏)) = ((𝐹‘(𝑥 − 𝑇)) − (𝐹‘(𝑣 − 𝑇)))) |
98 | 97 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑣 − 𝑇) → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) = (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘(𝑣 − 𝑇))))) |
99 | 98 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑣 − 𝑇) → ((abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤 ↔ (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘(𝑣 − 𝑇)))) < 𝑤)) |
100 | 95, 99 | imbi12d 334 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑣 − 𝑇) → (((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤) ↔ ((abs‘((𝑥 − 𝑇) − (𝑣 − 𝑇))) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘(𝑣 − 𝑇)))) < 𝑤))) |
101 | 100 | rspcva 3307 |
. . . . . . . . . . 11
⊢ (((𝑣 − 𝑇) ∈ 𝐴 ∧ ∀𝑏 ∈ 𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) → ((abs‘((𝑥 − 𝑇) − (𝑣 − 𝑇))) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘(𝑣 − 𝑇)))) < 𝑤)) |
102 | 91, 92, 101 | syl2anc 693 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → ((abs‘((𝑥 − 𝑇) − (𝑣 − 𝑇))) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘(𝑣 − 𝑇)))) < 𝑤)) |
103 | 90, 102 | mpd 15 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘(𝑣 − 𝑇)))) < 𝑤) |
104 | 75, 103 | eqbrtrd 4675 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) ∧ 𝑣 ∈ 𝐵) ∧ (abs‘(𝑥 − 𝑣)) < 𝑧) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤) |
105 | 104 | ex 450 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) ∧ 𝑣 ∈ 𝐵) → ((abs‘(𝑥 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤)) |
106 | 105 | ralrimiva 2966 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤)) → ∀𝑣 ∈ 𝐵 ((abs‘(𝑥 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤)) |
107 | 106 | 3exp 1264 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) → (𝑧 ∈ ℝ+
→ (∀𝑏 ∈
𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤) → ∀𝑣 ∈ 𝐵 ((abs‘(𝑥 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤)))) |
108 | 107 | reximdvai 3015 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) →
(∃𝑧 ∈
ℝ+ ∀𝑏 ∈ 𝐴 ((abs‘((𝑥 − 𝑇) − 𝑏)) < 𝑧 → (abs‘((𝐹‘(𝑥 − 𝑇)) − (𝐹‘𝑏))) < 𝑤) → ∃𝑧 ∈ ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑥 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤))) |
109 | 50, 108 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑤 ∈ ℝ+)) →
∃𝑧 ∈
ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑥 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤)) |
110 | 109 | ralrimivva 2971 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑣 ∈ 𝐵 ((abs‘(𝑥 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤)) |
111 | 81 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ ℂ) |
112 | | elcncf 22692 |
. . . 4
⊢ ((𝐵 ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝐺
∈ (𝐵–cn→ℂ) ↔ (𝐺:𝐵⟶ℂ ∧ ∀𝑎 ∈ 𝐵 ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑣 ∈ 𝐵 ((abs‘(𝑎 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) < 𝑤)))) |
113 | 111, 30, 112 | sylancl 694 |
. . 3
⊢ (𝜑 → (𝐺 ∈ (𝐵–cn→ℂ) ↔ (𝐺:𝐵⟶ℂ ∧ ∀𝑎 ∈ 𝐵 ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑣 ∈ 𝐵 ((abs‘(𝑎 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) < 𝑤)))) |
114 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑥ℝ+ |
115 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝐵 |
116 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(abs‘(𝑎 − 𝑣)) < 𝑧 |
117 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥abs |
118 | | nfmpt1 4747 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑥 ∈ 𝐵 ↦ (𝐹‘(𝑥 − 𝑇))) |
119 | 26, 118 | nfcxfr 2762 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝐺 |
120 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑎 |
121 | 119, 120 | nffv 6198 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝐺‘𝑎) |
122 | | nfcv 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥
− |
123 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑣 |
124 | 119, 123 | nffv 6198 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝐺‘𝑣) |
125 | 121, 122,
124 | nfov 6676 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((𝐺‘𝑎) − (𝐺‘𝑣)) |
126 | 117, 125 | nffv 6198 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) |
127 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥
< |
128 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑤 |
129 | 126, 127,
128 | nfbr 4699 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) < 𝑤 |
130 | 116, 129 | nfim 1825 |
. . . . . . . . 9
⊢
Ⅎ𝑥((abs‘(𝑎 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) < 𝑤) |
131 | 115, 130 | nfral 2945 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑣 ∈ 𝐵 ((abs‘(𝑎 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) < 𝑤) |
132 | 114, 131 | nfrex 3007 |
. . . . . . 7
⊢
Ⅎ𝑥∃𝑧 ∈ ℝ+
∀𝑣 ∈ 𝐵 ((abs‘(𝑎 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) < 𝑤) |
133 | 114, 132 | nfral 2945 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑣 ∈ 𝐵 ((abs‘(𝑎 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) < 𝑤) |
134 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑎∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑣 ∈ 𝐵 ((abs‘(𝑥 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤) |
135 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑥 → (𝑎 − 𝑣) = (𝑥 − 𝑣)) |
136 | 135 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → (abs‘(𝑎 − 𝑣)) = (abs‘(𝑥 − 𝑣))) |
137 | 136 | breq1d 4663 |
. . . . . . . . 9
⊢ (𝑎 = 𝑥 → ((abs‘(𝑎 − 𝑣)) < 𝑧 ↔ (abs‘(𝑥 − 𝑣)) < 𝑧)) |
138 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑥 → (𝐺‘𝑎) = (𝐺‘𝑥)) |
139 | 138 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑥 → ((𝐺‘𝑎) − (𝐺‘𝑣)) = ((𝐺‘𝑥) − (𝐺‘𝑣))) |
140 | 139 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → (abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) = (abs‘((𝐺‘𝑥) − (𝐺‘𝑣)))) |
141 | 140 | breq1d 4663 |
. . . . . . . . 9
⊢ (𝑎 = 𝑥 → ((abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) < 𝑤 ↔ (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤)) |
142 | 137, 141 | imbi12d 334 |
. . . . . . . 8
⊢ (𝑎 = 𝑥 → (((abs‘(𝑎 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) < 𝑤) ↔ ((abs‘(𝑥 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤))) |
143 | 142 | rexralbidv 3058 |
. . . . . . 7
⊢ (𝑎 = 𝑥 → (∃𝑧 ∈ ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑎 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) < 𝑤) ↔ ∃𝑧 ∈ ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑥 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤))) |
144 | 143 | ralbidv 2986 |
. . . . . 6
⊢ (𝑎 = 𝑥 → (∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑣 ∈ 𝐵 ((abs‘(𝑎 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) < 𝑤) ↔ ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑣 ∈ 𝐵 ((abs‘(𝑥 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤))) |
145 | 133, 134,
144 | cbvral 3167 |
. . . . 5
⊢
(∀𝑎 ∈
𝐵 ∀𝑤 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑎 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) < 𝑤) ↔ ∀𝑥 ∈ 𝐵 ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑣 ∈ 𝐵 ((abs‘(𝑥 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤)) |
146 | 145 | bicomi 214 |
. . . 4
⊢
(∀𝑥 ∈
𝐵 ∀𝑤 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑣 ∈ 𝐵 ((abs‘(𝑥 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤) ↔ ∀𝑎 ∈ 𝐵 ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑣 ∈ 𝐵 ((abs‘(𝑎 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) < 𝑤)) |
147 | 146 | anbi2i 730 |
. . 3
⊢ ((𝐺:𝐵⟶ℂ ∧ ∀𝑥 ∈ 𝐵 ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑣 ∈ 𝐵 ((abs‘(𝑥 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤)) ↔ (𝐺:𝐵⟶ℂ ∧ ∀𝑎 ∈ 𝐵 ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑣 ∈ 𝐵 ((abs‘(𝑎 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑎) − (𝐺‘𝑣))) < 𝑤))) |
148 | 113, 147 | syl6bbr 278 |
. 2
⊢ (𝜑 → (𝐺 ∈ (𝐵–cn→ℂ) ↔ (𝐺:𝐵⟶ℂ ∧ ∀𝑥 ∈ 𝐵 ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑣 ∈ 𝐵 ((abs‘(𝑥 − 𝑣)) < 𝑧 → (abs‘((𝐺‘𝑥) − (𝐺‘𝑣))) < 𝑤)))) |
149 | 27, 110, 148 | mpbir2and 957 |
1
⊢ (𝜑 → 𝐺 ∈ (𝐵–cn→ℂ)) |