cnre2csqima

Description: Image of a centered square by the canonical bijection from ( RR X. RR ) to CC . (Contributed by Thierry Arnoux, 27-Sep-2017)

		Ref	Expression
	Hypothesis	cnre2csqima.1	⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
	Assertion	cnre2csqima	⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑌 ∈ ( ℝ × ℝ ) ∧ 𝐷 ∈ ℝ⁺ ) → ( 𝑌 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) × ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ) → ( ( abs ‘ ( ℜ ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ) ) < 𝐷 ∧ ( abs ‘ ( ℑ ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ) ) < 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnre2csqima.1	⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) )
2		ioossre	⊢ ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) ⊆ ℝ
3		ioossre	⊢ ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ⊆ ℝ
4		xpinpreima2	⊢ ( ( ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) ⊆ ℝ ∧ ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ⊆ ℝ ) → ( ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) × ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ) = ( ( ^◡ ( 1^st ↾ ( ℝ × ℝ ) ) “ ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) ) ∩ ( ^◡ ( 2^nd ↾ ( ℝ × ℝ ) ) “ ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ) ) )
5	4	eleq2d	⊢ ( ( ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) ⊆ ℝ ∧ ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ⊆ ℝ ) → ( 𝑌 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) × ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ) ↔ 𝑌 ∈ ( ( ^◡ ( 1^st ↾ ( ℝ × ℝ ) ) “ ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) ) ∩ ( ^◡ ( 2^nd ↾ ( ℝ × ℝ ) ) “ ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ) ) ) )
6	2 3 5	mp2an	⊢ ( 𝑌 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) × ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ) ↔ 𝑌 ∈ ( ( ^◡ ( 1^st ↾ ( ℝ × ℝ ) ) “ ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) ) ∩ ( ^◡ ( 2^nd ↾ ( ℝ × ℝ ) ) “ ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ) ) )
7		elin	⊢ ( 𝑌 ∈ ( ( ^◡ ( 1^st ↾ ( ℝ × ℝ ) ) “ ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) ) ∩ ( ^◡ ( 2^nd ↾ ( ℝ × ℝ ) ) “ ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ) ) ↔ ( 𝑌 ∈ ( ^◡ ( 1^st ↾ ( ℝ × ℝ ) ) “ ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) ) ∧ 𝑌 ∈ ( ^◡ ( 2^nd ↾ ( ℝ × ℝ ) ) “ ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ) ) )
8		simpl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℝ )
9	8	recnd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℂ )
10		ax-icn	⊢ i ∈ ℂ
11	10	a1i	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → i ∈ ℂ )
12		simpr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
13	12	recnd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
14	11 13	mulcld	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( i · 𝑦 ) ∈ ℂ )
15	9 14	addcld	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + ( i · 𝑦 ) ) ∈ ℂ )
16		reval	⊢ ( ( 𝑥 + ( i · 𝑦 ) ) ∈ ℂ → ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = ( ( ( 𝑥 + ( i · 𝑦 ) ) + ( ∗ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ) / 2 ) )
17	15 16	syl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = ( ( ( 𝑥 + ( i · 𝑦 ) ) + ( ∗ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ) / 2 ) )
18		crre	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = 𝑥 )
19	17 18	eqtr3d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 + ( i · 𝑦 ) ) + ( ∗ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ) / 2 ) = 𝑥 )
20	19	mpoeq3ia	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( ( ( 𝑥 + ( i · 𝑦 ) ) + ( ∗ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ) / 2 ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ 𝑥 )
21	15	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 + ( i · 𝑦 ) ) ∈ ℂ )
22	1	a1i	⊢ ( ⊤ → 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( 𝑥 + ( i · 𝑦 ) ) ) )
23		df-re	⊢ ℜ = ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 + ( ∗ ‘ 𝑧 ) ) / 2 ) )
24	23	a1i	⊢ ( ⊤ → ℜ = ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 + ( ∗ ‘ 𝑧 ) ) / 2 ) ) )
25		id	⊢ ( 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) → 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) )
26		fveq2	⊢ ( 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) → ( ∗ ‘ 𝑧 ) = ( ∗ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) )
27	25 26	oveq12d	⊢ ( 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) → ( 𝑧 + ( ∗ ‘ 𝑧 ) ) = ( ( 𝑥 + ( i · 𝑦 ) ) + ( ∗ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ) )
28	27	oveq1d	⊢ ( 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( 𝑧 + ( ∗ ‘ 𝑧 ) ) / 2 ) = ( ( ( 𝑥 + ( i · 𝑦 ) ) + ( ∗ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ) / 2 ) )
29	21 22 24 28	fmpoco	⊢ ( ⊤ → ( ℜ ∘ 𝐹 ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( ( ( 𝑥 + ( i · 𝑦 ) ) + ( ∗ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ) / 2 ) ) )
30	29	mptru	⊢ ( ℜ ∘ 𝐹 ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( ( ( 𝑥 + ( i · 𝑦 ) ) + ( ∗ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ) / 2 ) )
31		df1stres	⊢ ( 1^st ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ 𝑥 )
32	20 30 31	3eqtr4ri	⊢ ( 1^st ↾ ( ℝ × ℝ ) ) = ( ℜ ∘ 𝐹 )
33	15	rgen2	⊢ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑥 + ( i · 𝑦 ) ) ∈ ℂ
34	1	fnmpo	⊢ ( ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑥 + ( i · 𝑦 ) ) ∈ ℂ → 𝐹 Fn ( ℝ × ℝ ) )
35	33 34	ax-mp	⊢ 𝐹 Fn ( ℝ × ℝ )
36		fo1st	⊢ 1^st : V –onto→ V
37		fofn	⊢ ( 1^st : V –onto→ V → 1^st Fn V )
38	36 37	ax-mp	⊢ 1^st Fn V
39		xp1st	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 1^st ‘ 𝑧 ) ∈ ℝ )
40	1	rnmpo	⊢ ran 𝐹 = { 𝑧 ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) }
41		simpr	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) ) → 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) )
42	15	adantr	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) ) → ( 𝑥 + ( i · 𝑦 ) ) ∈ ℂ )
43	41 42	eqeltrd	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) ) → 𝑧 ∈ ℂ )
44	43	ex	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) → 𝑧 ∈ ℂ ) )
45	44	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) → 𝑧 ∈ ℂ )
46	45	abssi	⊢ { 𝑧 ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) } ⊆ ℂ
47	40 46	eqsstri	⊢ ran 𝐹 ⊆ ℂ
48		simpl	⊢ ( ( 𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹 ) → 𝑧 ∈ ran 𝐹 )
49	47 48	sselid	⊢ ( ( 𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹 ) → 𝑧 ∈ ℂ )
50		simpr	⊢ ( ( 𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹 ) → 𝑢 ∈ ran 𝐹 )
51	47 50	sselid	⊢ ( ( 𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹 ) → 𝑢 ∈ ℂ )
52	49 51	resubd	⊢ ( ( 𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹 ) → ( ℜ ‘ ( 𝑧 − 𝑢 ) ) = ( ( ℜ ‘ 𝑧 ) − ( ℜ ‘ 𝑢 ) ) )
53	32 35 38 39 52	cnre2csqlem	⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑌 ∈ ( ℝ × ℝ ) ∧ 𝐷 ∈ ℝ⁺ ) → ( 𝑌 ∈ ( ^◡ ( 1^st ↾ ( ℝ × ℝ ) ) “ ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) ) → ( abs ‘ ( ℜ ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ) ) < 𝐷 ) )
54		imval	⊢ ( ( 𝑥 + ( i · 𝑦 ) ) ∈ ℂ → ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = ( ℜ ‘ ( ( 𝑥 + ( i · 𝑦 ) ) / i ) ) )
55	15 54	syl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = ( ℜ ‘ ( ( 𝑥 + ( i · 𝑦 ) ) / i ) ) )
56		crim	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = 𝑦 )
57	55 56	eqtr3d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ℜ ‘ ( ( 𝑥 + ( i · 𝑦 ) ) / i ) ) = 𝑦 )
58	57	mpoeq3ia	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( ℜ ‘ ( ( 𝑥 + ( i · 𝑦 ) ) / i ) ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ 𝑦 )
59		df-im	⊢ ℑ = ( 𝑧 ∈ ℂ ↦ ( ℜ ‘ ( 𝑧 / i ) ) )
60	59	a1i	⊢ ( ⊤ → ℑ = ( 𝑧 ∈ ℂ ↦ ( ℜ ‘ ( 𝑧 / i ) ) ) )
61		fvoveq1	⊢ ( 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) → ( ℜ ‘ ( 𝑧 / i ) ) = ( ℜ ‘ ( ( 𝑥 + ( i · 𝑦 ) ) / i ) ) )
62	21 22 60 61	fmpoco	⊢ ( ⊤ → ( ℑ ∘ 𝐹 ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( ℜ ‘ ( ( 𝑥 + ( i · 𝑦 ) ) / i ) ) ) )
63	62	mptru	⊢ ( ℑ ∘ 𝐹 ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ( ℜ ‘ ( ( 𝑥 + ( i · 𝑦 ) ) / i ) ) )
64		df2ndres	⊢ ( 2^nd ↾ ( ℝ × ℝ ) ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ 𝑦 )
65	58 63 64	3eqtr4ri	⊢ ( 2^nd ↾ ( ℝ × ℝ ) ) = ( ℑ ∘ 𝐹 )
66		fo2nd	⊢ 2^nd : V –onto→ V
67		fofn	⊢ ( 2^nd : V –onto→ V → 2^nd Fn V )
68	66 67	ax-mp	⊢ 2^nd Fn V
69		xp2nd	⊢ ( 𝑧 ∈ ( ℝ × ℝ ) → ( 2^nd ‘ 𝑧 ) ∈ ℝ )
70	49 51	imsubd	⊢ ( ( 𝑧 ∈ ran 𝐹 ∧ 𝑢 ∈ ran 𝐹 ) → ( ℑ ‘ ( 𝑧 − 𝑢 ) ) = ( ( ℑ ‘ 𝑧 ) − ( ℑ ‘ 𝑢 ) ) )
71	65 35 68 69 70	cnre2csqlem	⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑌 ∈ ( ℝ × ℝ ) ∧ 𝐷 ∈ ℝ⁺ ) → ( 𝑌 ∈ ( ^◡ ( 2^nd ↾ ( ℝ × ℝ ) ) “ ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ) → ( abs ‘ ( ℑ ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ) ) < 𝐷 ) )
72	53 71	anim12d	⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑌 ∈ ( ℝ × ℝ ) ∧ 𝐷 ∈ ℝ⁺ ) → ( ( 𝑌 ∈ ( ^◡ ( 1^st ↾ ( ℝ × ℝ ) ) “ ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) ) ∧ 𝑌 ∈ ( ^◡ ( 2^nd ↾ ( ℝ × ℝ ) ) “ ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ) ) → ( ( abs ‘ ( ℜ ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ) ) < 𝐷 ∧ ( abs ‘ ( ℑ ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ) ) < 𝐷 ) ) )
73	7 72	syl5bi	⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑌 ∈ ( ℝ × ℝ ) ∧ 𝐷 ∈ ℝ⁺ ) → ( 𝑌 ∈ ( ( ^◡ ( 1^st ↾ ( ℝ × ℝ ) ) “ ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) ) ∩ ( ^◡ ( 2^nd ↾ ( ℝ × ℝ ) ) “ ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ) ) → ( ( abs ‘ ( ℜ ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ) ) < 𝐷 ∧ ( abs ‘ ( ℑ ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ) ) < 𝐷 ) ) )
74	6 73	syl5bi	⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑌 ∈ ( ℝ × ℝ ) ∧ 𝐷 ∈ ℝ⁺ ) → ( 𝑌 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − 𝐷 ) (,) ( ( 1^st ‘ 𝑋 ) + 𝐷 ) ) × ( ( ( 2^nd ‘ 𝑋 ) − 𝐷 ) (,) ( ( 2^nd ‘ 𝑋 ) + 𝐷 ) ) ) → ( ( abs ‘ ( ℜ ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ) ) < 𝐷 ∧ ( abs ‘ ( ℑ ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑋 ) ) ) ) < 𝐷 ) ) )

Metamath Proof Explorer

Theorem cnre2csqima

Proof