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 46077

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 11137	. 2 ⊢ (𝜑 → 0 ∈ ℂ)
2		0ellimcdiv.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (𝐺 lim_ℂ 𝐸))
3		0ellimcdiv.c	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖ {0}))
4	3	eldifad 3901	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
5		0ellimcdiv.g	. . . . . . . . . . 11 ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)
6	4, 5	fmptd 7066	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:𝐴⟶ℂ)
7		0ellimcdiv.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
8		0ellimcdiv.b	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
9		0ellimcdiv.0limf	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ (𝐹 lim_ℂ 𝐸))
10	7, 8, 9	limcmptdm 46063	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
11		limcrcl 25841	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (𝐺 lim_ℂ 𝐸) → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
12	2, 11	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
13	12	simp3d 1145	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℂ)
14	6, 10, 13	ellimc3 25846	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 ∈ (𝐺 lim_ℂ 𝐸) ↔ (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦))))
15	2, 14	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦)))
16	15	simprd 495	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦))
17	15	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℂ)
18		0ellimcdiv.dne0	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 0)
19	17, 18	absrpcld 15413	. . . . . . . 8 ⊢ (𝜑 → (abs‘𝐷) ∈ ℝ⁺)
20	19	rphalfcld 12998	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ⁺)
21		breq2 5089	. . . . . . . . . 10 ⊢ (𝑦 = ((abs‘𝐷) / 2) → ((abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦 ↔ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
22	21	imbi2d 340	. . . . . . . . 9 ⊢ (𝑦 = ((abs‘𝐷) / 2) → (((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ↔ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
23	22	rexralbidv 3203	. . . . . . . 8 ⊢ (𝑦 = ((abs‘𝐷) / 2) → (∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ↔ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
24	23	rspccva 3563	. . . . . . 7 ⊢ ((∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ∧ ((abs‘𝐷) / 2) ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
25	16, 20, 24	syl2anc 585	. . . . . 6 ⊢ (𝜑 → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
26		simpl1l 1226	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → 𝜑)
27		simpl3 1195	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → 𝑣 ∈ 𝐴)
28		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧))
29		simpl2 1194	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
30	27, 28, 29	mp2d 49	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
31	19	rpcnd 12988	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (abs‘𝐷) ∈ ℂ)
32	31	2halvesd 12423	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) = (abs‘𝐷))
33	32	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘𝐷) = (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)))
34	33	oveq1d 7382	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)))
35		2cnd 12259	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ∈ ℂ)
36		2ne0 12285	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
37	36	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ≠ 0)
38	17, 35, 37	absdivd 15420	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / (abs‘2)))
39		2re 12255	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
40	39	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℝ)
41		0le2 12283	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 2
42	41	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 2)
43	40, 42	absidd 15385	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (abs‘2) = 2)
44	43	oveq2d 7383	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs‘𝐷) / (abs‘2)) = ((abs‘𝐷) / 2))
45	38, 44	eqtr2d 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs‘𝐷) / 2) = (abs‘(𝐷 / 2)))
46	45	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
47	20	rpcnd 12988	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℂ)
48	47, 47	pncand 11506	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) / 2))
49	34, 46, 48	3eqtr3rd 2780	. . . . . . . . . . . 12 ⊢ (𝜑 → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
50	49	3ad2ant1 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
51	45	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
52	51	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
53	52	oveq2d 7383	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) = ((abs‘𝐷) − ((abs‘𝐷) / 2)))
54	17	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝐷 ∈ ℂ)
55	54	abscld 15401	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) ∈ ℝ)
56	55	3adant3 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ∈ ℝ)
57	6	ffvelcdmda 7036	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ∈ ℂ)
58	57	3adant3 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐺‘𝑣) ∈ ℂ)
59	58	abscld 15401	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
60	17	3ad2ant1 1134	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → 𝐷 ∈ ℂ)
61	60, 58	subcld 11505	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐷 − (𝐺‘𝑣)) ∈ ℂ)
62	61	abscld 15401	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) ∈ ℝ)
63	59, 62	readdcld 11174	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))) ∈ ℝ)
64	56	rehalfcld 12424	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) ∈ ℝ)
65	59, 64	readdcld 11174	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)) ∈ ℝ)
66	57, 54	pncan3d 11508	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣))) = 𝐷)
67	66	eqcomd 2742	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝐷 = ((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣))))
68	67	fveq2d 6844	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) = (abs‘((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣)))))
69	54, 57	subcld 11505	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐷 − (𝐺‘𝑣)) ∈ ℂ)
70	57, 69	abstrid 15421	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣)))) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
71	68, 70	eqbrtrd 5107	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
72	71	3adant3 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
73	60, 58	abssubd 15418	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) = (abs‘((𝐺‘𝑣) − 𝐷)))
74		simp3 1139	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
75	73, 74	eqbrtrd 5107	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) < ((abs‘𝐷) / 2))
76	62, 64, 59, 75	ltadd2dd 11305	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))) < ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)))
77	56, 63, 65, 72, 76	lelttrd 11304	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) < ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)))
78	57	abscld 15401	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
79	78	3adant3 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
80	56, 64, 79	ltsubaddd 11746	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺‘𝑣)) ↔ (abs‘𝐷) < ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2))))
81	77, 80	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺‘𝑣)))
82	53, 81	eqbrtrd 5107	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) < (abs‘(𝐺‘𝑣)))
83	50, 82	eqbrtrd 5107	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
84	26, 27, 30, 83	syl3anc 1374	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
85	84	3exp1 1354	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺) → ((𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) → (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))))
86	85	ralimdv2 3146	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺) → (∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))))
87	86	reximdva 3150	. . . . . 6 ⊢ (𝜑 → (∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))))
88	25, 87	mpd 15	. . . . 5 ⊢ (𝜑 → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
89	88	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
90		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝑦 ∈ ℝ⁺)
91	17	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐷 ∈ ℂ)
92	18	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐷 ≠ 0)
93	91, 92	absrpcld 15413	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (abs‘𝐷) ∈ ℝ⁺)
94	93	rphalfcld 12998	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ((abs‘𝐷) / 2) ∈ ℝ⁺)
95	90, 94	rpmulcld 13002	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺)
96	95	ex 412	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ℝ⁺ → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
97	96	imdistani 568	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
98		eleq1 2824	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (𝑤 ∈ ℝ⁺ ↔ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
99	98	anbi2d 631	. . . . . . . . . 10 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((𝜑 ∧ 𝑤 ∈ ℝ⁺) ↔ (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺)))
100		breq2 5089	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((abs‘((𝐹‘𝑣) − 0)) < 𝑤 ↔ (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
101	100	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤) ↔ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
102	101	rexralbidv 3203	. . . . . . . . . 10 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤) ↔ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
103	99, 102	imbi12d 344	. . . . . . . . 9 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤)) ↔ ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))))
104	8, 7	fmptd 7066	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
105	104, 10, 13	ellimc3 25846	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 ∈ (𝐹 lim_ℂ 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤))))
106	9, 105	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤)))
107	106	simprd 495	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤))
108	107	r19.21bi 3229	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤))
109	103, 108	vtoclg 3499	. . . . . . . 8 ⊢ ((𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺ → ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
110	95, 97, 109	sylc 65	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
111	110	3ad2ant1 1134	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
112		simp12 1206	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑧 ∈ ℝ⁺)
113		simp2 1138	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑢 ∈ ℝ⁺)
114	112, 113	ifcld 4513	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ⁺)
115		nfv 1916	. . . . . . . . . . 11 ⊢ Ⅎ𝑣(𝜑 ∧ 𝑦 ∈ ℝ⁺)
116		nfv 1916	. . . . . . . . . . 11 ⊢ Ⅎ𝑣 𝑧 ∈ ℝ⁺
117		nfra1 3261	. . . . . . . . . . 11 ⊢ Ⅎ𝑣∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
118	115, 116, 117	nf3an 1903	. . . . . . . . . 10 ⊢ Ⅎ𝑣((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
119		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑣 𝑢 ∈ ℝ⁺
120		nfra1 3261	. . . . . . . . . 10 ⊢ Ⅎ𝑣∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))
121	118, 119, 120	nf3an 1903	. . . . . . . . 9 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
122		simp111 1304	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (𝜑 ∧ 𝑦 ∈ ℝ⁺))
123		simp112 1305	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ⁺)
124		simp12 1206	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ⁺)
125	122, 123, 124	jca31 514	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺))
126		simp2 1138	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑣 ∈ 𝐴)
127		simp3l 1203	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑣 ≠ 𝐸)
128	125, 126, 127	jca31 514	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸))
129	10	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐴 ⊆ ℂ)
130	129	3ad2ant1 1134	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → 𝐴 ⊆ ℂ)
131	130	3ad2ant1 1134	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐴 ⊆ ℂ)
132	131	3ad2ant1 1134	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝐴 ⊆ ℂ)
133	132, 126	sseldd 3922	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑣 ∈ ℂ)
134	13	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐸 ∈ ℂ)
135	134	3ad2ant1 1134	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → 𝐸 ∈ ℂ)
136	135	3ad2ant1 1134	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐸 ∈ ℂ)
137	136	3ad2ant1 1134	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝐸 ∈ ℂ)
138	133, 137	subcld 11505	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (𝑣 − 𝐸) ∈ ℂ)
139	138	abscld 15401	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) ∈ ℝ)
140	123	rpred 12986	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ)
141	124	rpred 12986	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ)
142	140, 141	ifcld 4513	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ)
143		simp3r 1204	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))
144		min1 13141	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑧)
145	140, 141, 144	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑧)
146	139, 142, 140, 143, 145	ltletrd 11306	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) < 𝑧)
147		simp113 1306	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
148		rspa 3226	. . . . . . . . . . . . 13 ⊢ ((∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ 𝑣 ∈ 𝐴) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
149	147, 126, 148	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
150	127, 146, 149	mp2and 700	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
151		simp13 1207	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
152		rspa 3226	. . . . . . . . . . . . 13 ⊢ ((∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
153	151, 126, 152	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
154		min2 13142	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑢)
155	140, 141, 154	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑢)
156	139, 142, 141, 143, 155	ltletrd 11306	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) < 𝑢)
157	127, 156	jca 511	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢))
158	122	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝜑)
159	158	3ad2ant1 1134	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → 𝜑)
160		simp12 1206	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → 𝑣 ∈ 𝐴)
161		nfv 1916	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑣 ∈ 𝐴)
162		nfmpt1 5184	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
163	7, 162	nfcxfr 2896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝐹
164		nfcv 2898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝑣
165	163, 164	nffv 6850	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥(𝐹‘𝑣)
166	165	nfel1 2915	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐹‘𝑣) ∈ ℂ
167	161, 166	nfim 1898	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)
168		eleq1 2824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑣 → (𝑥 ∈ 𝐴 ↔ 𝑣 ∈ 𝐴))
169	168	anbi2d 631	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑣 ∈ 𝐴)))
170		fveq2 6840	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
171	170	eleq1d 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) ∈ ℂ ↔ (𝐹‘𝑣) ∈ ℂ))
172	169, 171	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)))
173		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
174	7	fvmpt2 6959	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → (𝐹‘𝑥) = 𝐵)
175	173, 8, 174	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)
176	175, 8	eqeltrd 2836	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ)
177	167, 172, 176	chvarfv 2248	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)
178	177	subid1d 11494	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐹‘𝑣) − 0) = (𝐹‘𝑣))
179	178	eqcomd 2742	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) = ((𝐹‘𝑣) − 0))
180	179	fveq2d 6844	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐹‘𝑣)) = (abs‘((𝐹‘𝑣) − 0)))
181	159, 160, 180	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → (abs‘(𝐹‘𝑣)) = (abs‘((𝐹‘𝑣) − 0)))
182		simp3 1139	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢))
183		simp2 1138	. . . . . . . . . . . . . 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 15	. . . . . . . . . . . . 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 5107	. . . . . . . . . . . 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 1466	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
187		simp-7l 789	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
188		simp-4r 784	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣 ∈ 𝐴)
189		eldifsni 4735	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 ∈ (ℂ ∖ {0}) → 𝐶 ≠ 0)
190	3, 189	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0)
191	8, 4, 190	divcld 11931	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 𝐶) ∈ ℂ)
192		0ellimcdiv.h	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶))
193	191, 192	fmptd 7066	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐻:𝐴⟶ℂ)
194	193	ffvelcdmda 7036	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) ∈ ℂ)
195	194	subid1d 11494	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐻‘𝑣) − 0) = (𝐻‘𝑣))
196		nfmpt1 5184	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶))
197	192, 196	nfcxfr 2896	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝐻
198	197, 164	nffv 6850	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝐻‘𝑣)
199		nfcv 2898	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥 /
200		nfmpt1 5184	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐶)
201	5, 200	nfcxfr 2896	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝐺
202	201, 164	nffv 6850	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐺‘𝑣)
203	165, 199, 202	nfov 7397	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝐹‘𝑣) / (𝐺‘𝑣))
204	198, 203	nfeq 2912	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣))
205	161, 204	nfim 1898	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
206		fveq2 6840	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (𝐻‘𝑥) = (𝐻‘𝑣))
207		fveq2 6840	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → (𝐺‘𝑥) = (𝐺‘𝑣))
208	170, 207	oveq12d 7385	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) / (𝐺‘𝑥)) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
209	206, 208	eqeq12d 2752	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑣 → ((𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥)) ↔ (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣))))
210	169, 209	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥))) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))))
211	192	fvmpt2 6959	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝐵 / 𝐶) ∈ ℂ) → (𝐻‘𝑥) = (𝐵 / 𝐶))
212	173, 191, 211	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = (𝐵 / 𝐶))
213	175	eqcomd 2742	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = (𝐹‘𝑥))
214	5	fvmpt2 6959	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ (ℂ ∖ {0})) → (𝐺‘𝑥) = 𝐶)
215	173, 3, 214	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = 𝐶)
216	215	eqcomd 2742	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 = (𝐺‘𝑥))
217	213, 216	oveq12d 7385	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 𝐶) = ((𝐹‘𝑥) / (𝐺‘𝑥)))
218	212, 217	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥)))
219	205, 210, 218	chvarfv 2248	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
220	195, 219	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐻‘𝑣) − 0) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
221	220	fveq2d 6844	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐻‘𝑣) − 0)) = (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))))
222	187, 188, 221	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻‘𝑣) − 0)) = (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))))
223		simp-6l 787	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝜑 ∧ 𝑦 ∈ ℝ⁺))
224	223, 188	jca 511	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴))
225		simplr 769	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
226		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
227		nfcv 2898	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥0
228	202, 227	nfne 3033	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐺‘𝑣) ≠ 0
229	161, 228	nfim 1898	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)
230	207	neeq1d 2991	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝐺‘𝑥) ≠ 0 ↔ (𝐺‘𝑣) ≠ 0))
231	169, 230	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≠ 0) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)))
232	215, 190	eqnetrd 2999	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≠ 0)
233	229, 231, 232	chvarfv 2248	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)
234	177, 57, 233	absdivd 15420	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
235	234	adantlr 716	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
236	235	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
237	177	abscld 15401	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐹‘𝑣)) ∈ ℝ)
238	57, 233	absne0d 15412	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ≠ 0)
239	237, 78, 238	redivcld 11983	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
240	239	adantlr 716	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
241	240	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
242		rpre 12951	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ⁺ → 𝑦 ∈ ℝ)
243	242	ad2antlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → 𝑦 ∈ ℝ)
244	20	rpred 12986	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ)
245	244	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘𝐷) / 2) ∈ ℝ)
246	243, 245	remulcld 11175	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
247	246	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
248	57, 233	absrpcld 15413	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
249	248	adantlr 716	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
250	249	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
251	247, 250	rerpdivcld 13017	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
252	243	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑦 ∈ ℝ)
253		simp-4l 783	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
254		simpllr 776	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣 ∈ 𝐴)
255	253, 254, 237	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹‘𝑣)) ∈ ℝ)
256		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
257	255, 247, 250, 256	ltdiv1dd 13043	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) < ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))))
258	243	recnd 11173	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → 𝑦 ∈ ℂ)
259	47	ad2antrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘𝐷) / 2) ∈ ℂ)
260	249	rpcnd 12988	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℂ)
261	238	adantlr 716	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ≠ 0)
262	258, 259, 260, 261	divassd 11966	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣)))))
263	262	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣)))))
264	245, 249	rerpdivcld 13017	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
265	264	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
266		1red 11145	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 1 ∈ ℝ)
267		simpllr 776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 𝑦 ∈ ℝ⁺)
268	244	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((abs‘𝐷) / 2) ∈ ℝ)
269		1rp 12946	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℝ⁺
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 1 ∈ ℝ⁺)
271	248	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
272	47	div1d 11923	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
273	272	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
274		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
275	273, 274	eqbrtrd 5107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / 1) < (abs‘(𝐺‘𝑣)))
276	268, 270, 271, 275	ltdiv23d 13053	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) < 1)
277	276	adantllr 720	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) < 1)
278	265, 266, 267, 277	ltmul2dd 13042	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣)))) < (𝑦 · 1))
279	263, 278	eqbrtrd 5107	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) < (𝑦 · 1))
280	258	mulridd 11162	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (𝑦 · 1) = 𝑦)
281	280	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (𝑦 · 1) = 𝑦)
282	279, 281	breqtrd 5111	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) < 𝑦)
283	282	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) < 𝑦)
284	241, 251, 252, 257, 283	lttrd 11307	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) < 𝑦)
285	236, 284	eqbrtrd 5107	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) < 𝑦)
286	224, 225, 226, 285	syl21anc 838	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) < 𝑦)
287	222, 286	eqbrtrd 5107	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)
288	128, 150, 186, 287	syl21anc 838	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)
289	288	3exp 1120	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
290	121, 289	ralrimi 3235	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
291		brimralrspcev 5146	. . . . . . . 8 ⊢ ((if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
292	114, 290, 291	syl2anc 585	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
293	292	rexlimdv3a 3142	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → (∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
294	111, 293	mpd 15	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
295	294	rexlimdv3a 3142	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
296	89, 295	mpd 15	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
297	296	ralrimiva 3129	. 2 ⊢ (𝜑 → ∀𝑦 ∈ ℝ⁺ ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
298	193, 10, 13	ellimc3 25846	. 2 ⊢ (𝜑 → (0 ∈ (𝐻 lim_ℂ 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))))
299	1, 297, 298	mpbir2and 714	1 ⊢ (𝜑 → 0 ∈ (𝐻 lim_ℂ 𝐸))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2932 ∀wral 3051 ∃wrex 3061 ∖ cdif 3886 ⊆ wss 3889 ifcif 4466 {csn 4567 class class class wbr 5085 ↦ cmpt 5166 dom cdm 5631 ⟶wf 6494 ‘cfv 6498 (class class class)co 7367 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 < clt 11179 ≤ cle 11180 − cmin 11377 / cdiv 11807 2c2 12236 ℝ⁺crp 12942 abscabs 15196 lim_ℂ climc 25829

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-er 8643 df-map 8775 df-pm 8776 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fi 9324 df-sup 9355 df-inf 9356 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-7 12249 df-8 12250 df-9 12251 df-n0 12438 df-z 12525 df-dec 12645 df-uz 12789 df-q 12899 df-rp 12943 df-xneg 13063 df-xadd 13064 df-xmul 13065 df-fz 13462 df-seq 13964 df-exp 14024 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198 df-struct 17117 df-slot 17152 df-ndx 17164 df-base 17180 df-plusg 17233 df-mulr 17234 df-starv 17235 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-rest 17385 df-topn 17386 df-topgen 17406 df-psmet 21344 df-xmet 21345 df-met 21346 df-bl 21347 df-mopn 21348 df-cnfld 21353 df-top 22859 df-topon 22876 df-topsp 22898 df-bases 22911 df-cnp 23193 df-xms 24285 df-ms 24286 df-limc 25833

This theorem is referenced by: reclimc 46081

W3C validator