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 46850

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 26228	. . . 4 ⊢ (𝐹 lim_ℂ 𝐷) ⊆ ℂ
2		mullimcf.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝐹 lim_ℂ 𝐷))
3	1, 2	sselid 3911	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℂ)
4		limccl 26228	. . . 4 ⊢ (𝐺 lim_ℂ 𝐷) ⊆ ℂ
5		mullimcf.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ (𝐺 lim_ℂ 𝐷))
6	4, 5	sselid 3911	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℂ)
7	3, 6	mulcld 11359	. 2 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
8		simpr 490	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → 𝑤 ∈ ℝ⁺)
9	3	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → 𝐵 ∈ ℂ)
10	6	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → 𝐶 ∈ ℂ)
11		mulcn2 15795	. . . . 5 ⊢ ((𝑤 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
12	8, 9, 10, 11	syl3anc 1399	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
13		mullimcf.f	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
14	13	fdmd 6745	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐹 = 𝐴)
15		limcrcl 26227	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (𝐹 lim_ℂ 𝐷) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ))
16	2, 15	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ))
17	16	simp2d 1161	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐹 ⊆ ℂ)
18	14, 17	eqsstrrd 3948	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
19	16	simp3d 1162	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ ℂ)
20	13, 18, 19	ellimc3 26232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 ∈ (𝐹 lim_ℂ 𝐷) ↔ (𝐵 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))))
21	2, 20	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)))
22	21	simprd 501	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑎 ∈ ℝ⁺ ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
23	22	r19.21bi 3258	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺) → ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
24	23	adantrr 730	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
25		mullimcf.g	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺:𝐴⟶ℂ)
26	25, 18, 19	ellimc3 26232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶 ∈ (𝐺 lim_ℂ 𝐷) ↔ (𝐶 ∈ ℂ ∧ ∀𝑏 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))))
27	5, 26	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 ∈ ℂ ∧ ∀𝑏 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
28	27	simprd 501	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑏 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
29	28	r19.21bi 3258	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ⁺) → ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
30	29	adantrl 729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
31		reeanv 3238	. . . . . . . . . . 11 ⊢ (∃𝑒 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ↔ (∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
32	24, 30, 31	sylanbrc 595	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑒 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
33		ifcl 4531	. . . . . . . . . . . . . 14 ⊢ ((𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ⁺)
34	33	3ad2ant2 1152	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ⁺)
35		nfv 1949	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺))
36		nfv 1949	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)
37		nfra1 3290	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)
38		nfra1 3290	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)
39	37, 38	nfan 1934	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
40	35, 36, 39	nf3an 1936	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
41		simp11l 1303	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑)
42		simp1rl 1257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝑎 ∈ ℝ⁺)
43	42	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑎 ∈ ℝ⁺)
44	41, 43	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝜑 ∧ 𝑎 ∈ ℝ⁺))
45		simp12 1223	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺))
46		simp13l 1307	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
47	44, 45, 46	jca31 524	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)))
48		simp1r 1217	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
49		simp2 1155	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ∈ 𝐴)
50		simp3l 1220	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ≠ 𝐷)
51		simplll 787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) → 𝜑)
52	51	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑)
53		simp1lr 1256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺))
54		simp3r 1221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))
55		simp1l 1216	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝜑)
56		simp2 1155	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑧 ∈ 𝐴)
57	18	sselda 3913	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ)
58	55, 56, 57	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑧 ∈ ℂ)
59	55, 19	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝐷 ∈ ℂ)
60	58, 59	subcld 11699	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (𝑧 − 𝐷) ∈ ℂ)
61	60	abscld 15638	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) ∈ ℝ)
62		rpre 13159	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 ∈ ℝ⁺ → 𝑒 ∈ ℝ)
63	62	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) → 𝑒 ∈ ℝ)
64	63	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑒 ∈ ℝ)
65		rpre 13159	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∈ ℝ⁺ → 𝑓 ∈ ℝ)
66	65	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) → 𝑓 ∈ ℝ)
67	66	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑓 ∈ ℝ)
68	64, 67	ifcld 4532	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ)
69		simp3 1156	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))
70		min1 13349	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑒)
71	64, 67, 70	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑒)
72	61, 68, 64, 69, 71	ltletrd 11500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < 𝑒)
73	52, 53, 49, 54, 72	syl211anc 1404	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < 𝑒)
74	50, 73	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒))
75		rsp 3254	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)))
76	48, 49, 74, 75	syl3c 67	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)
77	47, 76	syld3an1 1438	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)
78		simp1l 1216	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝜑)
79	78, 42	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝜑 ∧ 𝑎 ∈ ℝ⁺))
80		simp2 1155	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺))
81		simp3r 1221	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
82	79, 80, 81	jca31 524	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
83		simp1r 1217	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
84		simp2 1155	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ∈ 𝐴)
85		simp3l 1220	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ≠ 𝐷)
86		simplll 787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → 𝜑)
87	86	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑)
88		simp1lr 1256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺))
89		simp3r 1221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))
90		min2 13350	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑓)
91	64, 67, 90	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑓)
92	61, 68, 67, 69, 91	ltletrd 11500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < 𝑓)
93	87, 88, 84, 89, 92	syl211anc 1404	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < 𝑓)
94	85, 93	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓))
95		rsp 3254	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
96	83, 84, 94, 95	syl3c 67	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)
97	82, 96	syl3an1 1181	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)
98	77, 97	jca 521	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
99	98	3exp 1137	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))))
100	40, 99	ralrimi 3264	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
101		brimralrspcev 5170	. . . . . . . . . . . . 13 ⊢ ((if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ⁺ ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
102	34, 100, 101	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
103	102	3exp 1137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ((𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) → ((∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))))
104	103	rexlimdvv 3222	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → (∃𝑒 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))))
105	32, 104	mpd 16	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
106	105	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
107	106	3adant3 1150	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
108		nfv 1949	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺)
109		nfra1 3290	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
110	108, 109	nfan 1934	. . . . . . . . . 10 ⊢ Ⅎ𝑧((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
111		simp1l 1216	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → 𝜑)
112	111	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝜑)
113	112	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → 𝜑)
114		simp2 1155	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → 𝑧 ∈ 𝐴)
115		mullimcf.h	. . . . . . . . . . . . . . 15 ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥) · (𝐺‘𝑥)))
116		fveq2 6911	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
117		fveq2 6911	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧))
118	116, 117	oveq12d 7464	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) · (𝐺‘𝑥)) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
119		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
120	13	ffvelcdmda 7111	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ)
121	25	ffvelcdmda 7111	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℂ)
122	120, 121	mulcld 11359	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ)
123	115, 118, 119, 122	fvmptd3 7043	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐻‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
124	123	fvoveq1d 7468	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))))
125	113, 114, 124	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))))
126	120, 121	jca 521	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ))
127	113, 114, 126	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ))
128		simpll3 1233	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
129	128	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
130		rsp 3254	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))))
131	130	3imp 1128	. . . . . . . . . . . . . 14 ⊢ ((∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
132	131	3adant1l 1195	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
133		fvoveq1 7469	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑧) → (abs‘(𝑐 − 𝐵)) = (abs‘((𝐹‘𝑧) − 𝐵)))
134	133	breq1d 5116	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐹‘𝑧) → ((abs‘(𝑐 − 𝐵)) < 𝑎 ↔ (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
135	134	anbi1d 643	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝐹‘𝑧) → (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) ↔ ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏)))
136		oveq1 7453	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑧) → (𝑐 · 𝑑) = ((𝐹‘𝑧) · 𝑑))
137	136	fvoveq1d 7468	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐹‘𝑧) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))))
138	137	breq1d 5116	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝐹‘𝑧) → ((abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤 ↔ (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
139	135, 138	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (𝐹‘𝑧) → ((((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) ↔ (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤)))
140		fvoveq1 7469	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝐺‘𝑧) → (abs‘(𝑑 − 𝐶)) = (abs‘((𝐺‘𝑧) − 𝐶)))
141	140	breq1d 5116	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = (𝐺‘𝑧) → ((abs‘(𝑑 − 𝐶)) < 𝑏 ↔ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
142	141	anbi2d 642	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = (𝐺‘𝑧) → (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) ↔ ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
143		oveq2 7454	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝐺‘𝑧) → ((𝐹‘𝑧) · 𝑑) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
144	143	fvoveq1d 7468	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = (𝐺‘𝑧) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))))
145	144	breq1d 5116	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = (𝐺‘𝑧) → ((abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤 ↔ (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤))
146	142, 145	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑑 = (𝐺‘𝑧) → ((((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤) ↔ (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤)))
147	139, 146	rspc2v 3590	. . . . . . . . . . . . 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 5131	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)
150	149	3exp 1137	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))
151	110, 150	ralrimi 3264	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))
152	151	ex 418	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) → (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))
153	152	reximdva 3179	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → (∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))
154	107, 153	mpd 16	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))
155	154	3exp 1137	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → (∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))))
156	155	rexlimdvv 3222	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → (∃𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))
157	12, 156	mpd 16	. . 3 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))
158	157	ralrimiva 3158	. 2 ⊢ (𝜑 → ∀𝑤 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))
159	13	ffvelcdmda 7111	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ)
160	25	ffvelcdmda 7111	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ ℂ)
161	159, 160	mulcld 11359	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ)
162	161, 115	fmptd 7141	. . 3 ⊢ (𝜑 → 𝐻:𝐴⟶ℂ)
163	162, 18, 19	ellimc3 26232	. 2 ⊢ (𝜑 → ((𝐵 · 𝐶) ∈ (𝐻 lim_ℂ 𝐷) ↔ ((𝐵 · 𝐶) ∈ ℂ ∧ ∀𝑤 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))))
164	7, 158, 163	mpbir2and 726	1 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ (𝐻 lim_ℂ 𝐷))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 ⊆ wss 3900 ifcif 4485 class class class wbr 5106 ↦ cmpt 5190 dom cdm 5656 ⟶wf 6557 ‘cfv 6561 (class class class)co 7446 ℂcc 11228 ℝcr 11229 · cmul 11235 < clt 11373 ≤ cle 11374 − cmin 11571 ℝ⁺crp 13150 abscabs 15433 lim_ℂ climc 26215

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307 ax-pre-sup 11308

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-om 7905 df-1st 8028 df-2nd 8029 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-er 8748 df-map 8880 df-pm 8881 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-fi 9433 df-sup 9464 df-inf 9465 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-div 12004 df-nn 12366 df-2 12435 df-3 12436 df-4 12437 df-5 12438 df-6 12439 df-7 12440 df-8 12441 df-9 12442 df-n0 12637 df-z 12724 df-dec 12845 df-uz 12996 df-q 13106 df-rp 13151 df-xneg 13271 df-xadd 13272 df-xmul 13273 df-fz 13670 df-seq 14175 df-exp 14235 df-cj 15298 df-re 15299 df-im 15300 df-sqrt 15434 df-abs 15435 df-struct 17357 df-slot 17392 df-ndx 17404 df-base 17420 df-plusg 17473 df-mulr 17474 df-starv 17475 df-tset 17479 df-ple 17480 df-ds 17482 df-unif 17483 df-rest 17625 df-topn 17626 df-topgen 17646 df-psmet 21703 df-xmet 21704 df-met 21705 df-bl 21706 df-mopn 21707 df-cnfld 21712 df-top 23245 df-topon 23262 df-topsp 23284 df-bases 23297 df-cnp 23579 df-xms 24672 df-ms 24673 df-limc 26219

This theorem is used by: fourierdlem101 47432 fourierdlem111 47442

W3C validator