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 45605

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 11252	. 2 ⊢ (𝜑 → 0 ∈ ℂ)
2		0ellimcdiv.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (𝐺 lim_ℂ 𝐸))
3		0ellimcdiv.c	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖ {0}))
4	3	eldifad 3975	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
5		0ellimcdiv.g	. . . . . . . . . . 11 ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)
6	4, 5	fmptd 7134	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:𝐴⟶ℂ)
7		0ellimcdiv.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
8		0ellimcdiv.b	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
9		0ellimcdiv.0limf	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ (𝐹 lim_ℂ 𝐸))
10	7, 8, 9	limcmptdm 45591	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
11		limcrcl 25924	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (𝐺 lim_ℂ 𝐸) → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
12	2, 11	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
13	12	simp3d 1143	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℂ)
14	6, 10, 13	ellimc3 25929	. . . . . . . . 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 15484	. . . . . . . 8 ⊢ (𝜑 → (abs‘𝐷) ∈ ℝ⁺)
20	19	rphalfcld 13087	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ⁺)
21		breq2 5152	. . . . . . . . . 10 ⊢ (𝑦 = ((abs‘𝐷) / 2) → ((abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦 ↔ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
22	21	imbi2d 340	. . . . . . . . 9 ⊢ (𝑦 = ((abs‘𝐷) / 2) → (((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ↔ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
23	22	rexralbidv 3221	. . . . . . . 8 ⊢ (𝑦 = ((abs‘𝐷) / 2) → (∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ↔ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
24	23	rspccva 3621	. . . . . . 7 ⊢ ((∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ∧ ((abs‘𝐷) / 2) ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
25	16, 20, 24	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
26		simpl1l 1223	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → 𝜑)
27		simpl3 1192	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → 𝑣 ∈ 𝐴)
28		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧))
29		simpl2 1191	. . . . . . . . . . 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 13077	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (abs‘𝐷) ∈ ℂ)
32	31	2halvesd 12510	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) = (abs‘𝐷))
33	32	eqcomd 2741	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘𝐷) = (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)))
34	33	oveq1d 7446	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)))
35		2cnd 12342	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ∈ ℂ)
36		2ne0 12368	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
37	36	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ≠ 0)
38	17, 35, 37	absdivd 15491	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / (abs‘2)))
39		2re 12338	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
40	39	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℝ)
41		0le2 12366	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 2
42	41	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 2)
43	40, 42	absidd 15458	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (abs‘2) = 2)
44	43	oveq2d 7447	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs‘𝐷) / (abs‘2)) = ((abs‘𝐷) / 2))
45	38, 44	eqtr2d 2776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs‘𝐷) / 2) = (abs‘(𝐷 / 2)))
46	45	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
47	20	rpcnd 13077	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℂ)
48	47, 47	pncand 11619	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) / 2))
49	34, 46, 48	3eqtr3rd 2784	. . . . . . . . . . . 12 ⊢ (𝜑 → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
50	49	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
51	45	eqcomd 2741	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
52	51	3ad2ant1 1132	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
53	52	oveq2d 7447	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) = ((abs‘𝐷) − ((abs‘𝐷) / 2)))
54	17	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝐷 ∈ ℂ)
55	54	abscld 15472	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) ∈ ℝ)
56	55	3adant3 1131	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ∈ ℝ)
57	6	ffvelcdmda 7104	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ∈ ℂ)
58	57	3adant3 1131	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐺‘𝑣) ∈ ℂ)
59	58	abscld 15472	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
60	17	3ad2ant1 1132	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → 𝐷 ∈ ℂ)
61	60, 58	subcld 11618	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐷 − (𝐺‘𝑣)) ∈ ℂ)
62	61	abscld 15472	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) ∈ ℝ)
63	59, 62	readdcld 11288	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))) ∈ ℝ)
64	56	rehalfcld 12511	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) ∈ ℝ)
65	59, 64	readdcld 11288	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)) ∈ ℝ)
66	57, 54	pncan3d 11621	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣))) = 𝐷)
67	66	eqcomd 2741	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝐷 = ((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣))))
68	67	fveq2d 6911	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) = (abs‘((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣)))))
69	54, 57	subcld 11618	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐷 − (𝐺‘𝑣)) ∈ ℂ)
70	57, 69	abstrid 15492	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣)))) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
71	68, 70	eqbrtrd 5170	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
72	71	3adant3 1131	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
73	60, 58	abssubd 15489	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) = (abs‘((𝐺‘𝑣) − 𝐷)))
74		simp3 1137	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
75	73, 74	eqbrtrd 5170	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) < ((abs‘𝐷) / 2))
76	62, 64, 59, 75	ltadd2dd 11418	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))) < ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)))
77	56, 63, 65, 72, 76	lelttrd 11417	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) < ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)))
78	57	abscld 15472	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
79	78	3adant3 1131	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
80	56, 64, 79	ltsubaddd 11857	. . . . . . . . . . . . 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 5170	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) < (abs‘(𝐺‘𝑣)))
83	50, 82	eqbrtrd 5170	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
84	26, 27, 30, 83	syl3anc 1370	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
85	84	3exp1 1351	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺) → ((𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) → (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))))
86	85	ralimdv2 3161	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺) → (∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))))
87	86	reximdva 3166	. . . . . 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 15484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (abs‘𝐷) ∈ ℝ⁺)
94	93	rphalfcld 13087	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ((abs‘𝐷) / 2) ∈ ℝ⁺)
95	90, 94	rpmulcld 13091	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺)
96	95	ex 412	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ℝ⁺ → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
97	96	imdistani 568	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
98		eleq1 2827	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (𝑤 ∈ ℝ⁺ ↔ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
99	98	anbi2d 630	. . . . . . . . . 10 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((𝜑 ∧ 𝑤 ∈ ℝ⁺) ↔ (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺)))
100		breq2 5152	. . . . . . . . . . . 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 3221	. . . . . . . . . 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 7134	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
105	104, 10, 13	ellimc3 25929	. . . . . . . . . . . 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 3249	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤))
109	103, 108	vtoclg 3554	. . . . . . . 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 1132	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
112		simp12 1203	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑧 ∈ ℝ⁺)
113		simp2 1136	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑢 ∈ ℝ⁺)
114	112, 113	ifcld 4577	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ⁺)
115		nfv 1912	. . . . . . . . . . 11 ⊢ Ⅎ𝑣(𝜑 ∧ 𝑦 ∈ ℝ⁺)
116		nfv 1912	. . . . . . . . . . 11 ⊢ Ⅎ𝑣 𝑧 ∈ ℝ⁺
117		nfra1 3282	. . . . . . . . . . 11 ⊢ Ⅎ𝑣∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
118	115, 116, 117	nf3an 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑣((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
119		nfv 1912	. . . . . . . . . 10 ⊢ Ⅎ𝑣 𝑢 ∈ ℝ⁺
120		nfra1 3282	. . . . . . . . . 10 ⊢ Ⅎ𝑣∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))
121	118, 119, 120	nf3an 1899	. . . . . . . . 9 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
122		simp111 1301	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (𝜑 ∧ 𝑦 ∈ ℝ⁺))
123		simp112 1302	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ⁺)
124		simp12 1203	. . . . . . . . . . . . 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 1136	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑣 ∈ 𝐴)
127		simp3l 1200	. . . . . . . . . . . 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 1132	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → 𝐴 ⊆ ℂ)
131	130	3ad2ant1 1132	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐴 ⊆ ℂ)
132	131	3ad2ant1 1132	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝐴 ⊆ ℂ)
133	132, 126	sseldd 3996	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑣 ∈ ℂ)
134	13	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐸 ∈ ℂ)
135	134	3ad2ant1 1132	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → 𝐸 ∈ ℂ)
136	135	3ad2ant1 1132	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐸 ∈ ℂ)
137	136	3ad2ant1 1132	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝐸 ∈ ℂ)
138	133, 137	subcld 11618	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (𝑣 − 𝐸) ∈ ℂ)
139	138	abscld 15472	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) ∈ ℝ)
140	123	rpred 13075	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ)
141	124	rpred 13075	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ)
142	140, 141	ifcld 4577	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ)
143		simp3r 1201	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))
144		min1 13228	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑧)
145	140, 141, 144	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑧)
146	139, 142, 140, 143, 145	ltletrd 11419	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) < 𝑧)
147		simp113 1303	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
148		rspa 3246	. . . . . . . . . . . . 13 ⊢ ((∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ 𝑣 ∈ 𝐴) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
149	147, 126, 148	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
150	127, 146, 149	mp2and 699	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
151		simp13 1204	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
152		rspa 3246	. . . . . . . . . . . . 13 ⊢ ((∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
153	151, 126, 152	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
154		min2 13229	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑢)
155	140, 141, 154	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑢)
156	139, 142, 141, 143, 155	ltletrd 11419	. . . . . . . . . . . . 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 1132	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → 𝜑)
160		simp12 1203	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → 𝑣 ∈ 𝐴)
161		nfv 1912	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑣 ∈ 𝐴)
162		nfmpt1 5256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
163	7, 162	nfcxfr 2901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝐹
164		nfcv 2903	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝑣
165	163, 164	nffv 6917	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥(𝐹‘𝑣)
166	165	nfel1 2920	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐹‘𝑣) ∈ ℂ
167	161, 166	nfim 1894	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)
168		eleq1 2827	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑣 → (𝑥 ∈ 𝐴 ↔ 𝑣 ∈ 𝐴))
169	168	anbi2d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑣 ∈ 𝐴)))
170		fveq2 6907	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
171	170	eleq1d 2824	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) ∈ ℂ ↔ (𝐹‘𝑣) ∈ ℂ))
172	169, 171	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)))
173		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
174	7	fvmpt2 7027	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → (𝐹‘𝑥) = 𝐵)
175	173, 8, 174	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)
176	175, 8	eqeltrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ)
177	167, 172, 176	chvarfv 2238	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)
178	177	subid1d 11607	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐹‘𝑣) − 0) = (𝐹‘𝑣))
179	178	eqcomd 2741	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) = ((𝐹‘𝑣) − 0))
180	179	fveq2d 6911	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐹‘𝑣)) = (abs‘((𝐹‘𝑣) − 0)))
181	159, 160, 180	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → (abs‘(𝐹‘𝑣)) = (abs‘((𝐹‘𝑣) − 0)))
182		simp3 1137	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢))
183		simp2 1136	. . . . . . . . . . . . . 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 5170	. . . . . . . . . . . 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 1462	. . . . . . . . . . 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 4795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 ∈ (ℂ ∖ {0}) → 𝐶 ≠ 0)
190	3, 189	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0)
191	8, 4, 190	divcld 12041	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 𝐶) ∈ ℂ)
192		0ellimcdiv.h	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶))
193	191, 192	fmptd 7134	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐻:𝐴⟶ℂ)
194	193	ffvelcdmda 7104	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) ∈ ℂ)
195	194	subid1d 11607	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐻‘𝑣) − 0) = (𝐻‘𝑣))
196		nfmpt1 5256	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶))
197	192, 196	nfcxfr 2901	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝐻
198	197, 164	nffv 6917	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝐻‘𝑣)
199		nfcv 2903	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥 /
200		nfmpt1 5256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐶)
201	5, 200	nfcxfr 2901	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝐺
202	201, 164	nffv 6917	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐺‘𝑣)
203	165, 199, 202	nfov 7461	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝐹‘𝑣) / (𝐺‘𝑣))
204	198, 203	nfeq 2917	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣))
205	161, 204	nfim 1894	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
206		fveq2 6907	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (𝐻‘𝑥) = (𝐻‘𝑣))
207		fveq2 6907	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → (𝐺‘𝑥) = (𝐺‘𝑣))
208	170, 207	oveq12d 7449	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) / (𝐺‘𝑥)) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
209	206, 208	eqeq12d 2751	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑣 → ((𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥)) ↔ (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣))))
210	169, 209	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥))) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))))
211	192	fvmpt2 7027	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝐵 / 𝐶) ∈ ℂ) → (𝐻‘𝑥) = (𝐵 / 𝐶))
212	173, 191, 211	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = (𝐵 / 𝐶))
213	175	eqcomd 2741	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = (𝐹‘𝑥))
214	5	fvmpt2 7027	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ (ℂ ∖ {0})) → (𝐺‘𝑥) = 𝐶)
215	173, 3, 214	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = 𝐶)
216	215	eqcomd 2741	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 = (𝐺‘𝑥))
217	213, 216	oveq12d 7449	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 𝐶) = ((𝐹‘𝑥) / (𝐺‘𝑥)))
218	212, 217	eqtrd 2775	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥)))
219	205, 210, 218	chvarfv 2238	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
220	195, 219	eqtrd 2775	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐻‘𝑣) − 0) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
221	220	fveq2d 6911	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐻‘𝑣) − 0)) = (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))))
222	187, 188, 221	syl2anc 584	. . . . . . . . . . . 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 2903	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥0
228	202, 227	nfne 3041	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐺‘𝑣) ≠ 0
229	161, 228	nfim 1894	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)
230	207	neeq1d 2998	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝐺‘𝑥) ≠ 0 ↔ (𝐺‘𝑣) ≠ 0))
231	169, 230	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≠ 0) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)))
232	215, 190	eqnetrd 3006	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≠ 0)
233	229, 231, 232	chvarfv 2238	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)
234	177, 57, 233	absdivd 15491	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
235	234	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
236	235	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
237	177	abscld 15472	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐹‘𝑣)) ∈ ℝ)
238	57, 233	absne0d 15483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ≠ 0)
239	237, 78, 238	redivcld 12093	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
240	239	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
241	240	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
242		rpre 13041	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ⁺ → 𝑦 ∈ ℝ)
243	242	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → 𝑦 ∈ ℝ)
244	20	rpred 13075	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ)
245	244	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘𝐷) / 2) ∈ ℝ)
246	243, 245	remulcld 11289	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
247	246	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
248	57, 233	absrpcld 15484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
249	248	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
250	249	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
251	247, 250	rerpdivcld 13106	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
252	243	ad2antrr 726	. . . . . . . . . . . . . . 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 584	. . . . . . . . . . . . . . . 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 13132	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) < ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))))
258	243	recnd 11287	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → 𝑦 ∈ ℂ)
259	47	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘𝐷) / 2) ∈ ℂ)
260	249	rpcnd 13077	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℂ)
261	238	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ≠ 0)
262	258, 259, 260, 261	divassd 12076	. . . . . . . . . . . . . . . . . . 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 13106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
265	264	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
266		1red 11260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 1 ∈ ℝ)
267		simpllr 776	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 𝑦 ∈ ℝ⁺)
268	244	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((abs‘𝐷) / 2) ∈ ℝ)
269		1rp 13036	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℝ⁺
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 1 ∈ ℝ⁺)
271	248	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
272	47	div1d 12033	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
273	272	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
274		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
275	273, 274	eqbrtrd 5170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / 1) < (abs‘(𝐺‘𝑣)))
276	268, 270, 271, 275	ltdiv23d 13142	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) < 1)
277	276	adantllr 719	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) < 1)
278	265, 266, 267, 277	ltmul2dd 13131	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣)))) < (𝑦 · 1))
279	263, 278	eqbrtrd 5170	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) < (𝑦 · 1))
280	258	mulridd 11276	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (𝑦 · 1) = 𝑦)
281	280	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (𝑦 · 1) = 𝑦)
282	279, 281	breqtrd 5174	. . . . . . . . . . . . . . . 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 11420	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) < 𝑦)
285	236, 284	eqbrtrd 5170	. . . . . . . . . . . . 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 5170	. . . . . . . . . . 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 1118	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
290	121, 289	ralrimi 3255	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
291		brimralrspcev 5209	. . . . . . . 8 ⊢ ((if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
292	114, 290, 291	syl2anc 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
293	292	rexlimdv3a 3157	. . . . . 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 3157	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
296	89, 295	mpd 15	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
297	296	ralrimiva 3144	. 2 ⊢ (𝜑 → ∀𝑦 ∈ ℝ⁺ ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
298	193, 10, 13	ellimc3 25929	. 2 ⊢ (𝜑 → (0 ∈ (𝐻 lim_ℂ 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))))
299	1, 297, 298	mpbir2and 713	1 ⊢ (𝜑 → 0 ∈ (𝐻 lim_ℂ 𝐸))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1537 ∈ wcel 2106 ≠ wne 2938 ∀wral 3059 ∃wrex 3068 ∖ cdif 3960 ⊆ wss 3963 ifcif 4531 {csn 4631 class class class wbr 5148 ↦ cmpt 5231 dom cdm 5689 ⟶wf 6559 ‘cfv 6563 (class class class)co 7431 ℂcc 11151 ℝcr 11152 0cc0 11153 1c1 11154 + caddc 11156 · cmul 11158 < clt 11293 ≤ cle 11294 − cmin 11490 / cdiv 11918 2c2 12319 ℝ⁺crp 13032 abscabs 15270 lim_ℂ climc 25912

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230 ax-pre-sup 11231

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-tp 4636 df-op 4638 df-uni 4913 df-int 4952 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8013 df-2nd 8014 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-1o 8505 df-er 8744 df-map 8867 df-pm 8868 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-fi 9449 df-sup 9480 df-inf 9481 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-div 11919 df-nn 12265 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 df-n0 12525 df-z 12612 df-dec 12732 df-uz 12877 df-q 12989 df-rp 13033 df-xneg 13152 df-xadd 13153 df-xmul 13154 df-fz 13545 df-seq 14040 df-exp 14100 df-cj 15135 df-re 15136 df-im 15137 df-sqrt 15271 df-abs 15272 df-struct 17181 df-slot 17216 df-ndx 17228 df-base 17246 df-plusg 17311 df-mulr 17312 df-starv 17313 df-tset 17317 df-ple 17318 df-ds 17320 df-unif 17321 df-rest 17469 df-topn 17470 df-topgen 17490 df-psmet 21374 df-xmet 21375 df-met 21376 df-bl 21377 df-mopn 21378 df-cnfld 21383 df-top 22916 df-topon 22933 df-topsp 22955 df-bases 22969 df-cnp 23252 df-xms 24346 df-ms 24347 df-limc 25916

This theorem is referenced by: reclimc 45609

W3C validator