Theorem mullimc

Description: Limit of the product of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	mullimc.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	mullimc.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
	mullimc.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) )
	mullimc.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	mullimc.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
	mullimc.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 limℂ 𝐷 ) )
	mullimc.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐺 limℂ 𝐷 ) )
Assertion	mullimc	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ ( 𝐻 limℂ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		mullimc.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		mullimc.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
3		mullimc.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) )
4		mullimc.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
5		mullimc.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
6		mullimc.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 limℂ 𝐷 ) )
7		mullimc.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐺 limℂ 𝐷 ) )
8		limccl	⊢ ( 𝐹 limℂ 𝐷 ) ⊆ ℂ
9	8 6	sselid	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
10		limccl	⊢ ( 𝐺 limℂ 𝐷 ) ⊆ ℂ
11	10 7	sselid	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
12	9 11	mulcld	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ ℂ )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ∈ ℝ+ )
14	9	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → 𝑋 ∈ ℂ )
15	11	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → 𝑌 ∈ ℂ )
16		mulcn2	⊢ ( ( 𝑤 ∈ ℝ+ ∧ 𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ∃ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) )
17	13 14 15 16	syl3anc	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) )
18	4 1	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
19	1 4	dmmptd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
20		limcrcl	⊢ ( 𝑋 ∈ ( 𝐹 limℂ 𝐷 ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ ) )
21	6 20	syl	⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ ) )
22	21	simp2d	⊢ ( 𝜑 → dom 𝐹 ⊆ ℂ )
23	19 22	eqsstrrd	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
24	21	simp3d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
25	18 23 24	ellimc3	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 limℂ 𝐷 ) ↔ ( 𝑋 ∈ ℂ ∧ ∀ 𝑎 ∈ ℝ+ ∃ 𝑒 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ) )
26	6 25	mpbid	⊢ ( 𝜑 → ( 𝑋 ∈ ℂ ∧ ∀ 𝑎 ∈ ℝ+ ∃ 𝑒 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) )
27	26	simprd	⊢ ( 𝜑 → ∀ 𝑎 ∈ ℝ+ ∃ 𝑒 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) )
28	27	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) → ∃ 𝑒 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) )
29	28	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ∃ 𝑒 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) )
30	5 2	fmptd	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℂ )
31	30 23 24	ellimc3	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐺 limℂ 𝐷 ) ↔ ( 𝑌 ∈ ℂ ∧ ∀ 𝑏 ∈ ℝ+ ∃ 𝑓 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) )
32	7 31	mpbid	⊢ ( 𝜑 → ( 𝑌 ∈ ℂ ∧ ∀ 𝑏 ∈ ℝ+ ∃ 𝑓 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) )
33	32	simprd	⊢ ( 𝜑 → ∀ 𝑏 ∈ ℝ+ ∃ 𝑓 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) )
34	33	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ℝ+ ) → ∃ 𝑓 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) )
35	34	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ∃ 𝑓 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) )
36		reeanv	⊢ ( ∃ 𝑒 ∈ ℝ+ ∃ 𝑓 ∈ ℝ+ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ↔ ( ∃ 𝑒 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∃ 𝑓 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) )
37	29 35 36	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ∃ 𝑒 ∈ ℝ+ ∃ 𝑓 ∈ ℝ+ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) )
38		ifcl	⊢ ( ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) → if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ∈ ℝ+ )
39	38	3ad2ant2	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ∈ ℝ+ )
40		nfv	⊢ Ⅎ 𝑧 ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) )
41		nfv	⊢ Ⅎ 𝑧 ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ )
42		nfra1	⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 )
43		nfra1	⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 )
44	42 43	nfan	⊢ Ⅎ 𝑧 ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) )
45	40 41 44	nf3an	⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) )
46		simp11l	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝜑 )
47		simp1rl	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → 𝑎 ∈ ℝ+ )
48	47	3ad2ant1	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝑎 ∈ ℝ+ )
49	46 48	jca	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) )
50		simp12	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) )
51		simp13l	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) )
52	49 50 51	jca31	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) )
53		simp1r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) )
54		simp2	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝑧 ∈ 𝐴 )
55		simp3l	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝑧 ≠ 𝐷 )
56		simplll	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) → 𝜑 )
57	56	3ad2ant1	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝜑 )
58		simp1lr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) )
59		simp3r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) )
60		simp1l	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → 𝜑 )
61		simp2	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → 𝑧 ∈ 𝐴 )
62	23	sselda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℂ )
63	60 61 62	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → 𝑧 ∈ ℂ )
64	60 24	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → 𝐷 ∈ ℂ )
65	63 64	subcld	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( 𝑧 − 𝐷 ) ∈ ℂ )
66	65	abscld	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) ∈ ℝ )
67		rpre	⊢ ( 𝑒 ∈ ℝ+ → 𝑒 ∈ ℝ )
68	67	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) → 𝑒 ∈ ℝ )
69	68	3ad2ant1	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → 𝑒 ∈ ℝ )
70		rpre	⊢ ( 𝑓 ∈ ℝ+ → 𝑓 ∈ ℝ )
71	70	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) → 𝑓 ∈ ℝ )
72	71	3ad2ant1	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → 𝑓 ∈ ℝ )
73	69 72	ifcld	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ∈ ℝ )
74		simp3	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) )
75		min1	⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ≤ 𝑒 )
76	69 72 75	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ≤ 𝑒 )
77	66 73 69 74 76	ltletrd	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 )
78	57 58 54 59 77	syl211anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 )
79	55 78	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) )
80		rsp	⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) )
81	53 54 79 80	syl3c	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 )
82	52 81	syld3an1	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 )
83		simp1l	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → 𝜑 )
84	83 47	jca	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) )
85		simp2	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) )
86		simp3r	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) )
87	84 85 86	jca31	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) )
88		simp1r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) )
89		simp2	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝑧 ∈ 𝐴 )
90		simp3l	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝑧 ≠ 𝐷 )
91		simplll	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) → 𝜑 )
92	91	3ad2ant1	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → 𝜑 )
93		simp1lr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) )
94		simp3r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) )
95		min2	⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ≤ 𝑓 )
96	69 72 95	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ≤ 𝑓 )
97	66 73 72 74 96	ltletrd	⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 )
98	92 93 89 94 97	syl211anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 )
99	90 98	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) )
100		rsp	⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) )
101	88 89 99 100	syl3c	⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 )
102	87 101	syl3an1	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 )
103	82 102	jca	⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) )
104	103	3exp	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) )
105	45 104	ralrimi	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) )
106		brimralrspcev	⊢ ( ( if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ∈ ℝ+ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < if ( 𝑒 ≤ 𝑓 , 𝑒 , 𝑓 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) )
107	39 105 106	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) )
108	107	3exp	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ( ( 𝑒 ∈ ℝ+ ∧ 𝑓 ∈ ℝ+ ) → ( ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ) )
109	108	rexlimdvv	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ( ∃ 𝑒 ∈ ℝ+ ∃ 𝑓 ∈ ℝ+ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑓 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) )
110	37 109	mpd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) )
111	110	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) )
112	111	3adant3	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) )
113		nfv	⊢ Ⅎ 𝑧 ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ )
114		nfra1	⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) )
115	113 114	nfan	⊢ Ⅎ 𝑧 ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) )
116		simp1l	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) → 𝜑 )
117	116	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → 𝜑 )
118	117	3ad2ant1	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → 𝜑 )
119		simp2	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → 𝑧 ∈ 𝐴 )
120		nfv	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑧 ∈ 𝐴 )
121		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 · 𝐶 ) )
122	3 121	nfcxfr	⊢ Ⅎ 𝑥 𝐻
123		nfcv	⊢ Ⅎ 𝑥 𝑧
124	122 123	nffv	⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑧 )
125		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
126	1 125	nfcxfr	⊢ Ⅎ 𝑥 𝐹
127	126 123	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 )
128		nfcv	⊢ Ⅎ 𝑥 ·
129		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
130	2 129	nfcxfr	⊢ Ⅎ 𝑥 𝐺
131	130 123	nffv	⊢ Ⅎ 𝑥 ( 𝐺 ‘ 𝑧 )
132	127 128 131	nfov	⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) )
133	124 132	nfeq	⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) )
134	120 133	nfim	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) )
135		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
136	135	anbi2d	⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ) )
137		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑧 ) )
138		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
139		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) )
140	138 139	oveq12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) )
141	137 140	eqeq12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝐻 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝐻 ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) )
142	136 141	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ) ) )
143		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
144	4 5	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
145	3	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐵 · 𝐶 ) ∈ ℂ ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐵 · 𝐶 ) )
146	143 144 145	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐵 · 𝐶 ) )
147	1	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℂ ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
148	143 4 147	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
149	148	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = ( 𝐹 ‘ 𝑥 ) )
150	2	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ℂ ) → ( 𝐺 ‘ 𝑥 ) = 𝐶 )
151	143 5 150	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = 𝐶 )
152	151	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 = ( 𝐺 ‘ 𝑥 ) )
153	149 152	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 · 𝐶 ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) )
154	146 153	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) )
155	134 142 154	chvarfv	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) )
156	155	fvoveq1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( 𝑋 · 𝑌 ) ) ) )
157	118 119 156	syl2anc	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( 𝑋 · 𝑌 ) ) ) )
158	18	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
159	30	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
160	158 159	jca	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℂ ) )
161	118 119 160	syl2anc	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℂ ) )
162		simpll3	⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) )
163	162	3ad2ant1	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) )
164		rsp	⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) )
165	164	3imp	⊢ ( ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) )
166	165	3adant1l	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) )
167		fvoveq1	⊢ ( 𝑐 = ( 𝐹 ‘ 𝑧 ) → ( abs ‘ ( 𝑐 − 𝑋 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) )
168	167	breq1d	⊢ ( 𝑐 = ( 𝐹 ‘ 𝑧 ) → ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ) )
169	168	anbi1d	⊢ ( 𝑐 = ( 𝐹 ‘ 𝑧 ) → ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) ) )
170		oveq1	⊢ ( 𝑐 = ( 𝐹 ‘ 𝑧 ) → ( 𝑐 · 𝑑 ) = ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) )
171	170	fvoveq1d	⊢ ( 𝑐 = ( 𝐹 ‘ 𝑧 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) )
172	171	breq1d	⊢ ( 𝑐 = ( 𝐹 ‘ 𝑧 ) → ( ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) )
173	169 172	imbi12d	⊢ ( 𝑐 = ( 𝐹 ‘ 𝑧 ) → ( ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ↔ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) )
174		fvoveq1	⊢ ( 𝑑 = ( 𝐺 ‘ 𝑧 ) → ( abs ‘ ( 𝑑 − 𝑌 ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) )
175	174	breq1d	⊢ ( 𝑑 = ( 𝐺 ‘ 𝑧 ) → ( ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) )
176	175	anbi2d	⊢ ( 𝑑 = ( 𝐺 ‘ 𝑧 ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) )
177		oveq2	⊢ ( 𝑑 = ( 𝐺 ‘ 𝑧 ) → ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) )
178	177	fvoveq1d	⊢ ( 𝑑 = ( 𝐺 ‘ 𝑧 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( 𝑋 · 𝑌 ) ) ) )
179	178	breq1d	⊢ ( 𝑑 = ( 𝐺 ‘ 𝑧 ) → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) )
180	176 179	imbi12d	⊢ ( 𝑑 = ( 𝐺 ‘ 𝑧 ) → ( ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ↔ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) )
181	173 180	rspc2v	⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℂ ) → ( ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) )
182	161 163 166 181	syl3c	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 )
183	157 182	eqbrtrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) ∧ 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 )
184	183	3exp	⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) )
185	115 184	ralrimi	⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) )
186	185	ex	⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) )
187	186	reximdva	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) → ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − 𝑌 ) ) < 𝑏 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) )
188	112 187	mpd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) )
189	188	3exp	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → ( ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ) )
190	189	rexlimdvv	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ( ∃ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ∀ 𝑐 ∈ ℂ ∀ 𝑑 ∈ ℂ ( ( ( abs ‘ ( 𝑐 − 𝑋 ) ) < 𝑎 ∧ ( abs ‘ ( 𝑑 − 𝑌 ) ) < 𝑏 ) → ( abs ‘ ( ( 𝑐 · 𝑑 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) )
191	17 190	mpd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) )
192	191	ralrimiva	⊢ ( 𝜑 → ∀ 𝑤 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) )
193	144 3	fmptd	⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ ℂ )
194	193 23 24	ellimc3	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ∈ ( 𝐻 limℂ 𝐷 ) ↔ ( ( 𝑋 · 𝑌 ) ∈ ℂ ∧ ∀ 𝑤 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝐷 ∧ ( abs ‘ ( 𝑧 − 𝐷 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑧 ) − ( 𝑋 · 𝑌 ) ) ) < 𝑤 ) ) ) )
195	12 192 194	mpbir2and	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ ( 𝐻 limℂ 𝐷 ) )