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 46480

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 11226	. 2 ⊢ (𝜑 → 0 ∈ ℂ)
2		0ellimcdiv.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (𝐺 lim_ℂ 𝐸))
3		0ellimcdiv.c	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖ {0}))
4	3	eldifad 3911	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
5		0ellimcdiv.g	. . . . . . . . . . 11 ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)
6	4, 5	fmptd 7108	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:𝐴⟶ℂ)
7		0ellimcdiv.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
8		0ellimcdiv.b	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
9		0ellimcdiv.0limf	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ (𝐹 lim_ℂ 𝐸))
10	7, 8, 9	limcmptdm 46466	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
11		limcrcl 26104	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (𝐺 lim_ℂ 𝐸) → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
12	2, 11	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
13	12	simp3d 1162	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℂ)
14	6, 10, 13	ellimc3 26109	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 ∈ (𝐺 lim_ℂ 𝐸) ↔ (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦))))
15	2, 14	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦)))
16	15	simprd 501	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦))
17	15	simpld 500	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℂ)
18		0ellimcdiv.dne0	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 0)
19	17, 18	absrpcld 15541	. . . . . . . 8 ⊢ (𝜑 → (abs‘𝐷) ∈ ℝ⁺)
20	19	rphalfcld 13101	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ⁺)
21		breq2 5107	. . . . . . . . . 10 ⊢ (𝑦 = ((abs‘𝐷) / 2) → ((abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦 ↔ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
22	21	imbi2d 343	. . . . . . . . 9 ⊢ (𝑦 = ((abs‘𝐷) / 2) → (((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ↔ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
23	22	rexralbidv 3228	. . . . . . . 8 ⊢ (𝑦 = ((abs‘𝐷) / 2) → (∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ↔ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
24	23	rspccva 3575	. . . . . . 7 ⊢ ((∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ∧ ((abs‘𝐷) / 2) ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
25	16, 20, 24	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
26		simpl1l 1243	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → 𝜑)
27		simpl3 1212	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → 𝑣 ∈ 𝐴)
28		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧))
29		simpl2 1211	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
30	27, 28, 29	mp2d 50	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
31	19	rpcnd 13091	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (abs‘𝐷) ∈ ℂ)
32	31	2halvesd 12517	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) = (abs‘𝐷))
33	32	eqcomd 2766	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘𝐷) = (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)))
34	33	oveq1d 7429	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)))
35		2cnd 12346	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ∈ ℂ)
36		2ne0 12374	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
37	36	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ≠ 0)
38	17, 35, 37	absdivd 15548	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / (abs‘2)))
39		2re 12342	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
40	39	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℝ)
41		0le2 12370	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 2
42	41	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 2)
43	40, 42	absidd 15513	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (abs‘2) = 2)
44	43	oveq2d 7430	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs‘𝐷) / (abs‘2)) = ((abs‘𝐷) / 2))
45	38, 44	eqtr2d 2796	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs‘𝐷) / 2) = (abs‘(𝐷 / 2)))
46	45	oveq2d 7430	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
47	20	rpcnd 13091	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℂ)
48	47, 47	pncand 11597	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) / 2))
49	34, 46, 48	3eqtr3rd 2804	. . . . . . . . . . . 12 ⊢ (𝜑 → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
50	49	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
51	45	eqcomd 2766	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
52	51	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
53	52	oveq2d 7430	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) = ((abs‘𝐷) − ((abs‘𝐷) / 2)))
54	17	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝐷 ∈ ℂ)
55	54	abscld 15529	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) ∈ ℝ)
56	55	3adant3 1150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ∈ ℝ)
57	6	ffvelcdmda 7078	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ∈ ℂ)
58	57	3adant3 1150	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐺‘𝑣) ∈ ℂ)
59	58	abscld 15529	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
60	17	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → 𝐷 ∈ ℂ)
61	60, 58	subcld 11596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐷 − (𝐺‘𝑣)) ∈ ℂ)
62	61	abscld 15529	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) ∈ ℝ)
63	59, 62	readdcld 11265	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))) ∈ ℝ)
64	56	rehalfcld 12518	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) ∈ ℝ)
65	59, 64	readdcld 11265	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)) ∈ ℝ)
66	57, 54	pncan3d 11599	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣))) = 𝐷)
67	66	eqcomd 2766	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝐷 = ((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣))))
68	67	fveq2d 6883	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) = (abs‘((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣)))))
69	54, 57	subcld 11596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐷 − (𝐺‘𝑣)) ∈ ℂ)
70	57, 69	abstrid 15549	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣)))) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
71	68, 70	eqbrtrd 5127	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
72	71	3adant3 1150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
73	60, 58	abssubd 15546	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) = (abs‘((𝐺‘𝑣) − 𝐷)))
74		simp3 1156	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
75	73, 74	eqbrtrd 5127	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) < ((abs‘𝐷) / 2))
76	62, 64, 59, 75	ltadd2dd 11396	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))) < ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)))
77	56, 63, 65, 72, 76	lelttrd 11395	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) < ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)))
78	57	abscld 15529	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
79	78	3adant3 1150	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
80	56, 64, 79	ltsubaddd 11837	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺‘𝑣)) ↔ (abs‘𝐷) < ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2))))
81	77, 80	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺‘𝑣)))
82	53, 81	eqbrtrd 5127	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) < (abs‘(𝐺‘𝑣)))
83	50, 82	eqbrtrd 5127	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
84	26, 27, 30, 83	syl3anc 1398	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
85	84	3exp1 1371	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺) → ((𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) → (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))))
86	85	ralimdv2 3171	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺) → (∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))))
87	86	reximdva 3175	. . . . . 6 ⊢ (𝜑 → (∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))))
88	25, 87	mpd 16	. . . . 5 ⊢ (𝜑 → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
89	88	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
90		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝑦 ∈ ℝ⁺)
91	17	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐷 ∈ ℂ)
92	18	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐷 ≠ 0)
93	91, 92	absrpcld 15541	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (abs‘𝐷) ∈ ℝ⁺)
94	93	rphalfcld 13101	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ((abs‘𝐷) / 2) ∈ ℝ⁺)
95	90, 94	rpmulcld 13105	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺)
96	95	ex 418	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ℝ⁺ → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
97	96	imdistani 579	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
98		eleq1 2848	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (𝑤 ∈ ℝ⁺ ↔ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
99	98	anbi2d 642	. . . . . . . . . 10 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((𝜑 ∧ 𝑤 ∈ ℝ⁺) ↔ (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺)))
100		breq2 5107	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((abs‘((𝐹‘𝑣) − 0)) < 𝑤 ↔ (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
101	100	imbi2d 343	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤) ↔ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
102	101	rexralbidv 3228	. . . . . . . . . 10 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤) ↔ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
103	99, 102	imbi12d 347	. . . . . . . . 9 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤)) ↔ ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))))
104	8, 7	fmptd 7108	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
105	104, 10, 13	ellimc3 26109	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 ∈ (𝐹 lim_ℂ 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤))))
106	9, 105	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤)))
107	106	simprd 501	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤))
108	107	r19.21bi 3254	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤))
109	103, 108	vtoclg 3517	. . . . . . . 8 ⊢ ((𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺ → ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
110	95, 97, 109	sylc 66	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
111	110	3ad2ant1 1151	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
112		simp12 1223	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑧 ∈ ℝ⁺)
113		simp2 1155	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑢 ∈ ℝ⁺)
114	112, 113	ifcld 4529	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ⁺)
115		nfv 1947	. . . . . . . . . . 11 ⊢ Ⅎ𝑣(𝜑 ∧ 𝑦 ∈ ℝ⁺)
116		nfv 1947	. . . . . . . . . . 11 ⊢ Ⅎ𝑣 𝑧 ∈ ℝ⁺
117		nfra1 3286	. . . . . . . . . . 11 ⊢ Ⅎ𝑣∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
118	115, 116, 117	nf3an 1934	. . . . . . . . . 10 ⊢ Ⅎ𝑣((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
119		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑣 𝑢 ∈ ℝ⁺
120		nfra1 3286	. . . . . . . . . 10 ⊢ Ⅎ𝑣∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))
121	118, 119, 120	nf3an 1934	. . . . . . . . 9 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
122		simp111 1321	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (𝜑 ∧ 𝑦 ∈ ℝ⁺))
123		simp112 1322	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ⁺)
124		simp12 1223	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ⁺)
125	122, 123, 124	jca31 524	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺))
126		simp2 1155	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑣 ∈ 𝐴)
127		simp3l 1220	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑣 ≠ 𝐸)
128	125, 126, 127	jca31 524	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸))
129	10	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐴 ⊆ ℂ)
130	129	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → 𝐴 ⊆ ℂ)
131	130	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐴 ⊆ ℂ)
132	131	3ad2ant1 1151	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝐴 ⊆ ℂ)
133	132, 126	sseldd 3932	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑣 ∈ ℂ)
134	13	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐸 ∈ ℂ)
135	134	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → 𝐸 ∈ ℂ)
136	135	3ad2ant1 1151	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐸 ∈ ℂ)
137	136	3ad2ant1 1151	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝐸 ∈ ℂ)
138	133, 137	subcld 11596	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (𝑣 − 𝐸) ∈ ℂ)
139	138	abscld 15529	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) ∈ ℝ)
140	123	rpred 13089	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ)
141	124	rpred 13089	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ)
142	140, 141	ifcld 4529	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ)
143		simp3r 1221	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))
144		min1 13244	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑧)
145	140, 141, 144	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑧)
146	139, 142, 140, 143, 145	ltletrd 11397	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) < 𝑧)
147		simp113 1323	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
148		rspa 3251	. . . . . . . . . . . . 13 ⊢ ((∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ 𝑣 ∈ 𝐴) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
149	147, 126, 148	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
150	127, 146, 149	mp2and 712	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
151		simp13 1224	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
152		rspa 3251	. . . . . . . . . . . . 13 ⊢ ((∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
153	151, 126, 152	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
154		min2 13245	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑢)
155	140, 141, 154	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑢)
156	139, 142, 141, 143, 155	ltletrd 11397	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) < 𝑢)
157	127, 156	jca 521	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢))
158	122	simpld 500	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝜑)
159	158	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → 𝜑)
160		simp12 1223	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → 𝑣 ∈ 𝐴)
161		nfv 1947	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑣 ∈ 𝐴)
162		nfmpt1 5204	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
163	7, 162	nfcxfr 2920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝐹
164		nfcv 2922	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝑣
165	163, 164	nffv 6889	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥(𝐹‘𝑣)
166	165	nfel1 2938	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐹‘𝑣) ∈ ℂ
167	161, 166	nfim 1929	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)
168		eleq1 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑣 → (𝑥 ∈ 𝐴 ↔ 𝑣 ∈ 𝐴))
169	168	anbi2d 642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑣 ∈ 𝐴)))
170		fveq2 6879	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
171	170	eleq1d 2845	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) ∈ ℂ ↔ (𝐹‘𝑣) ∈ ℂ))
172	169, 171	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)))
173		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
174	7	fvmpt2 6999	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → (𝐹‘𝑥) = 𝐵)
175	173, 8, 174	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)
176	175, 8	eqeltrd 2860	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ)
177	167, 172, 176	chvarfv 2276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)
178	177	subid1d 11585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐹‘𝑣) − 0) = (𝐹‘𝑣))
179	178	eqcomd 2766	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) = ((𝐹‘𝑣) − 0))
180	179	fveq2d 6883	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐹‘𝑣)) = (abs‘((𝐹‘𝑣) − 0)))
181	159, 160, 180	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → (abs‘(𝐹‘𝑣)) = (abs‘((𝐹‘𝑣) − 0)))
182		simp3 1156	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢))
183		simp2 1155	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
184	182, 183	mpd 16	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))
185	181, 184	eqbrtrd 5127	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
186	153, 157, 185	mpd3an23 1492	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
187		simp-7l 801	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
188		simp-4r 796	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣 ∈ 𝐴)
189		eldifsni 4753	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 ∈ (ℂ ∖ {0}) → 𝐶 ≠ 0)
190	3, 189	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0)
191	8, 4, 190	divcld 12018	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 𝐶) ∈ ℂ)
192		0ellimcdiv.h	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶))
193	191, 192	fmptd 7108	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐻:𝐴⟶ℂ)
194	193	ffvelcdmda 7078	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) ∈ ℂ)
195	194	subid1d 11585	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐻‘𝑣) − 0) = (𝐻‘𝑣))
196		nfmpt1 5204	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶))
197	192, 196	nfcxfr 2920	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝐻
198	197, 164	nffv 6889	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝐻‘𝑣)
199		nfcv 2922	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥 /
200		nfmpt1 5204	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐶)
201	5, 200	nfcxfr 2920	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝐺
202	201, 164	nffv 6889	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐺‘𝑣)
203	165, 199, 202	nfov 7444	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝐹‘𝑣) / (𝐺‘𝑣))
204	198, 203	nfeq 2935	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣))
205	161, 204	nfim 1929	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
206		fveq2 6879	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (𝐻‘𝑥) = (𝐻‘𝑣))
207		fveq2 6879	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → (𝐺‘𝑥) = (𝐺‘𝑣))
208	170, 207	oveq12d 7432	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) / (𝐺‘𝑥)) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
209	206, 208	eqeq12d 2776	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑣 → ((𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥)) ↔ (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣))))
210	169, 209	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥))) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))))
211	192	fvmpt2 6999	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝐵 / 𝐶) ∈ ℂ) → (𝐻‘𝑥) = (𝐵 / 𝐶))
212	173, 191, 211	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = (𝐵 / 𝐶))
213	175	eqcomd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = (𝐹‘𝑥))
214	5	fvmpt2 6999	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ (ℂ ∖ {0})) → (𝐺‘𝑥) = 𝐶)
215	173, 3, 214	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = 𝐶)
216	215	eqcomd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 = (𝐺‘𝑥))
217	213, 216	oveq12d 7432	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 𝐶) = ((𝐹‘𝑥) / (𝐺‘𝑥)))
218	212, 217	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥)))
219	205, 210, 218	chvarfv 2276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
220	195, 219	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐻‘𝑣) − 0) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
221	220	fveq2d 6883	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐻‘𝑣) − 0)) = (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))))
222	187, 188, 221	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻‘𝑣) − 0)) = (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))))
223		simp-6l 799	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝜑 ∧ 𝑦 ∈ ℝ⁺))
224	223, 188	jca 521	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴))
225		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
226		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
227		nfcv 2922	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥0
228	202, 227	nfne 3058	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐺‘𝑣) ≠ 0
229	161, 228	nfim 1929	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)
230	207	neeq1d 3014	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝐺‘𝑥) ≠ 0 ↔ (𝐺‘𝑣) ≠ 0))
231	169, 230	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≠ 0) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)))
232	215, 190	eqnetrd 3022	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≠ 0)
233	229, 231, 232	chvarfv 2276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)
234	177, 57, 233	absdivd 15548	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
235	234	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
236	235	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
237	177	abscld 15529	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐹‘𝑣)) ∈ ℝ)
238	57, 233	absne0d 15540	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ≠ 0)
239	237, 78, 238	redivcld 12070	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
240	239	adantlr 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
241	240	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
242		rpre 13054	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ⁺ → 𝑦 ∈ ℝ)
243	242	ad2antlr 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → 𝑦 ∈ ℝ)
244	20	rpred 13089	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ)
245	244	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘𝐷) / 2) ∈ ℝ)
246	243, 245	remulcld 11266	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
247	246	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
248	57, 233	absrpcld 15541	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
249	248	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
250	249	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
251	247, 250	rerpdivcld 13120	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
252	243	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑦 ∈ ℝ)
253		simp-4l 795	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
254		simpllr 788	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣 ∈ 𝐴)
255	253, 254, 237	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹‘𝑣)) ∈ ℝ)
256		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
257	255, 247, 250, 256	ltdiv1dd 13146	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) < ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))))
258	243	recnd 11264	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → 𝑦 ∈ ℂ)
259	47	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘𝐷) / 2) ∈ ℂ)
260	249	rpcnd 13091	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℂ)
261	238	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ≠ 0)
262	258, 259, 260, 261	divassd 12053	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣)))))
263	262	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣)))))
264	245, 249	rerpdivcld 13120	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
265	264	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
266		1red 11236	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 1 ∈ ℝ)
267		simpllr 788	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 𝑦 ∈ ℝ⁺)
268	244	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((abs‘𝐷) / 2) ∈ ℝ)
269		1rp 13049	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℝ⁺
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 1 ∈ ℝ⁺)
271	248	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
272	47	div1d 12010	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
273	272	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
274		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
275	273, 274	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / 1) < (abs‘(𝐺‘𝑣)))
276	268, 270, 271, 275	ltdiv23d 13156	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) < 1)
277	276	adantllr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) < 1)
278	265, 266, 267, 277	ltmul2dd 13145	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣)))) < (𝑦 · 1))
279	263, 278	eqbrtrd 5127	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) < (𝑦 · 1))
280	258	mulridd 11253	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (𝑦 · 1) = 𝑦)
281	280	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (𝑦 · 1) = 𝑦)
282	279, 281	breqtrd 5131	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) < 𝑦)
283	282	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) < 𝑦)
284	241, 251, 252, 257, 283	lttrd 11398	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) < 𝑦)
285	236, 284	eqbrtrd 5127	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) < 𝑦)
286	224, 225, 226, 285	syl21anc 851	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) < 𝑦)
287	222, 286	eqbrtrd 5127	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)
288	128, 150, 186, 287	syl21anc 851	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)
289	288	3exp 1137	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
290	121, 289	ralrimi 3260	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
291		brimralrspcev 5166	. . . . . . . 8 ⊢ ((if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
292	114, 290, 291	syl2anc 596	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
293	292	rexlimdv3a 3167	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → (∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
294	111, 293	mpd 16	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
295	294	rexlimdv3a 3167	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
296	89, 295	mpd 16	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
297	296	ralrimiva 3154	. 2 ⊢ (𝜑 → ∀𝑦 ∈ ℝ⁺ ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
298	193, 10, 13	ellimc3 26109	. 2 ⊢ (𝜑 → (0 ∈ (𝐻 lim_ℂ 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))))
299	1, 297, 298	mpbir2and 726	1 ⊢ (𝜑 → 0 ∈ (𝐻 lim_ℂ 𝐸))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 ∖ cdif 3896 ⊆ wss 3899 ifcif 4482 {csn 4584 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5655 ⟶wf 6529 ‘cfv 6533 (class class class)co 7414 ℂcc 11125 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 < clt 11270 ≤ cle 11271 − cmin 11468 / cdiv 11898 2c2 12322 ℝ⁺crp 13045 abscabs 15324 lim_ℂ climc 26092

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8458 df-er 8699 df-map 8831 df-pm 8832 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fi 9384 df-sup 9415 df-inf 9416 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-q 13001 df-rp 13046 df-xneg 13166 df-xadd 13167 df-xmul 13168 df-fz 13565 df-seq 14069 df-exp 14129 df-cj 15189 df-re 15190 df-im 15191 df-sqrt 15325 df-abs 15326 df-struct 17242 df-slot 17277 df-ndx 17289 df-base 17305 df-plusg 17358 df-mulr 17359 df-starv 17360 df-tset 17364 df-ple 17365 df-ds 17367 df-unif 17368 df-rest 17510 df-topn 17511 df-topgen 17531 df-psmet 21580 df-xmet 21581 df-met 21582 df-bl 21583 df-mopn 21584 df-cnfld 21589 df-top 23122 df-topon 23139 df-topsp 23161 df-bases 23174 df-cnp 23456 df-xms 24549 df-ms 24550 df-limc 26096

This theorem is used by: reclimc 46484

W3C validator