Step | Hyp | Ref
| Expression |
1 | | ioossre 13140 |
. . 3
⊢
(((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) ⊆ ℝ |
2 | | ioossre 13140 |
. . 3
⊢
(((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷)) ⊆ ℝ |
3 | | xpinpreima2 31857 |
. . . 4
⊢
(((((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) ⊆ ℝ ∧ (((2nd
‘𝑋) − 𝐷)(,)((2nd
‘𝑋) + 𝐷)) ⊆ ℝ) →
((((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) × (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))) = ((◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) ∩ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))))) |
4 | 3 | eleq2d 2824 |
. . 3
⊢
(((((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) ⊆ ℝ ∧ (((2nd
‘𝑋) − 𝐷)(,)((2nd
‘𝑋) + 𝐷)) ⊆ ℝ) →
(𝑌 ∈
((((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) × (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))) ↔ 𝑌 ∈ ((◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) ∩ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷)))))) |
5 | 1, 2, 4 | mp2an 689 |
. 2
⊢ (𝑌 ∈ ((((1st
‘𝑋) − 𝐷)(,)((1st
‘𝑋) + 𝐷)) × (((2nd
‘𝑋) − 𝐷)(,)((2nd
‘𝑋) + 𝐷))) ↔ 𝑌 ∈ ((◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) ∩ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))))) |
6 | | elin 3903 |
. . 3
⊢ (𝑌 ∈ ((◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) ∩ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷)))) ↔ (𝑌 ∈ (◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) ∧ 𝑌 ∈ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))))) |
7 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈
ℝ) |
8 | 7 | recnd 11003 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈
ℂ) |
9 | | ax-icn 10930 |
. . . . . . . . . . . 12
⊢ i ∈
ℂ |
10 | 9 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → i ∈
ℂ) |
11 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℝ) |
12 | 11 | recnd 11003 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℂ) |
13 | 10, 12 | mulcld 10995 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (i
· 𝑦) ∈
ℂ) |
14 | 8, 13 | addcld 10994 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + (i · 𝑦)) ∈
ℂ) |
15 | | reval 14817 |
. . . . . . . . 9
⊢ ((𝑥 + (i · 𝑦)) ∈ ℂ →
(ℜ‘(𝑥 + (i
· 𝑦))) = (((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦)))) / 2)) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(ℜ‘(𝑥 + (i
· 𝑦))) = (((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦)))) / 2)) |
17 | | crre 14825 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(ℜ‘(𝑥 + (i
· 𝑦))) = 𝑥) |
18 | 16, 17 | eqtr3d 2780 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦)))) / 2) = 𝑥) |
19 | 18 | mpoeq3ia 7353 |
. . . . . 6
⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦)))) / 2)) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ 𝑥) |
20 | 14 | adantl 482 |
. . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 𝑦
∈ ℝ)) → (𝑥
+ (i · 𝑦)) ∈
ℂ) |
21 | | cnre2csqima.1 |
. . . . . . . . 9
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) |
22 | 21 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))) |
23 | | df-re 14811 |
. . . . . . . . 9
⊢ ℜ =
(𝑧 ∈ ℂ ↦
((𝑧 + (∗‘𝑧)) / 2)) |
24 | 23 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ ℜ = (𝑧 ∈
ℂ ↦ ((𝑧 +
(∗‘𝑧)) /
2))) |
25 | | id 22 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑥 + (i · 𝑦)) → 𝑧 = (𝑥 + (i · 𝑦))) |
26 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑥 + (i · 𝑦)) → (∗‘𝑧) = (∗‘(𝑥 + (i · 𝑦)))) |
27 | 25, 26 | oveq12d 7293 |
. . . . . . . . 9
⊢ (𝑧 = (𝑥 + (i · 𝑦)) → (𝑧 + (∗‘𝑧)) = ((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦))))) |
28 | 27 | oveq1d 7290 |
. . . . . . . 8
⊢ (𝑧 = (𝑥 + (i · 𝑦)) → ((𝑧 + (∗‘𝑧)) / 2) = (((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦)))) / 2)) |
29 | 20, 22, 24, 28 | fmpoco 7935 |
. . . . . . 7
⊢ (⊤
→ (ℜ ∘ 𝐹) =
(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦)))) / 2))) |
30 | 29 | mptru 1546 |
. . . . . 6
⊢ (ℜ
∘ 𝐹) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦)))) / 2)) |
31 | | df1stres 31036 |
. . . . . 6
⊢
(1st ↾ (ℝ × ℝ)) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ 𝑥) |
32 | 19, 30, 31 | 3eqtr4ri 2777 |
. . . . 5
⊢
(1st ↾ (ℝ × ℝ)) = (ℜ ∘
𝐹) |
33 | 14 | rgen2 3120 |
. . . . . 6
⊢
∀𝑥 ∈
ℝ ∀𝑦 ∈
ℝ (𝑥 + (i ·
𝑦)) ∈
ℂ |
34 | 21 | fnmpo 7909 |
. . . . . 6
⊢
(∀𝑥 ∈
ℝ ∀𝑦 ∈
ℝ (𝑥 + (i ·
𝑦)) ∈ ℂ →
𝐹 Fn (ℝ ×
ℝ)) |
35 | 33, 34 | ax-mp 5 |
. . . . 5
⊢ 𝐹 Fn (ℝ ×
ℝ) |
36 | | fo1st 7851 |
. . . . . 6
⊢
1st :V–onto→V |
37 | | fofn 6690 |
. . . . . 6
⊢
(1st :V–onto→V → 1st Fn V) |
38 | 36, 37 | ax-mp 5 |
. . . . 5
⊢
1st Fn V |
39 | | xp1st 7863 |
. . . . 5
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (1st ‘𝑧) ∈ ℝ) |
40 | 21 | rnmpo 7407 |
. . . . . . . 8
⊢ ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = (𝑥 + (i · 𝑦))} |
41 | | simpr 485 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 = (𝑥 + (i · 𝑦))) → 𝑧 = (𝑥 + (i · 𝑦))) |
42 | 14 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 = (𝑥 + (i · 𝑦))) → (𝑥 + (i · 𝑦)) ∈ ℂ) |
43 | 41, 42 | eqeltrd 2839 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 = (𝑥 + (i · 𝑦))) → 𝑧 ∈ ℂ) |
44 | 43 | ex 413 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧 = (𝑥 + (i · 𝑦)) → 𝑧 ∈ ℂ)) |
45 | 44 | rexlimivv 3221 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ 𝑧 = (𝑥 + (i · 𝑦)) → 𝑧 ∈ ℂ) |
46 | 45 | abssi 4003 |
. . . . . . . 8
⊢ {𝑧 ∣ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = (𝑥 + (i · 𝑦))} ⊆ ℂ |
47 | 40, 46 | eqsstri 3955 |
. . . . . . 7
⊢ ran 𝐹 ⊆
ℂ |
48 | | simpl 483 |
. . . . . . 7
⊢ ((𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹) → 𝑧 ∈ ran 𝐹) |
49 | 47, 48 | sselid 3919 |
. . . . . 6
⊢ ((𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹) → 𝑧 ∈ ℂ) |
50 | | simpr 485 |
. . . . . . 7
⊢ ((𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 ∈ ran 𝐹) |
51 | 47, 50 | sselid 3919 |
. . . . . 6
⊢ ((𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 ∈ ℂ) |
52 | 49, 51 | resubd 14927 |
. . . . 5
⊢ ((𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹) → (ℜ‘(𝑧 − 𝑢)) = ((ℜ‘𝑧) − (ℜ‘𝑢))) |
53 | 32, 35, 38, 39, 52 | cnre2csqlem 31860 |
. . . 4
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) → (abs‘(ℜ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷)) |
54 | | imval 14818 |
. . . . . . . . 9
⊢ ((𝑥 + (i · 𝑦)) ∈ ℂ →
(ℑ‘(𝑥 + (i
· 𝑦))) =
(ℜ‘((𝑥 + (i
· 𝑦)) /
i))) |
55 | 14, 54 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(ℑ‘(𝑥 + (i
· 𝑦))) =
(ℜ‘((𝑥 + (i
· 𝑦)) /
i))) |
56 | | crim 14826 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(ℑ‘(𝑥 + (i
· 𝑦))) = 𝑦) |
57 | 55, 56 | eqtr3d 2780 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(ℜ‘((𝑥 + (i
· 𝑦)) / i)) = 𝑦) |
58 | 57 | mpoeq3ia 7353 |
. . . . . 6
⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
(ℜ‘((𝑥 + (i
· 𝑦)) / i))) =
(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ 𝑦) |
59 | | df-im 14812 |
. . . . . . . . 9
⊢ ℑ =
(𝑧 ∈ ℂ ↦
(ℜ‘(𝑧 /
i))) |
60 | 59 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ ℑ = (𝑧 ∈
ℂ ↦ (ℜ‘(𝑧 / i)))) |
61 | | fvoveq1 7298 |
. . . . . . . 8
⊢ (𝑧 = (𝑥 + (i · 𝑦)) → (ℜ‘(𝑧 / i)) = (ℜ‘((𝑥 + (i · 𝑦)) / i))) |
62 | 20, 22, 60, 61 | fmpoco 7935 |
. . . . . . 7
⊢ (⊤
→ (ℑ ∘ 𝐹)
= (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
(ℜ‘((𝑥 + (i
· 𝑦)) /
i)))) |
63 | 62 | mptru 1546 |
. . . . . 6
⊢ (ℑ
∘ 𝐹) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
(ℜ‘((𝑥 + (i
· 𝑦)) /
i))) |
64 | | df2ndres 31037 |
. . . . . 6
⊢
(2nd ↾ (ℝ × ℝ)) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ 𝑦) |
65 | 58, 63, 64 | 3eqtr4ri 2777 |
. . . . 5
⊢
(2nd ↾ (ℝ × ℝ)) = (ℑ ∘
𝐹) |
66 | | fo2nd 7852 |
. . . . . 6
⊢
2nd :V–onto→V |
67 | | fofn 6690 |
. . . . . 6
⊢
(2nd :V–onto→V → 2nd Fn V) |
68 | 66, 67 | ax-mp 5 |
. . . . 5
⊢
2nd Fn V |
69 | | xp2nd 7864 |
. . . . 5
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (2nd ‘𝑧) ∈ ℝ) |
70 | 49, 51 | imsubd 14928 |
. . . . 5
⊢ ((𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹) → (ℑ‘(𝑧 − 𝑢)) = ((ℑ‘𝑧) − (ℑ‘𝑢))) |
71 | 65, 35, 68, 69, 70 | cnre2csqlem 31860 |
. . . 4
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))) → (abs‘(ℑ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷)) |
72 | 53, 71 | anim12d 609 |
. . 3
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → ((𝑌 ∈ (◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) ∧ 𝑌 ∈ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷)))) →
((abs‘(ℜ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷 ∧ (abs‘(ℑ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷))) |
73 | 6, 72 | syl5bi 241 |
. 2
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ ((◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) ∩ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷)))) →
((abs‘(ℜ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷 ∧ (abs‘(ℑ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷))) |
74 | 5, 73 | syl5bi 241 |
1
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ ((((1st
‘𝑋) − 𝐷)(,)((1st
‘𝑋) + 𝐷)) × (((2nd
‘𝑋) − 𝐷)(,)((2nd
‘𝑋) + 𝐷))) →
((abs‘(ℜ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷 ∧ (abs‘(ℑ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷))) |