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 45638

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 25910	. . . 4 ⊢ (𝐹 lim_ℂ 𝐷) ⊆ ℂ
2		mullimcf.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝐹 lim_ℂ 𝐷))
3	1, 2	sselid 3981	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℂ)
4		limccl 25910	. . . 4 ⊢ (𝐺 lim_ℂ 𝐷) ⊆ ℂ
5		mullimcf.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ (𝐺 lim_ℂ 𝐷))
6	4, 5	sselid 3981	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℂ)
7	3, 6	mulcld 11281	. 2 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
8		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → 𝑤 ∈ ℝ⁺)
9	3	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → 𝐵 ∈ ℂ)
10	6	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → 𝐶 ∈ ℂ)
11		mulcn2 15632	. . . . 5 ⊢ ((𝑤 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
12	8, 9, 10, 11	syl3anc 1373	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
13		mullimcf.f	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
14	13	fdmd 6746	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐹 = 𝐴)
15		limcrcl 25909	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (𝐹 lim_ℂ 𝐷) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ))
16	2, 15	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ))
17	16	simp2d 1144	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐹 ⊆ ℂ)
18	14, 17	eqsstrrd 4019	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
19	16	simp3d 1145	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 ∈ ℂ)
20	13, 18, 19	ellimc3 25914	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 ∈ (𝐹 lim_ℂ 𝐷) ↔ (𝐵 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))))
21	2, 20	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 ∈ ℂ ∧ ∀𝑎 ∈ ℝ⁺ ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)))
22	21	simprd 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑎 ∈ ℝ⁺ ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
23	22	r19.21bi 3251	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ⁺) → ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
24	23	adantrr 717	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
25		mullimcf.g	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺:𝐴⟶ℂ)
26	25, 18, 19	ellimc3 25914	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶 ∈ (𝐺 lim_ℂ 𝐷) ↔ (𝐶 ∈ ℂ ∧ ∀𝑏 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))))
27	5, 26	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 ∈ ℂ ∧ ∀𝑏 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
28	27	simprd 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑏 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
29	28	r19.21bi 3251	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑏 ∈ ℝ⁺) → ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
30	29	adantrl 716	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
31		reeanv 3229	. . . . . . . . . . 11 ⊢ (∃𝑒 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ↔ (∃𝑒 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∃𝑓 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
32	24, 30, 31	sylanbrc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑒 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
33		ifcl 4571	. . . . . . . . . . . . . 14 ⊢ ((𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ⁺)
34	33	3ad2ant2 1135	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ⁺)
35		nfv 1914	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺))
36		nfv 1914	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)
37		nfra1 3284	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)
38		nfra1 3284	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)
39	37, 38	nfan 1899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧(∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
40	35, 36, 39	nf3an 1901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
41		simp11l 1285	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑)
42		simp1rl 1239	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝑎 ∈ ℝ⁺)
43	42	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑎 ∈ ℝ⁺)
44	41, 43	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝜑 ∧ 𝑎 ∈ ℝ⁺))
45		simp12 1205	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺))
46		simp13l 1289	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
47	44, 45, 46	jca31 514	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)))
48		simp1r 1199	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
49		simp2 1138	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ∈ 𝐴)
50		simp3l 1202	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ≠ 𝐷)
51		simplll 775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) → 𝜑)
52	51	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑)
53		simp1lr 1238	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺))
54		simp3r 1203	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))
55		simp1l 1198	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝜑)
56		simp2 1138	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑧 ∈ 𝐴)
57	18	sselda 3983	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ)
58	55, 56, 57	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑧 ∈ ℂ)
59	55, 19	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝐷 ∈ ℂ)
60	58, 59	subcld 11620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (𝑧 − 𝐷) ∈ ℂ)
61	60	abscld 15475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) ∈ ℝ)
62		rpre 13043	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 ∈ ℝ⁺ → 𝑒 ∈ ℝ)
63	62	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) → 𝑒 ∈ ℝ)
64	63	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑒 ∈ ℝ)
65		rpre 13043	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∈ ℝ⁺ → 𝑓 ∈ ℝ)
66	65	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) → 𝑓 ∈ ℝ)
67	66	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → 𝑓 ∈ ℝ)
68	64, 67	ifcld 4572	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ)
69		simp3 1139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))
70		min1 13231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑒)
71	64, 67, 70	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑒)
72	61, 68, 64, 69, 71	ltletrd 11421	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < 𝑒)
73	52, 53, 49, 54, 72	syl211anc 1378	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < 𝑒)
74	50, 73	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒))
75		rsp 3247	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)))
76	48, 49, 74, 75	syl3c 66	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)
77	47, 76	syld3an1 1412	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎)
78		simp1l 1198	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝜑)
79	78, 42	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝜑 ∧ 𝑎 ∈ ℝ⁺))
80		simp2 1138	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺))
81		simp3r 1203	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
82	79, 80, 81	jca31 514	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
83		simp1r 1199	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
84		simp2 1138	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ∈ 𝐴)
85		simp3l 1202	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝑧 ≠ 𝐷)
86		simplll 775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → 𝜑)
87	86	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → 𝜑)
88		simp1lr 1238	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺))
89		simp3r 1203	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))
90		min2 13232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑓)
91	64, 67, 90	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ≤ 𝑓)
92	61, 68, 67, 69, 91	ltletrd 11421	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ 𝑧 ∈ 𝐴 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → (abs‘(𝑧 − 𝐷)) < 𝑓)
93	87, 88, 84, 89, 92	syl211anc 1378	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘(𝑧 − 𝐷)) < 𝑓)
94	85, 93	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓))
95		rsp 3247	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
96	83, 84, 94, 95	syl3c 66	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ⁺) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺)) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)
97	82, 96	syl3an1 1164	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)
98	77, 97	jca 511	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓))) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
99	98	3exp 1120	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))))
100	40, 99	ralrimi 3257	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
101		brimralrspcev 5204	. . . . . . . . . . . . 13 ⊢ ((if(𝑒 ≤ 𝑓, 𝑒, 𝑓) ∈ ℝ⁺ ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < if(𝑒 ≤ 𝑓, 𝑒, 𝑓)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
102	34, 100, 101	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) ∧ (𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) ∧ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
103	102	3exp 1120	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ((𝑒 ∈ ℝ⁺ ∧ 𝑓 ∈ ℝ⁺) → ((∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))))
104	103	rexlimdvv 3212	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → (∃𝑒 ∈ ℝ⁺ ∃𝑓 ∈ ℝ⁺ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑒) → (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑓) → (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))))
105	32, 104	mpd 15	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
106	105	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
107	106	3adant3 1133	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
108		nfv 1914	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺)
109		nfra1 3284	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
110	108, 109	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑧((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
111		simp1l 1198	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → 𝜑)
112	111	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → 𝜑)
113	112	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → 𝜑)
114		simp2 1138	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → 𝑧 ∈ 𝐴)
115		mullimcf.h	. . . . . . . . . . . . . . 15 ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥) · (𝐺‘𝑥)))
116		fveq2 6906	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
117		fveq2 6906	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧))
118	116, 117	oveq12d 7449	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) · (𝐺‘𝑥)) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
119		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
120	13	ffvelcdmda 7104	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ)
121	25	ffvelcdmda 7104	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℂ)
122	120, 121	mulcld 11281	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) · (𝐺‘𝑧)) ∈ ℂ)
123	115, 118, 119, 122	fvmptd3 7039	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐻‘𝑧) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
124	123	fvoveq1d 7453	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))))
125	113, 114, 124	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))))
126	120, 121	jca 511	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ))
127	113, 114, 126	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ))
128		simpll3 1215	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
129	128	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
130		rsp 3247	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))))
131	130	3imp 1111	. . . . . . . . . . . . . 14 ⊢ ((∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
132	131	3adant1l 1177	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
133		fvoveq1 7454	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑧) → (abs‘(𝑐 − 𝐵)) = (abs‘((𝐹‘𝑧) − 𝐵)))
134	133	breq1d 5153	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐹‘𝑧) → ((abs‘(𝑐 − 𝐵)) < 𝑎 ↔ (abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎))
135	134	anbi1d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝐹‘𝑧) → (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) ↔ ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏)))
136		oveq1 7438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑧) → (𝑐 · 𝑑) = ((𝐹‘𝑧) · 𝑑))
137	136	fvoveq1d 7453	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐹‘𝑧) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))))
138	137	breq1d 5153	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝐹‘𝑧) → ((abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤 ↔ (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤))
139	135, 138	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (𝐹‘𝑧) → ((((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) ↔ (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤)))
140		fvoveq1 7454	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝐺‘𝑧) → (abs‘(𝑑 − 𝐶)) = (abs‘((𝐺‘𝑧) − 𝐶)))
141	140	breq1d 5153	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = (𝐺‘𝑧) → ((abs‘(𝑑 − 𝐶)) < 𝑏 ↔ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))
142	141	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = (𝐺‘𝑧) → (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) ↔ ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)))
143		oveq2 7439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝐺‘𝑧) → ((𝐹‘𝑧) · 𝑑) = ((𝐹‘𝑧) · (𝐺‘𝑧)))
144	143	fvoveq1d 7453	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = (𝐺‘𝑧) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) = (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))))
145	144	breq1d 5153	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = (𝐺‘𝑧) → ((abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤 ↔ (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤))
146	142, 145	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑑 = (𝐺‘𝑧) → ((((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · 𝑑) − (𝐵 · 𝐶))) < 𝑤) ↔ (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤)))
147	139, 146	rspc2v 3633	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑧) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) → (∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → (((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏) → (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤)))
148	127, 129, 132, 147	syl3c 66	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → (abs‘(((𝐹‘𝑧) · (𝐺‘𝑧)) − (𝐵 · 𝐶))) < 𝑤)
149	125, 148	eqbrtrd 5165	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) ∧ 𝑧 ∈ 𝐴 ∧ (𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦)) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)
150	149	3exp 1120	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))
151	110, 150	ralrimi 3257	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) ∧ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏))) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))
152	151	ex 412	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) ∧ 𝑦 ∈ ℝ⁺) → (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))
153	152	reximdva 3168	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → (∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → ((abs‘((𝐹‘𝑧) − 𝐵)) < 𝑎 ∧ (abs‘((𝐺‘𝑧) − 𝐶)) < 𝑏)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))
154	107, 153	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) ∧ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤)) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))
155	154	3exp 1120	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → (∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))))
156	155	rexlimdvv 3212	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → (∃𝑎 ∈ ℝ⁺ ∃𝑏 ∈ ℝ⁺ ∀𝑐 ∈ ℂ ∀𝑑 ∈ ℂ (((abs‘(𝑐 − 𝐵)) < 𝑎 ∧ (abs‘(𝑑 − 𝐶)) < 𝑏) → (abs‘((𝑐 · 𝑑) − (𝐵 · 𝐶))) < 𝑤) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤)))
157	12, 156	mpd 15	. . 3 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))
158	157	ralrimiva 3146	. 2 ⊢ (𝜑 → ∀𝑤 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))
159	13	ffvelcdmda 7104	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ)
160	25	ffvelcdmda 7104	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ ℂ)
161	159, 160	mulcld 11281	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ)
162	161, 115	fmptd 7134	. . 3 ⊢ (𝜑 → 𝐻:𝐴⟶ℂ)
163	162, 18, 19	ellimc3 25914	. 2 ⊢ (𝜑 → ((𝐵 · 𝐶) ∈ (𝐻 lim_ℂ 𝐷) ↔ ((𝐵 · 𝐶) ∈ ℂ ∧ ∀𝑤 ∈ ℝ⁺ ∃𝑦 ∈ ℝ⁺ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑦) → (abs‘((𝐻‘𝑧) − (𝐵 · 𝐶))) < 𝑤))))
164	7, 158, 163	mpbir2and 713	1 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ (𝐻 lim_ℂ 𝐷))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 ⊆ wss 3951 ifcif 4525 class class class wbr 5143 ↦ cmpt 5225 dom cdm 5685 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 ℂcc 11153 ℝcr 11154 · cmul 11160 < clt 11295 ≤ cle 11296 − cmin 11492 ℝ⁺crp 13034 abscabs 15273 lim_ℂ climc 25897

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-er 8745 df-map 8868 df-pm 8869 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-fi 9451 df-sup 9482 df-inf 9483 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-z 12614 df-dec 12734 df-uz 12879 df-q 12991 df-rp 13035 df-xneg 13154 df-xadd 13155 df-xmul 13156 df-fz 13548 df-seq 14043 df-exp 14103 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-struct 17184 df-slot 17219 df-ndx 17231 df-base 17248 df-plusg 17310 df-mulr 17311 df-starv 17312 df-tset 17316 df-ple 17317 df-ds 17319 df-unif 17320 df-rest 17467 df-topn 17468 df-topgen 17488 df-psmet 21356 df-xmet 21357 df-met 21358 df-bl 21359 df-mopn 21360 df-cnfld 21365 df-top 22900 df-topon 22917 df-topsp 22939 df-bases 22953 df-cnp 23236 df-xms 24330 df-ms 24331 df-limc 25901

This theorem is referenced by: fourierdlem101 46222 fourierdlem111 46232

W3C validator