mullimcf - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mullimcf		Structured version Visualization version GIF version

Theorem mullimcf 46197

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

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

**Assertion**
Ref	Expression
mullimcf	⊢ (𝜑 → (𝐵 · 𝐶) ∈ (𝐻 lim_ℂ 𝐷))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 𝑥,𝐷 𝑥,𝐹 𝑥,𝐺 𝜑,𝑥 Allowed substitution hints: 𝐶(𝑥) 𝐻(𝑥)

Proof of Theorem mullimcf Dummy variables 𝑎 𝑏 𝑒 𝑓 𝑦 𝑧 𝑤 𝑐 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		limccl 25995	. . . 4 ⊢ (𝐹 lim_ℂ 𝐷) ⊆ ℂ
2		mullimcf.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝐹 lim_ℂ 𝐷))
3	1, 2	sselid 3937	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℂ)
4		limccl 25995	. . . 4 ⊢ (𝐺 lim_ℂ 𝐷) ⊆ ℂ
5		mullimcf.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ (𝐺 lim_ℂ 𝐷))
6	4, 5	sselid 3937	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℂ)
7	3, 6	mulcld 11217	. 2 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
8		simpr 489	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → 𝑤 ∈ ℝ⁺)
9	3	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → 𝐵 ∈ ℂ)
10	6	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → 𝐶 ∈ ℂ)
11		mulcn2 15637	. . . . 5 ⊢ ((𝑤 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
12	8, 9, 10, 11	syl3anc 1394	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
13		mullimcf.f	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
14	13	fdmd 6706	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐹 = 𝐴)
15		limcrcl 25994	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (𝐹 lim_ℂ 𝐷) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ))
16	2, 15	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ))
17	16	simp2d 1159	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐹 ⊆ ℂ)
18	14, 17	eqsstrrd 3974	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
19	16	simp3d 1160	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ ℂ)
20	13, 18, 19	ellimc3 25999	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 ∈ (𝐹 lim_ℂ 𝐷) ↔ (𝐵 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))))
21	2, 20	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)))
22	21	simprd 500	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑎 ∈ ℝ⁺ ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
23	22	r19.21bi 3257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺) → ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
24	23	adantrr 729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
25		mullimcf.g	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺:𝐴⟶ℂ)
26	25, 18, 19	ellimc3 25999	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶 ∈ (𝐺 lim_ℂ 𝐷) ↔ (𝐶 ∈ ℂ ∧ ∀𝑏 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))))
27	5, 26	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 ∈ ℂ ∧ ∀𝑏 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
28	27	simprd 500	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑏 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
29	28	r19.21bi 3257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ⁺) → ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
30	29	adantrl 728	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
31		reeanv 3237	. . . . . . . . . . 11 ⊢ (∃𝑒 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ↔ (∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
32	24, 30, 31	sylanbrc 594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑒 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
33		ifcl 4529	. . . . . . . . . . . . . 14 ⊢ ((𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ⁺)
34	33	3ad2ant2 1150	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ⁺)
35		nfv 1937	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺))
36		nfv 1937	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)
37		nfra1 3289	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)
38		nfra1 3289	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)
39	37, 38	nfan 1922	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
40	35, 36, 39	nf3an 1924	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
41		simp11l 1301	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑)
42		simp1rl 1255	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝑎 ∈ ℝ⁺)
43	42	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑎 ∈ ℝ⁺)
44	41, 43	jca 520	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝜑 ∧ 𝑎 ∈ ℝ⁺))
45		simp12 1221	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺))
46		simp13l 1305	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
47	44, 45, 46	jca31 523	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)))
48		simp1r 1215	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
49		simp2 1153	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ∈ 𝐴)
50		simp3l 1218	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ≠ 𝐷)
51		simplll 786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) → 𝜑)
52	51	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑)
53		simp1lr 1254	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺))
54		simp3r 1219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))
55		simp1l 1214	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝜑)
56		simp2 1153	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑧 ∈ 𝐴)
57	18	sselda 3939	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ)
58	55, 56, 57	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑧 ∈ ℂ)
59	55, 19	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝐷 ∈ ℂ)
60	58, 59	subcld 11557	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (𝑧 − 𝐷) ∈ ℂ)
61	60	abscld 15480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) ∈ ℝ)
62		rpre 13016	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 ∈ ℝ⁺ → 𝑒 ∈ ℝ)
63	62	ad2antrl 740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) → 𝑒 ∈ ℝ)
64	63	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑒 ∈ ℝ)
65		rpre 13016	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∈ ℝ⁺ → 𝑓 ∈ ℝ)
66	65	ad2antll 741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) → 𝑓 ∈ ℝ)
67	66	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑓 ∈ ℝ)
68	64, 67	ifcld 4530	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ)
69		simp3 1154	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))
70		min1 13206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑒)
71	64, 67, 70	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑒)
72	61, 68, 64, 69, 71	ltletrd 11358	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < 𝑒)
73	52, 53, 49, 54, 72	syl211anc 1399	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < 𝑒)
74	50, 73	jca 520	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒))
75		rsp 3253	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)))
76	48, 49, 74, 75	syl3c 67	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)
77	47, 76	syld3an1 1433	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)
78		simp1l 1214	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝜑)
79	78, 42	jca 520	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝜑 ∧ 𝑎 ∈ ℝ⁺))
80		simp2 1153	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺))
81		simp3r 1219	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
82	79, 80, 81	jca31 523	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
83		simp1r 1215	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
84		simp2 1153	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ∈ 𝐴)
85		simp3l 1218	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ≠ 𝐷)
86		simplll 786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → 𝜑)
87	86	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑)
88		simp1lr 1254	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺))
89		simp3r 1219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))
90		min2 13207	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑓)
91	64, 67, 90	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑓)
92	61, 68, 67, 69, 91	ltletrd 11358	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < 𝑓)
93	87, 88, 84, 89, 92	syl211anc 1399	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < 𝑓)
94	85, 93	jca 520	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓))
95		rsp 3253	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
96	83, 84, 94, 95	syl3c 67	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)
97	82, 96	syl3an1 1179	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)
98	77, 97	jca 520	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
99	98	3exp 1135	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))))
100	40, 99	ralrimi 3263	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
101		brimralrspcev 5166	. . . . . . . . . . . . 13 ⊢ ((if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ⁺ ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
102	34, 100, 101	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
103	102	3exp 1135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ((𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) → ((∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))))
104	103	rexlimdvv 3221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → (∃𝑒 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))))
105	32, 104	mpd 16	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
106	105	adantlr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
107	106	3adant3 1148	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
108		nfv 1937	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺)
109		nfra1 3289	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
110	108, 109	nfan 1922	. . . . . . . . . 10 ⊢ Ⅎ𝑧((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
111		simp1l 1214	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → 𝜑)
112	111	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝜑)
113	112	3ad2ant1 1149	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → 𝜑)
114		simp2 1153	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → 𝑧 ∈ 𝐴)
115		mullimcf.h	. . . . . . . . . . . . . . 15 ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥) · (𝐺‘𝑥)))
116		fveq2 6871	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
117		fveq2 6871	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧))
118	116, 117	oveq12d 7418	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) · (𝐺‘𝑥)) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
119		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
120	13	ffvelcdmda 7069	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ)
121	25	ffvelcdmda 7069	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℂ)
122	120, 121	mulcld 11217	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ)
123	115, 118, 119, 122	fvmptd3 7003	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐻‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
124	123	fvoveq1d 7422	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))))
125	113, 114, 124	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))))
126	120, 121	jca 520	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ))
127	113, 114, 126	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ))
128		simpll3 1231	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
129	128	3ad2ant1 1149	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
130		rsp 3253	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))))
131	130	3imp 1126	. . . . . . . . . . . . . 14 ⊢ ((∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
132	131	3adant1l 1193	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
133		fvoveq1 7423	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑧) → (abs‘(𝑐 − 𝐵)) = (abs‘((𝐹‘𝑧) − 𝐵)))
134	133	breq1d 5115	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐹‘𝑧) → ((abs‘(𝑐 − 𝐵)) < 𝑎 ↔ (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
135	134	anbi1d 642	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝐹‘𝑧) → (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) ↔ ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏)))
136		oveq1 7407	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑧) → (𝑐 · 𝑑) = ((𝐹‘𝑧) · 𝑑))
137	136	fvoveq1d 7422	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐹‘𝑧) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))))
138	137	breq1d 5115	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝐹‘𝑧) → ((abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤 ↔ (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
139	135, 138	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (𝐹‘𝑧) → ((((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) ↔ (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤)))
140		fvoveq1 7423	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝐺‘𝑧) → (abs‘(𝑑 − 𝐶)) = (abs‘((𝐺‘𝑧) − 𝐶)))
141	140	breq1d 5115	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = (𝐺‘𝑧) → ((abs‘(𝑑 − 𝐶)) < 𝑏 ↔ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
142	141	anbi2d 641	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = (𝐺‘𝑧) → (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) ↔ ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
143		oveq2 7408	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝐺‘𝑧) → ((𝐹‘𝑧) · 𝑑) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
144	143	fvoveq1d 7422	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = (𝐺‘𝑧) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))))
145	144	breq1d 5115	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = (𝐺‘𝑧) → ((abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤 ↔ (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤))
146	142, 145	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑑 = (𝐺‘𝑧) → ((((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤) ↔ (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤)))
147	139, 146	rspc2v 3595	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) → (∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤)))
148	127, 129, 132, 147	syl3c 67	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤)
149	125, 148	eqbrtrd 5127	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)
150	149	3exp 1135	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))
151	110, 150	ralrimi 3263	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))
152	151	ex 417	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) → (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))
153	152	reximdva 3178	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → (∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))
154	107, 153	mpd 16	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))
155	154	3exp 1135	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → (∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))))
156	155	rexlimdvv 3221	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → (∃𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))
157	12, 156	mpd 16	. . 3 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))
158	157	ralrimiva 3157	. 2 ⊢ (𝜑 → ∀𝑤 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))
159	13	ffvelcdmda 7069	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ)
160	25	ffvelcdmda 7069	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ ℂ)
161	159, 160	mulcld 11217	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ)
162	161, 115	fmptd 7099	. . 3 ⊢ (𝜑 → 𝐻:𝐴⟶ℂ)
163	162, 18, 19	ellimc3 25999	. 2 ⊢ (𝜑 → ((𝐵 · 𝐶) ∈ (𝐻 lim_ℂ 𝐷) ↔ ((𝐵 · 𝐶) ∈ ℂ ∧ ∀𝑤 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))))
164	7, 158, 163	mpbir2and 725	1 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ (𝐻 lim_ℂ 𝐷))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 ∀wral 3079 ∃wrex 3089 ⊆ wss 3907 ifcif 4483 class class class wbr 5105 ↦ cmpt 5186 dom cdm 5652 ⟶wf 6521 ‘cfv 6525 (class class class)co 7400 ℂcc 11086 ℝcr 11087 · cmul 11093 < clt 11231 ≤ cle 11232 − cmin 11429 ℝ⁺crp 13007 abscabs 15275 lim_ℂ climc 25982

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5232 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4869 df-int 4909 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-1st 7974 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-er 8682 df-map 8814 df-pm 8815 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-fi 9359 df-sup 9390 df-inf 9391 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12225 df-2 12294 df-3 12295 df-4 12296 df-5 12297 df-6 12298 df-7 12299 df-8 12300 df-9 12301 df-n0 12496 df-z 12583 df-dec 12703 df-uz 12854 df-q 12964 df-rp 13008 df-xneg 13128 df-xadd 13129 df-xmul 13130 df-fz 13527 df-seq 14029 df-exp 14089 df-cj 15140 df-re 15141 df-im 15142 df-sqrt 15276 df-abs 15277 df-struct 17197 df-slot 17232 df-ndx 17244 df-base 17260 df-plusg 17313 df-mulr 17314 df-starv 17315 df-tset 17319 df-ple 17320 df-ds 17322 df-unif 17323 df-rest 17465 df-topn 17466 df-topgen 17486 df-psmet 21474 df-xmet 21475 df-met 21476 df-bl 21477 df-mopn 21478 df-cnfld 21483 df-top 23012 df-topon 23029 df-topsp 23051 df-bases 23064 df-cnp 23346 df-xms 24438 df-ms 24439 df-limc 25986

This theorem is referenced by: fourierdlem101 46779 fourierdlem111 46789

W3C validator