| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ioossre 13449 | . . 3
⊢
(((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) ⊆ ℝ | 
| 2 |  | ioossre 13449 | . . 3
⊢
(((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷)) ⊆ ℝ | 
| 3 |  | xpinpreima2 33907 | . . . 4
⊢
(((((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) ⊆ ℝ ∧ (((2nd
‘𝑋) − 𝐷)(,)((2nd
‘𝑋) + 𝐷)) ⊆ ℝ) →
((((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) × (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))) = ((◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) ∩ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))))) | 
| 4 | 3 | eleq2d 2826 | . . 3
⊢
(((((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) ⊆ ℝ ∧ (((2nd
‘𝑋) − 𝐷)(,)((2nd
‘𝑋) + 𝐷)) ⊆ ℝ) →
(𝑌 ∈
((((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) × (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))) ↔ 𝑌 ∈ ((◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) ∩ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷)))))) | 
| 5 | 1, 2, 4 | mp2an 692 | . 2
⊢ (𝑌 ∈ ((((1st
‘𝑋) − 𝐷)(,)((1st
‘𝑋) + 𝐷)) × (((2nd
‘𝑋) − 𝐷)(,)((2nd
‘𝑋) + 𝐷))) ↔ 𝑌 ∈ ((◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) ∩ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))))) | 
| 6 |  | elin 3966 | . . 3
⊢ (𝑌 ∈ ((◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) ∩ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷)))) ↔ (𝑌 ∈ (◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) ∧ 𝑌 ∈ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))))) | 
| 7 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈
ℝ) | 
| 8 | 7 | recnd 11290 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈
ℂ) | 
| 9 |  | ax-icn 11215 | . . . . . . . . . . . 12
⊢ i ∈
ℂ | 
| 10 | 9 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → i ∈
ℂ) | 
| 11 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℝ) | 
| 12 | 11 | recnd 11290 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℂ) | 
| 13 | 10, 12 | mulcld 11282 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (i
· 𝑦) ∈
ℂ) | 
| 14 | 8, 13 | addcld 11281 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + (i · 𝑦)) ∈
ℂ) | 
| 15 |  | reval 15146 | . . . . . . . . 9
⊢ ((𝑥 + (i · 𝑦)) ∈ ℂ →
(ℜ‘(𝑥 + (i
· 𝑦))) = (((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦)))) / 2)) | 
| 16 | 14, 15 | syl 17 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(ℜ‘(𝑥 + (i
· 𝑦))) = (((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦)))) / 2)) | 
| 17 |  | crre 15154 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(ℜ‘(𝑥 + (i
· 𝑦))) = 𝑥) | 
| 18 | 16, 17 | eqtr3d 2778 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦)))) / 2) = 𝑥) | 
| 19 | 18 | mpoeq3ia 7512 | . . . . . 6
⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦)))) / 2)) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ 𝑥) | 
| 20 | 14 | adantl 481 | . . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 𝑦
∈ ℝ)) → (𝑥
+ (i · 𝑦)) ∈
ℂ) | 
| 21 |  | cnre2csqima.1 | . . . . . . . . 9
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) | 
| 22 | 21 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))) | 
| 23 |  | df-re 15140 | . . . . . . . . 9
⊢ ℜ =
(𝑧 ∈ ℂ ↦
((𝑧 + (∗‘𝑧)) / 2)) | 
| 24 | 23 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ ℜ = (𝑧 ∈
ℂ ↦ ((𝑧 +
(∗‘𝑧)) /
2))) | 
| 25 |  | id 22 | . . . . . . . . . 10
⊢ (𝑧 = (𝑥 + (i · 𝑦)) → 𝑧 = (𝑥 + (i · 𝑦))) | 
| 26 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑧 = (𝑥 + (i · 𝑦)) → (∗‘𝑧) = (∗‘(𝑥 + (i · 𝑦)))) | 
| 27 | 25, 26 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝑧 = (𝑥 + (i · 𝑦)) → (𝑧 + (∗‘𝑧)) = ((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦))))) | 
| 28 | 27 | oveq1d 7447 | . . . . . . . 8
⊢ (𝑧 = (𝑥 + (i · 𝑦)) → ((𝑧 + (∗‘𝑧)) / 2) = (((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦)))) / 2)) | 
| 29 | 20, 22, 24, 28 | fmpoco 8121 | . . . . . . 7
⊢ (⊤
→ (ℜ ∘ 𝐹) =
(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦)))) / 2))) | 
| 30 | 29 | mptru 1546 | . . . . . 6
⊢ (ℜ
∘ 𝐹) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (((𝑥 + (i · 𝑦)) + (∗‘(𝑥 + (i · 𝑦)))) / 2)) | 
| 31 |  | df1stres 32714 | . . . . . 6
⊢
(1st ↾ (ℝ × ℝ)) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ 𝑥) | 
| 32 | 19, 30, 31 | 3eqtr4ri 2775 | . . . . 5
⊢
(1st ↾ (ℝ × ℝ)) = (ℜ ∘
𝐹) | 
| 33 | 14 | rgen2 3198 | . . . . . 6
⊢
∀𝑥 ∈
ℝ ∀𝑦 ∈
ℝ (𝑥 + (i ·
𝑦)) ∈
ℂ | 
| 34 | 21 | fnmpo 8095 | . . . . . 6
⊢
(∀𝑥 ∈
ℝ ∀𝑦 ∈
ℝ (𝑥 + (i ·
𝑦)) ∈ ℂ →
𝐹 Fn (ℝ ×
ℝ)) | 
| 35 | 33, 34 | ax-mp 5 | . . . . 5
⊢ 𝐹 Fn (ℝ ×
ℝ) | 
| 36 |  | fo1st 8035 | . . . . . 6
⊢
1st :V–onto→V | 
| 37 |  | fofn 6821 | . . . . . 6
⊢
(1st :V–onto→V → 1st Fn V) | 
| 38 | 36, 37 | ax-mp 5 | . . . . 5
⊢
1st Fn V | 
| 39 |  | xp1st 8047 | . . . . 5
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (1st ‘𝑧) ∈ ℝ) | 
| 40 | 21 | rnmpo 7567 | . . . . . . . 8
⊢ ran 𝐹 = {𝑧 ∣ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = (𝑥 + (i · 𝑦))} | 
| 41 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 = (𝑥 + (i · 𝑦))) → 𝑧 = (𝑥 + (i · 𝑦))) | 
| 42 | 14 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 = (𝑥 + (i · 𝑦))) → (𝑥 + (i · 𝑦)) ∈ ℂ) | 
| 43 | 41, 42 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑧 = (𝑥 + (i · 𝑦))) → 𝑧 ∈ ℂ) | 
| 44 | 43 | ex 412 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧 = (𝑥 + (i · 𝑦)) → 𝑧 ∈ ℂ)) | 
| 45 | 44 | rexlimivv 3200 | . . . . . . . . 9
⊢
(∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ 𝑧 = (𝑥 + (i · 𝑦)) → 𝑧 ∈ ℂ) | 
| 46 | 45 | abssi 4069 | . . . . . . . 8
⊢ {𝑧 ∣ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑧 = (𝑥 + (i · 𝑦))} ⊆ ℂ | 
| 47 | 40, 46 | eqsstri 4029 | . . . . . . 7
⊢ ran 𝐹 ⊆
ℂ | 
| 48 |  | simpl 482 | . . . . . . 7
⊢ ((𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹) → 𝑧 ∈ ran 𝐹) | 
| 49 | 47, 48 | sselid 3980 | . . . . . 6
⊢ ((𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹) → 𝑧 ∈ ℂ) | 
| 50 |  | simpr 484 | . . . . . . 7
⊢ ((𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 ∈ ran 𝐹) | 
| 51 | 47, 50 | sselid 3980 | . . . . . 6
⊢ ((𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 ∈ ℂ) | 
| 52 | 49, 51 | resubd 15256 | . . . . 5
⊢ ((𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹) → (ℜ‘(𝑧 − 𝑢)) = ((ℜ‘𝑧) − (ℜ‘𝑢))) | 
| 53 | 32, 35, 38, 39, 52 | cnre2csqlem 33910 | . . . 4
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) → (abs‘(ℜ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷)) | 
| 54 |  | imval 15147 | . . . . . . . . 9
⊢ ((𝑥 + (i · 𝑦)) ∈ ℂ →
(ℑ‘(𝑥 + (i
· 𝑦))) =
(ℜ‘((𝑥 + (i
· 𝑦)) /
i))) | 
| 55 | 14, 54 | syl 17 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(ℑ‘(𝑥 + (i
· 𝑦))) =
(ℜ‘((𝑥 + (i
· 𝑦)) /
i))) | 
| 56 |  | crim 15155 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(ℑ‘(𝑥 + (i
· 𝑦))) = 𝑦) | 
| 57 | 55, 56 | eqtr3d 2778 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(ℜ‘((𝑥 + (i
· 𝑦)) / i)) = 𝑦) | 
| 58 | 57 | mpoeq3ia 7512 | . . . . . 6
⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
(ℜ‘((𝑥 + (i
· 𝑦)) / i))) =
(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ 𝑦) | 
| 59 |  | df-im 15141 | . . . . . . . . 9
⊢ ℑ =
(𝑧 ∈ ℂ ↦
(ℜ‘(𝑧 /
i))) | 
| 60 | 59 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ ℑ = (𝑧 ∈
ℂ ↦ (ℜ‘(𝑧 / i)))) | 
| 61 |  | fvoveq1 7455 | . . . . . . . 8
⊢ (𝑧 = (𝑥 + (i · 𝑦)) → (ℜ‘(𝑧 / i)) = (ℜ‘((𝑥 + (i · 𝑦)) / i))) | 
| 62 | 20, 22, 60, 61 | fmpoco 8121 | . . . . . . 7
⊢ (⊤
→ (ℑ ∘ 𝐹)
= (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
(ℜ‘((𝑥 + (i
· 𝑦)) /
i)))) | 
| 63 | 62 | mptru 1546 | . . . . . 6
⊢ (ℑ
∘ 𝐹) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
(ℜ‘((𝑥 + (i
· 𝑦)) /
i))) | 
| 64 |  | df2ndres 32715 | . . . . . 6
⊢
(2nd ↾ (ℝ × ℝ)) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ 𝑦) | 
| 65 | 58, 63, 64 | 3eqtr4ri 2775 | . . . . 5
⊢
(2nd ↾ (ℝ × ℝ)) = (ℑ ∘
𝐹) | 
| 66 |  | fo2nd 8036 | . . . . . 6
⊢
2nd :V–onto→V | 
| 67 |  | fofn 6821 | . . . . . 6
⊢
(2nd :V–onto→V → 2nd Fn V) | 
| 68 | 66, 67 | ax-mp 5 | . . . . 5
⊢
2nd Fn V | 
| 69 |  | xp2nd 8048 | . . . . 5
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (2nd ‘𝑧) ∈ ℝ) | 
| 70 | 49, 51 | imsubd 15257 | . . . . 5
⊢ ((𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹) → (ℑ‘(𝑧 − 𝑢)) = ((ℑ‘𝑧) − (ℑ‘𝑢))) | 
| 71 | 65, 35, 68, 69, 70 | cnre2csqlem 33910 | . . . 4
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))) → (abs‘(ℑ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷)) | 
| 72 | 53, 71 | anim12d 609 | . . 3
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → ((𝑌 ∈ (◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) ∧ 𝑌 ∈ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷)))) →
((abs‘(ℜ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷 ∧ (abs‘(ℑ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷))) | 
| 73 | 6, 72 | biimtrid 242 | . 2
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ ((◡(1st ↾ (ℝ ×
ℝ)) “ (((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷))) ∩ (◡(2nd ↾ (ℝ ×
ℝ)) “ (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷)))) →
((abs‘(ℜ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷 ∧ (abs‘(ℑ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷))) | 
| 74 | 5, 73 | biimtrid 242 | 1
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝑌 ∈
(ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ ((((1st
‘𝑋) − 𝐷)(,)((1st
‘𝑋) + 𝐷)) × (((2nd
‘𝑋) − 𝐷)(,)((2nd
‘𝑋) + 𝐷))) →
((abs‘(ℜ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷 ∧ (abs‘(ℑ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷))) |