0ellimcdiv - Mathbox for Glauco Siliprandi

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

Theorem 0ellimcdiv 46391

Description: If the numerator converges to 0 and the denominator converges to a nonzero number, then the fraction converges to 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
0ellimcdiv.f	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
0ellimcdiv.g	⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)
0ellimcdiv.h	⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶))
0ellimcdiv.b	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
0ellimcdiv.c	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖ {0}))
0ellimcdiv.0limf	⊢ (𝜑 → 0 ∈ (𝐹 lim_ℂ 𝐸))
0ellimcdiv.d	⊢ (𝜑 → 𝐷 ∈ (𝐺 lim_ℂ 𝐸))
0ellimcdiv.dne0	⊢ (𝜑 → 𝐷 ≠ 0)

**Assertion**
Ref	Expression
0ellimcdiv	⊢ (𝜑 → 0 ∈ (𝐻 lim_ℂ 𝐸))

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

Proof of Theorem 0ellimcdiv Dummy variables 𝑢 𝑣 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0cnd 11203	. 2 ⊢ (𝜑 → 0 ∈ ℂ)
2		0ellimcdiv.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (𝐺 lim_ℂ 𝐸))
3		0ellimcdiv.c	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖ {0}))
4	3	eldifad 3917	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
5		0ellimcdiv.g	. . . . . . . . . . 11 ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)
6	4, 5	fmptd 7109	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:𝐴⟶ℂ)
7		0ellimcdiv.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
8		0ellimcdiv.b	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
9		0ellimcdiv.0limf	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ (𝐹 lim_ℂ 𝐸))
10	7, 8, 9	limcmptdm 46377	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
11		limcrcl 26042	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (𝐺 lim_ℂ 𝐸) → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
12	2, 11	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
13	12	simp3d 1162	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℂ)
14	6, 10, 13	ellimc3 26047	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 ∈ (𝐺 lim_ℂ 𝐸) ↔ (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦))))
15	2, 14	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦)))
16	15	simprd 500	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦))
17	15	simpld 499	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℂ)
18		0ellimcdiv.dne0	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 0)
19	17, 18	absrpcld 15507	. . . . . . . 8 ⊢ (𝜑 → (abs‘𝐷) ∈ ℝ⁺)
20	19	rphalfcld 13076	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ⁺)
21		breq2 5113	. . . . . . . . . 10 ⊢ (𝑦 = ((abs‘𝐷) / 2) → ((abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦 ↔ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
22	21	imbi2d 343	. . . . . . . . 9 ⊢ (𝑦 = ((abs‘𝐷) / 2) → (((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ↔ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
23	22	rexralbidv 3231	. . . . . . . 8 ⊢ (𝑦 = ((abs‘𝐷) / 2) → (∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ↔ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
24	23	rspccva 3580	. . . . . . 7 ⊢ ((∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ∧ ((abs‘𝐷) / 2) ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
25	16, 20, 24	syl2anc 595	. . . . . 6 ⊢ (𝜑 → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
26		simpl1l 1243	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → 𝜑)
27		simpl3 1212	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → 𝑣 ∈ 𝐴)
28		simpr 489	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧))
29		simpl2 1211	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
30	27, 28, 29	mp2d 50	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
31	19	rpcnd 13066	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (abs‘𝐷) ∈ ℂ)
32	31	2halvesd 12494	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) = (abs‘𝐷))
33	32	eqcomd 2769	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘𝐷) = (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)))
34	33	oveq1d 7425	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)))
35		2cnd 12323	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ∈ ℂ)
36		2ne0 12351	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
37	36	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ≠ 0)
38	17, 35, 37	absdivd 15514	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / (abs‘2)))
39		2re 12319	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
40	39	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℝ)
41		0le2 12347	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 2
42	41	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 2)
43	40, 42	absidd 15479	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (abs‘2) = 2)
44	43	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs‘𝐷) / (abs‘2)) = ((abs‘𝐷) / 2))
45	38, 44	eqtr2d 2799	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs‘𝐷) / 2) = (abs‘(𝐷 / 2)))
46	45	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
47	20	rpcnd 13066	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℂ)
48	47, 47	pncand 11574	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) / 2))
49	34, 46, 48	3eqtr3rd 2807	. . . . . . . . . . . 12 ⊢ (𝜑 → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
50	49	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
51	45	eqcomd 2769	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
52	51	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
53	52	oveq2d 7426	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) = ((abs‘𝐷) − ((abs‘𝐷) / 2)))
54	17	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝐷 ∈ ℂ)
55	54	abscld 15495	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) ∈ ℝ)
56	55	3adant3 1150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ∈ ℝ)
57	6	ffvelcdmda 7079	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ∈ ℂ)
58	57	3adant3 1150	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐺‘𝑣) ∈ ℂ)
59	58	abscld 15495	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
60	17	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → 𝐷 ∈ ℂ)
61	60, 58	subcld 11573	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐷 − (𝐺‘𝑣)) ∈ ℂ)
62	61	abscld 15495	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) ∈ ℝ)
63	59, 62	readdcld 11242	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))) ∈ ℝ)
64	56	rehalfcld 12495	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) ∈ ℝ)
65	59, 64	readdcld 11242	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)) ∈ ℝ)
66	57, 54	pncan3d 11576	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣))) = 𝐷)
67	66	eqcomd 2769	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝐷 = ((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣))))
68	67	fveq2d 6885	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) = (abs‘((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣)))))
69	54, 57	subcld 11573	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐷 − (𝐺‘𝑣)) ∈ ℂ)
70	57, 69	abstrid 15515	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣)))) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
71	68, 70	eqbrtrd 5133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
72	71	3adant3 1150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
73	60, 58	abssubd 15512	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) = (abs‘((𝐺‘𝑣) − 𝐷)))
74		simp3 1156	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
75	73, 74	eqbrtrd 5133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) < ((abs‘𝐷) / 2))
76	62, 64, 59, 75	ltadd2dd 11373	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))) < ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)))
77	56, 63, 65, 72, 76	lelttrd 11372	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) < ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)))
78	57	abscld 15495	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
79	78	3adant3 1150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
80	56, 64, 79	ltsubaddd 11814	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺‘𝑣)) ↔ (abs‘𝐷) < ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2))))
81	77, 80	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺‘𝑣)))
82	53, 81	eqbrtrd 5133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) < (abs‘(𝐺‘𝑣)))
83	50, 82	eqbrtrd 5133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
84	26, 27, 30, 83	syl3anc 1398	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
85	84	3exp1 1371	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺) → ((𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) → (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))))
86	85	ralimdv2 3174	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺) → (∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))))
87	86	reximdva 3178	. . . . . 6 ⊢ (𝜑 → (∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))))
88	25, 87	mpd 16	. . . . 5 ⊢ (𝜑 → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
89	88	adantr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
90		simpr 489	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝑦 ∈ ℝ⁺)
91	17	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐷 ∈ ℂ)
92	18	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐷 ≠ 0)
93	91, 92	absrpcld 15507	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (abs‘𝐷) ∈ ℝ⁺)
94	93	rphalfcld 13076	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ((abs‘𝐷) / 2) ∈ ℝ⁺)
95	90, 94	rpmulcld 13080	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺)
96	95	ex 417	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ℝ⁺ → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
97	96	imdistani 578	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
98		eleq1 2851	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (𝑤 ∈ ℝ⁺ ↔ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
99	98	anbi2d 641	. . . . . . . . . 10 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((𝜑 ∧ 𝑤 ∈ ℝ⁺) ↔ (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺)))
100		breq2 5113	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((abs‘((𝐹‘𝑣) − 0)) < 𝑤 ↔ (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
101	100	imbi2d 343	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤) ↔ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
102	101	rexralbidv 3231	. . . . . . . . . 10 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤) ↔ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
103	99, 102	imbi12d 347	. . . . . . . . 9 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤)) ↔ ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))))
104	8, 7	fmptd 7109	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
105	104, 10, 13	ellimc3 26047	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 ∈ (𝐹 lim_ℂ 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤))))
106	9, 105	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤)))
107	106	simprd 500	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤))
108	107	r19.21bi 3257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤))
109	103, 108	vtoclg 3522	. . . . . . . 8 ⊢ ((𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺ → ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
110	95, 97, 109	sylc 66	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
111	110	3ad2ant1 1151	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
112		simp12 1223	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑧 ∈ ℝ⁺)
113		simp2 1155	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑢 ∈ ℝ⁺)
114	112, 113	ifcld 4534	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ⁺)
115		nfv 1944	. . . . . . . . . . 11 ⊢ Ⅎ𝑣(𝜑 ∧ 𝑦 ∈ ℝ⁺)
116		nfv 1944	. . . . . . . . . . 11 ⊢ Ⅎ𝑣 𝑧 ∈ ℝ⁺
117		nfra1 3289	. . . . . . . . . . 11 ⊢ Ⅎ𝑣∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
118	115, 116, 117	nf3an 1931	. . . . . . . . . 10 ⊢ Ⅎ𝑣((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
119		nfv 1944	. . . . . . . . . 10 ⊢ Ⅎ𝑣 𝑢 ∈ ℝ⁺
120		nfra1 3289	. . . . . . . . . 10 ⊢ Ⅎ𝑣∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))
121	118, 119, 120	nf3an 1931	. . . . . . . . 9 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
122		simp111 1321	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (𝜑 ∧ 𝑦 ∈ ℝ⁺))
123		simp112 1322	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ⁺)
124		simp12 1223	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ⁺)
125	122, 123, 124	jca31 523	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺))
126		simp2 1155	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑣 ∈ 𝐴)
127		simp3l 1220	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑣 ≠ 𝐸)
128	125, 126, 127	jca31 523	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸))
129	10	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐴 ⊆ ℂ)
130	129	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → 𝐴 ⊆ ℂ)
131	130	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐴 ⊆ ℂ)
132	131	3ad2ant1 1151	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝐴 ⊆ ℂ)
133	132, 126	sseldd 3938	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑣 ∈ ℂ)
134	13	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐸 ∈ ℂ)
135	134	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → 𝐸 ∈ ℂ)
136	135	3ad2ant1 1151	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐸 ∈ ℂ)
137	136	3ad2ant1 1151	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝐸 ∈ ℂ)
138	133, 137	subcld 11573	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (𝑣 − 𝐸) ∈ ℂ)
139	138	abscld 15495	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) ∈ ℝ)
140	123	rpred 13064	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ)
141	124	rpred 13064	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ)
142	140, 141	ifcld 4534	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ)
143		simp3r 1221	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))
144		min1 13219	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑧)
145	140, 141, 144	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑧)
146	139, 142, 140, 143, 145	ltletrd 11374	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) < 𝑧)
147		simp113 1323	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
148		rspa 3254	. . . . . . . . . . . . 13 ⊢ ((∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ 𝑣 ∈ 𝐴) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
149	147, 126, 148	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
150	127, 146, 149	mp2and 711	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
151		simp13 1224	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
152		rspa 3254	. . . . . . . . . . . . 13 ⊢ ((∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
153	151, 126, 152	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
154		min2 13220	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑢)
155	140, 141, 154	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑢)
156	139, 142, 141, 143, 155	ltletrd 11374	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) < 𝑢)
157	127, 156	jca 520	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢))
158	122	simpld 499	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝜑)
159	158	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → 𝜑)
160		simp12 1223	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → 𝑣 ∈ 𝐴)
161		nfv 1944	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑣 ∈ 𝐴)
162		nfmpt1 5210	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
163	7, 162	nfcxfr 2923	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝐹
164		nfcv 2925	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝑣
165	163, 164	nffv 6891	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥(𝐹‘𝑣)
166	165	nfel1 2941	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐹‘𝑣) ∈ ℂ
167	161, 166	nfim 1926	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)
168		eleq1 2851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑣 → (𝑥 ∈ 𝐴 ↔ 𝑣 ∈ 𝐴))
169	168	anbi2d 641	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑣 ∈ 𝐴)))
170		fveq2 6881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
171	170	eleq1d 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) ∈ ℂ ↔ (𝐹‘𝑣) ∈ ℂ))
172	169, 171	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)))
173		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
174	7	fvmpt2 7001	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → (𝐹‘𝑥) = 𝐵)
175	173, 8, 174	syl2anc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)
176	175, 8	eqeltrd 2863	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ)
177	167, 172, 176	chvarfv 2276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)
178	177	subid1d 11562	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐹‘𝑣) − 0) = (𝐹‘𝑣))
179	178	eqcomd 2769	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) = ((𝐹‘𝑣) − 0))
180	179	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐹‘𝑣)) = (abs‘((𝐹‘𝑣) − 0)))
181	159, 160, 180	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → (abs‘(𝐹‘𝑣)) = (abs‘((𝐹‘𝑣) − 0)))
182		simp3 1156	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢))
183		simp2 1155	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
184	182, 183	mpd 16	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))
185	181, 184	eqbrtrd 5133	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
186	153, 157, 185	mpd3an23 1492	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
187		simp-7l 800	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
188		simp-4r 795	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣 ∈ 𝐴)
189		eldifsni 4758	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 ∈ (ℂ ∖ {0}) → 𝐶 ≠ 0)
190	3, 189	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0)
191	8, 4, 190	divcld 11995	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 𝐶) ∈ ℂ)
192		0ellimcdiv.h	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶))
193	191, 192	fmptd 7109	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐻:𝐴⟶ℂ)
194	193	ffvelcdmda 7079	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) ∈ ℂ)
195	194	subid1d 11562	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐻‘𝑣) − 0) = (𝐻‘𝑣))
196		nfmpt1 5210	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶))
197	192, 196	nfcxfr 2923	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝐻
198	197, 164	nffv 6891	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝐻‘𝑣)
199		nfcv 2925	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥 /
200		nfmpt1 5210	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐶)
201	5, 200	nfcxfr 2923	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝐺
202	201, 164	nffv 6891	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐺‘𝑣)
203	165, 199, 202	nfov 7440	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝐹‘𝑣) / (𝐺‘𝑣))
204	198, 203	nfeq 2938	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣))
205	161, 204	nfim 1926	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
206		fveq2 6881	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (𝐻‘𝑥) = (𝐻‘𝑣))
207		fveq2 6881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → (𝐺‘𝑥) = (𝐺‘𝑣))
208	170, 207	oveq12d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) / (𝐺‘𝑥)) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
209	206, 208	eqeq12d 2779	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑣 → ((𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥)) ↔ (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣))))
210	169, 209	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥))) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))))
211	192	fvmpt2 7001	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝐵 / 𝐶) ∈ ℂ) → (𝐻‘𝑥) = (𝐵 / 𝐶))
212	173, 191, 211	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = (𝐵 / 𝐶))
213	175	eqcomd 2769	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = (𝐹‘𝑥))
214	5	fvmpt2 7001	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ (ℂ ∖ {0})) → (𝐺‘𝑥) = 𝐶)
215	173, 3, 214	syl2anc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = 𝐶)
216	215	eqcomd 2769	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 = (𝐺‘𝑥))
217	213, 216	oveq12d 7428	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 𝐶) = ((𝐹‘𝑥) / (𝐺‘𝑥)))
218	212, 217	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥)))
219	205, 210, 218	chvarfv 2276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
220	195, 219	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐻‘𝑣) − 0) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
221	220	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐻‘𝑣) − 0)) = (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))))
222	187, 188, 221	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻‘𝑣) − 0)) = (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))))
223		simp-6l 798	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝜑 ∧ 𝑦 ∈ ℝ⁺))
224	223, 188	jca 520	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴))
225		simplr 780	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
226		simpr 489	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
227		nfcv 2925	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥0
228	202, 227	nfne 3061	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐺‘𝑣) ≠ 0
229	161, 228	nfim 1926	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)
230	207	neeq1d 3017	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝐺‘𝑥) ≠ 0 ↔ (𝐺‘𝑣) ≠ 0))
231	169, 230	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≠ 0) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)))
232	215, 190	eqnetrd 3025	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≠ 0)
233	229, 231, 232	chvarfv 2276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)
234	177, 57, 233	absdivd 15514	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
235	234	adantlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
236	235	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
237	177	abscld 15495	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐹‘𝑣)) ∈ ℝ)
238	57, 233	absne0d 15506	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ≠ 0)
239	237, 78, 238	redivcld 12047	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
240	239	adantlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
241	240	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
242		rpre 13029	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ⁺ → 𝑦 ∈ ℝ)
243	242	ad2antlr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → 𝑦 ∈ ℝ)
244	20	rpred 13064	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ)
245	244	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘𝐷) / 2) ∈ ℝ)
246	243, 245	remulcld 11243	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
247	246	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
248	57, 233	absrpcld 15507	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
249	248	adantlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
250	249	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
251	247, 250	rerpdivcld 13095	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
252	243	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑦 ∈ ℝ)
253		simp-4l 794	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
254		simpllr 787	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣 ∈ 𝐴)
255	253, 254, 237	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹‘𝑣)) ∈ ℝ)
256		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
257	255, 247, 250, 256	ltdiv1dd 13121	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) < ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))))
258	243	recnd 11241	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → 𝑦 ∈ ℂ)
259	47	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘𝐷) / 2) ∈ ℂ)
260	249	rpcnd 13066	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℂ)
261	238	adantlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ≠ 0)
262	258, 259, 260, 261	divassd 12030	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣)))))
263	262	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣)))))
264	245, 249	rerpdivcld 13095	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
265	264	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
266		1red 11213	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 1 ∈ ℝ)
267		simpllr 787	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 𝑦 ∈ ℝ⁺)
268	244	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((abs‘𝐷) / 2) ∈ ℝ)
269		1rp 13024	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℝ⁺
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 1 ∈ ℝ⁺)
271	248	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
272	47	div1d 11987	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
273	272	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
274		simpr 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
275	273, 274	eqbrtrd 5133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / 1) < (abs‘(𝐺‘𝑣)))
276	268, 270, 271, 275	ltdiv23d 13131	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) < 1)
277	276	adantllr 731	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) < 1)
278	265, 266, 267, 277	ltmul2dd 13120	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣)))) < (𝑦 · 1))
279	263, 278	eqbrtrd 5133	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) < (𝑦 · 1))
280	258	mulridd 11230	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (𝑦 · 1) = 𝑦)
281	280	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (𝑦 · 1) = 𝑦)
282	279, 281	breqtrd 5137	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) < 𝑦)
283	282	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) < 𝑦)
284	241, 251, 252, 257, 283	lttrd 11375	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) < 𝑦)
285	236, 284	eqbrtrd 5133	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) < 𝑦)
286	224, 225, 226, 285	syl21anc 850	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) < 𝑦)
287	222, 286	eqbrtrd 5133	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)
288	128, 150, 186, 287	syl21anc 850	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)
289	288	3exp 1137	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
290	121, 289	ralrimi 3263	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
291		brimralrspcev 5172	. . . . . . . 8 ⊢ ((if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
292	114, 290, 291	syl2anc 595	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
293	292	rexlimdv3a 3170	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → (∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
294	111, 293	mpd 16	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
295	294	rexlimdv3a 3170	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
296	89, 295	mpd 16	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
297	296	ralrimiva 3157	. 2 ⊢ (𝜑 → ∀𝑦 ∈ ℝ⁺ ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
298	193, 10, 13	ellimc3 26047	. 2 ⊢ (𝜑 → (0 ∈ (𝐻 lim_ℂ 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))))
299	1, 297, 298	mpbir2and 725	1 ⊢ (𝜑 → 0 ∈ (𝐻 lim_ℂ 𝐸))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 ∃wrex 3089 ∖ cdif 3902 ⊆ wss 3905 ifcif 4487 {csn 4589 class class class wbr 5109 ↦ cmpt 5192 dom cdm 5661 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ℂcc 11102 ℝcr 11103 0cc0 11104 1c1 11105 + caddc 11107 · cmul 11109 < clt 11247 ≤ cle 11248 − cmin 11445 / cdiv 11875 2c2 12299 ℝ⁺crp 13020 abscabs 15290 lim_ℂ climc 26030

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11160 ax-resscn 11161 ax-1cn 11162 ax-icn 11163 ax-addcl 11164 ax-addrcl 11165 ax-mulcl 11166 ax-mulrcl 11167 ax-mulcom 11168 ax-addass 11169 ax-mulass 11170 ax-distr 11171 ax-i2m1 11172 ax-1ne0 11173 ax-1rid 11174 ax-rnegex 11175 ax-rrecex 11176 ax-cnre 11177 ax-pre-lttri 11178 ax-pre-lttrn 11179 ax-pre-ltadd 11180 ax-pre-mulgt0 11181 ax-pre-sup 11182

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-er 8690 df-map 8822 df-pm 8823 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fi 9367 df-sup 9398 df-inf 9399 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-sub 11447 df-neg 11448 df-div 11876 df-nn 12238 df-2 12307 df-3 12308 df-4 12309 df-5 12310 df-6 12311 df-7 12312 df-8 12313 df-9 12314 df-n0 12509 df-z 12596 df-dec 12716 df-uz 12867 df-q 12977 df-rp 13021 df-xneg 13141 df-xadd 13142 df-xmul 13143 df-fz 13540 df-seq 14043 df-exp 14103 df-cj 15155 df-re 15156 df-im 15157 df-sqrt 15291 df-abs 15292 df-struct 17211 df-slot 17246 df-ndx 17258 df-base 17274 df-plusg 17327 df-mulr 17328 df-starv 17329 df-tset 17333 df-ple 17334 df-ds 17336 df-unif 17337 df-rest 17479 df-topn 17480 df-topgen 17500 df-psmet 21523 df-xmet 21524 df-met 21525 df-bl 21526 df-mopn 21527 df-cnfld 21532 df-top 23060 df-topon 23077 df-topsp 23099 df-bases 23112 df-cnp 23394 df-xms 24486 df-ms 24487 df-limc 26034

This theorem is used by: reclimc 46395

W3C validator