mullimcf

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

	Ref	Expression
Hypotheses	mullimcf.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	mullimcf.g	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℂ )
	mullimcf.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) )
	mullimcf.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐹 lim_ℂ 𝐷 ) )
	mullimcf.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐺 lim_ℂ 𝐷 ) )
Assertion	mullimcf	⊢ ( 𝜑 → ( 𝐵 · 𝐶 ) ∈ ( 𝐻 lim_ℂ 𝐷 ) )

Proof

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

Metamath Proof Explorer

Theorem mullimcf

Proof