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 39881

Description: If the numerator converges to 0 and the denominator converges to non zero 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 10033	. 2 ⊢ (𝜑 → 0 ∈ ℂ)
2		0ellimcdiv.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (𝐺 lim_ℂ 𝐸))
3		0ellimcdiv.c	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ (ℂ ∖ {0}))
4	3	eldifad 3586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
5		0ellimcdiv.g	. . . . . . . . . . 11 ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)
6	4, 5	fmptd 6385	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:𝐴⟶ℂ)
7		0ellimcdiv.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
8		0ellimcdiv.b	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)
9		0ellimcdiv.0limf	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ (𝐹 lim_ℂ 𝐸))
10	7, 8, 9	limcmptdm 39867	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
11		limcrcl 23638	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (𝐺 lim_ℂ 𝐸) → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
12	2, 11	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺:dom 𝐺⟶ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ))
13	12	simp3d 1075	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ ℂ)
14	6, 10, 13	ellimc3 23643	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 ∈ (𝐺 lim_ℂ 𝐸) ↔ (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦))))
15	2, 14	mpbid 222	. . . . . . . 8 ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦)))
16	15	simprd 479	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦))
17	15	simpld 475	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℂ)
18		0ellimcdiv.dne0	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 0)
19	17, 18	absrpcld 14187	. . . . . . . 8 ⊢ (𝜑 → (abs‘𝐷) ∈ ℝ⁺)
20	19	rphalfcld 11884	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ⁺)
21		breq2 4657	. . . . . . . . . 10 ⊢ (𝑦 = ((abs‘𝐷) / 2) → ((abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦 ↔ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
22	21	imbi2d 330	. . . . . . . . 9 ⊢ (𝑦 = ((abs‘𝐷) / 2) → (((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ↔ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
23	22	rexralbidv 3058	. . . . . . . 8 ⊢ (𝑦 = ((abs‘𝐷) / 2) → (∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ↔ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))))
24	23	rspccva 3308	. . . . . . 7 ⊢ ((∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < 𝑦) ∧ ((abs‘𝐷) / 2) ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
25	16, 20, 24	syl2anc 693	. . . . . 6 ⊢ (𝜑 → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)))
26		simpl1l 1112	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → 𝜑)
27		simpl3 1066	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → 𝑣 ∈ 𝐴)
28		simpr 477	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧))
29		simpl2 1065	. . . . . . . . . . 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 11874	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (abs‘𝐷) ∈ ℂ)
32	31	2halvesd 11278	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) = (abs‘𝐷))
33	32	eqcomd 2628	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘𝐷) = (((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)))
34	33	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)))
35		2cnd 11093	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ∈ ℂ)
36		2ne0 11113	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
37	36	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 2 ≠ 0)
38	17, 35, 37	absdivd 14194	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / (abs‘2)))
39		2re 11090	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
40	39	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℝ)
41		0le2 11111	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 2
42	41	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 2)
43	40, 42	absidd 14161	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (abs‘2) = 2)
44	43	oveq2d 6666	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs‘𝐷) / (abs‘2)) = ((abs‘𝐷) / 2))
45	38, 44	eqtr2d 2657	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs‘𝐷) / 2) = (abs‘(𝐷 / 2)))
46	45	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘𝐷) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
47	20	rpcnd 11874	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℂ)
48	47, 47	pncand 10393	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((abs‘𝐷) / 2) + ((abs‘𝐷) / 2)) − ((abs‘𝐷) / 2)) = ((abs‘𝐷) / 2))
49	34, 46, 48	3eqtr3rd 2665	. . . . . . . . . . . 12 ⊢ (𝜑 → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
50	49	3ad2ant1 1082	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) = ((abs‘𝐷) − (abs‘(𝐷 / 2))))
51	45	eqcomd 2628	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
52	51	3ad2ant1 1082	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 / 2)) = ((abs‘𝐷) / 2))
53	52	oveq2d 6666	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) = ((abs‘𝐷) − ((abs‘𝐷) / 2)))
54	17	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝐷 ∈ ℂ)
55	54	abscld 14175	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) ∈ ℝ)
56	55	3adant3 1081	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ∈ ℝ)
57	6	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ∈ ℂ)
58	57	3adant3 1081	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐺‘𝑣) ∈ ℂ)
59	58	abscld 14175	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
60	17	3ad2ant1 1082	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → 𝐷 ∈ ℂ)
61	60, 58	subcld 10392	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (𝐷 − (𝐺‘𝑣)) ∈ ℂ)
62	61	abscld 14175	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) ∈ ℝ)
63	59, 62	readdcld 10069	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))) ∈ ℝ)
64	56	rehalfcld 11279	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) ∈ ℝ)
65	59, 64	readdcld 10069	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)) ∈ ℝ)
66	57, 54	pncan3d 10395	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣))) = 𝐷)
67	66	eqcomd 2628	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝐷 = ((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣))))
68	67	fveq2d 6195	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) = (abs‘((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣)))))
69	54, 57	subcld 10392	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐷 − (𝐺‘𝑣)) ∈ ℂ)
70	57, 69	abstrid 14195	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐺‘𝑣) + (𝐷 − (𝐺‘𝑣)))) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
71	68, 70	eqbrtrd 4675	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘𝐷) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
72	71	3adant3 1081	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) ≤ ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))))
73	60, 58	abssubd 14192	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) = (abs‘((𝐺‘𝑣) − 𝐷)))
74		simp3 1063	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))
75	73, 74	eqbrtrd 4675	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐷 − (𝐺‘𝑣))) < ((abs‘𝐷) / 2))
76	62, 64, 59, 75	ltadd2dd 10196	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘(𝐺‘𝑣)) + (abs‘(𝐷 − (𝐺‘𝑣)))) < ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)))
77	56, 63, 65, 72, 76	lelttrd 10195	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘𝐷) < ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2)))
78	57	abscld 14175	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
79	78	3adant3 1081	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (abs‘(𝐺‘𝑣)) ∈ ℝ)
80	56, 64, 79	ltsubaddd 10623	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → (((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺‘𝑣)) ↔ (abs‘𝐷) < ((abs‘(𝐺‘𝑣)) + ((abs‘𝐷) / 2))))
81	77, 80	mpbird 247	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − ((abs‘𝐷) / 2)) < (abs‘(𝐺‘𝑣)))
82	53, 81	eqbrtrd 4675	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) − (abs‘(𝐷 / 2))) < (abs‘(𝐺‘𝑣)))
83	50, 82	eqbrtrd 4675	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴 ∧ (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
84	26, 27, 30, 83	syl3anc 1326	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ⁺) ∧ (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧)) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
85	84	3exp1 1283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺) → ((𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2))) → (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))))
86	85	ralimdv2 2961	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ⁺) → (∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))))
87	86	reximdva 3017	. . . . . 6 ⊢ (𝜑 → (∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → (abs‘((𝐺‘𝑣) − 𝐷)) < ((abs‘𝐷) / 2)) → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))))
88	25, 87	mpd 15	. . . . 5 ⊢ (𝜑 → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
89	88	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
90		simpr 477	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝑦 ∈ ℝ⁺)
91	17	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐷 ∈ ℂ)
92	18	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐷 ≠ 0)
93	91, 92	absrpcld 14187	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (abs‘𝐷) ∈ ℝ⁺)
94	93	rphalfcld 11884	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ((abs‘𝐷) / 2) ∈ ℝ⁺)
95	90, 94	rpmulcld 11888	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺)
96	95	ex 450	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ℝ⁺ → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
97	96	imdistani 726	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
98		eleq1 2689	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (𝑤 ∈ ℝ⁺ ↔ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺))
99	98	anbi2d 740	. . . . . . . . . 10 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((𝜑 ∧ 𝑤 ∈ ℝ⁺) ↔ (𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺)))
100		breq2 4657	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → ((abs‘((𝐹‘𝑣) − 0)) < 𝑤 ↔ (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
101	100	imbi2d 330	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤) ↔ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
102	101	rexralbidv 3058	. . . . . . . . . 10 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤) ↔ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))))
103	99, 102	imbi12d 334	. . . . . . . . 9 ⊢ (𝑤 = (𝑦 · ((abs‘𝐷) / 2)) → (((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤)) ↔ ((𝜑 ∧ (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))))
104	8, 7	fmptd 6385	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
105	104, 10, 13	ellimc3 23643	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 ∈ (𝐹 lim_ℂ 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤))))
106	9, 105	mpbid 222	. . . . . . . . . . 11 ⊢ (𝜑 → (0 ∈ ℂ ∧ ∀𝑤 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤)))
107	106	simprd 479	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤))
108	107	r19.21bi 2932	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < 𝑤))
109	103, 108	vtoclg 3266	. . . . . . . 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 1082	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → ∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
112		simp12 1092	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑧 ∈ ℝ⁺)
113		simp2 1062	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝑢 ∈ ℝ⁺)
114	112, 113	ifcld 4131	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ⁺)
115		nfv 1843	. . . . . . . . . . 11 ⊢ Ⅎ𝑣(𝜑 ∧ 𝑦 ∈ ℝ⁺)
116		nfv 1843	. . . . . . . . . . 11 ⊢ Ⅎ𝑣 𝑧 ∈ ℝ⁺
117		nfra1 2941	. . . . . . . . . . 11 ⊢ Ⅎ𝑣∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
118	115, 116, 117	nf3an 1831	. . . . . . . . . 10 ⊢ Ⅎ𝑣((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
119		nfv 1843	. . . . . . . . . 10 ⊢ Ⅎ𝑣 𝑢 ∈ ℝ⁺
120		nfra1 2941	. . . . . . . . . 10 ⊢ Ⅎ𝑣∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))
121	118, 119, 120	nf3an 1831	. . . . . . . . 9 ⊢ Ⅎ𝑣(((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
122		simp111 1190	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (𝜑 ∧ 𝑦 ∈ ℝ⁺))
123		simp112 1191	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ⁺)
124		simp12 1092	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ⁺)
125	122, 123, 124	jca31 557	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺))
126		simp2 1062	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑣 ∈ 𝐴)
127		simp3l 1089	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑣 ≠ 𝐸)
128	125, 126, 127	jca31 557	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸))
129	10	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐴 ⊆ ℂ)
130	129	3ad2ant1 1082	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → 𝐴 ⊆ ℂ)
131	130	3ad2ant1 1082	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐴 ⊆ ℂ)
132	131	3ad2ant1 1082	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝐴 ⊆ ℂ)
133	132, 126	sseldd 3604	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑣 ∈ ℂ)
134	13	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → 𝐸 ∈ ℂ)
135	134	3ad2ant1 1082	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → 𝐸 ∈ ℂ)
136	135	3ad2ant1 1082	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → 𝐸 ∈ ℂ)
137	136	3ad2ant1 1082	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝐸 ∈ ℂ)
138	133, 137	subcld 10392	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (𝑣 − 𝐸) ∈ ℂ)
139	138	abscld 14175	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) ∈ ℝ)
140	123	rpred 11872	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑧 ∈ ℝ)
141	124	rpred 11872	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝑢 ∈ ℝ)
142	140, 141	ifcld 4131	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ)
143		simp3r 1090	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))
144		min1 12020	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑧)
145	140, 141, 144	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑧)
146	139, 142, 140, 143, 145	ltletrd 10197	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) < 𝑧)
147		simp113 1192	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
148		rspa 2930	. . . . . . . . . . . . 13 ⊢ ((∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ 𝑣 ∈ 𝐴) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
149	147, 126, 148	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))))
150	127, 146, 149	mp2and 715	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
151		simp13 1093	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
152		rspa 2930	. . . . . . . . . . . . 13 ⊢ ((∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ 𝑣 ∈ 𝐴) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
153	151, 126, 152	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))))
154		min2 12021	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑢)
155	140, 141, 154	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ≤ 𝑢)
156	139, 142, 141, 143, 155	ltletrd 10197	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝑣 − 𝐸)) < 𝑢)
157	127, 156	jca 554	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢))
158	122	simpld 475	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → 𝜑)
159	158	3ad2ant1 1082	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → 𝜑)
160		simp12 1092	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → 𝑣 ∈ 𝐴)
161		nfv 1843	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑣 ∈ 𝐴)
162		nfmpt1 4747	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)
163	7, 162	nfcxfr 2762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝐹
164		nfcv 2764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥𝑣
165	163, 164	nffv 6198	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥(𝐹‘𝑣)
166	165	nfel1 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐹‘𝑣) ∈ ℂ
167	161, 166	nfim 1825	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)
168		eleq1 2689	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑣 → (𝑥 ∈ 𝐴 ↔ 𝑣 ∈ 𝐴))
169	168	anbi2d 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑣 ∈ 𝐴)))
170		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣))
171	170	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) ∈ ℂ ↔ (𝐹‘𝑣) ∈ ℂ))
172	169, 171	imbi12d 334	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)))
173		simpr 477	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
174	7	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → (𝐹‘𝑥) = 𝐵)
175	173, 8, 174	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)
176	175, 8	eqeltrd 2701	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ)
177	167, 172, 176	chvar 2262	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ)
178	177	subid1d 10381	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐹‘𝑣) − 0) = (𝐹‘𝑣))
179	178	eqcomd 2628	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) = ((𝐹‘𝑣) − 0))
180	179	fveq2d 6195	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐹‘𝑣)) = (abs‘((𝐹‘𝑣) − 0)))
181	159, 160, 180	syl2anc 693	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → (abs‘(𝐹‘𝑣)) = (abs‘((𝐹‘𝑣) − 0)))
182		simp3 1063	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) ∧ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢)) → (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢))
183		simp2 1062	. . . . . . . . . . . . . 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 4675	. . . . . . . . . . . 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 1426	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
187		simp-7l 812	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
188		simp-4r 807	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣 ∈ 𝐴)
189		eldifsni 4320	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 ∈ (ℂ ∖ {0}) → 𝐶 ≠ 0)
190	3, 189	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 0)
191	8, 4, 190	divcld 10801	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 𝐶) ∈ ℂ)
192		0ellimcdiv.h	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶))
193	191, 192	fmptd 6385	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐻:𝐴⟶ℂ)
194	193	ffvelrnda 6359	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) ∈ ℂ)
195	194	subid1d 10381	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐻‘𝑣) − 0) = (𝐻‘𝑣))
196		nfmpt1 4747	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ (𝐵 / 𝐶))
197	192, 196	nfcxfr 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝐻
198	197, 164	nffv 6198	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥(𝐻‘𝑣)
199		nfcv 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥 /
200		nfmpt1 4747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐶)
201	5, 200	nfcxfr 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥𝐺
202	201, 164	nffv 6198	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐺‘𝑣)
203	165, 199, 202	nfov 6676	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝐹‘𝑣) / (𝐺‘𝑣))
204	198, 203	nfeq 2776	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥(𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣))
205	161, 204	nfim 1825	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
206		fveq2 6191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (𝐻‘𝑥) = (𝐻‘𝑣))
207		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → (𝐺‘𝑥) = (𝐺‘𝑣))
208	170, 207	oveq12d 6668	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥) / (𝐺‘𝑥)) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
209	206, 208	eqeq12d 2637	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑣 → ((𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥)) ↔ (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣))))
210	169, 209	imbi12d 334	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥))) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))))
211	192	fvmpt2 6291	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝐵 / 𝐶) ∈ ℂ) → (𝐻‘𝑥) = (𝐵 / 𝐶))
212	173, 191, 211	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = (𝐵 / 𝐶))
213	175	eqcomd 2628	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = (𝐹‘𝑥))
214	5	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ (ℂ ∖ {0})) → (𝐺‘𝑥) = 𝐶)
215	173, 3, 214	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = 𝐶)
216	215	eqcomd 2628	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 = (𝐺‘𝑥))
217	213, 216	oveq12d 6668	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 / 𝐶) = ((𝐹‘𝑥) / (𝐺‘𝑥)))
218	212, 217	eqtrd 2656	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥)))
219	205, 210, 218	chvar 2262	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐻‘𝑣) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
220	195, 219	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐻‘𝑣) − 0) = ((𝐹‘𝑣) / (𝐺‘𝑣)))
221	220	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐻‘𝑣) − 0)) = (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))))
222	187, 188, 221	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻‘𝑣) − 0)) = (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))))
223		simp-6l 810	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝜑 ∧ 𝑦 ∈ ℝ⁺))
224	223, 188	jca 554	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴))
225		simplr 792	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
226		simpr 477	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
227		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑥0
228	202, 227	nfne 2894	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥(𝐺‘𝑣) ≠ 0
229	161, 228	nfim 1825	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)
230	207	neeq1d 2853	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑣 → ((𝐺‘𝑥) ≠ 0 ↔ (𝐺‘𝑣) ≠ 0))
231	169, 230	imbi12d 334	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≠ 0) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)))
232	215, 190	eqnetrd 2861	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ≠ 0)
233	229, 231, 232	chvar 2262	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) ≠ 0)
234	177, 57, 233	absdivd 14194	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
235	234	adantlr 751	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
236	235	ad2antrr 762	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) = ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))))
237	177	abscld 14175	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐹‘𝑣)) ∈ ℝ)
238	57, 233	absne0d 14186	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ≠ 0)
239	237, 78, 238	redivcld 10853	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
240	239	adantlr 751	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
241	240	ad2antrr 762	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
242		rpre 11839	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ⁺ → 𝑦 ∈ ℝ)
243	242	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → 𝑦 ∈ ℝ)
244	20	rpred 11872	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((abs‘𝐷) / 2) ∈ ℝ)
245	244	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘𝐷) / 2) ∈ ℝ)
246	243, 245	remulcld 10070	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
247	246	ad2antrr 762	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (𝑦 · ((abs‘𝐷) / 2)) ∈ ℝ)
248	57, 233	absrpcld 14187	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
249	248	adantlr 751	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
250	249	ad2antrr 762	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
251	247, 250	rerpdivcld 11903	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
252	243	ad2antrr 762	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑦 ∈ ℝ)
253		simp-4l 806	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝜑)
254		simpllr 799	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → 𝑣 ∈ 𝐴)
255	253, 254, 237	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹‘𝑣)) ∈ ℝ)
256		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2)))
257	255, 247, 250, 256	ltdiv1dd 11929	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) < ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))))
258	243	recnd 10068	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → 𝑦 ∈ ℂ)
259	47	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((abs‘𝐷) / 2) ∈ ℂ)
260	249	rpcnd 11874	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ∈ ℂ)
261	238	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (abs‘(𝐺‘𝑣)) ≠ 0)
262	258, 259, 260, 261	divassd 10836	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣)))))
263	262	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) = (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣)))))
264	245, 249	rerpdivcld 11903	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
265	264	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) ∈ ℝ)
266		1red 10055	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 1 ∈ ℝ)
267		simpllr 799	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 𝑦 ∈ ℝ⁺)
268	244	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((abs‘𝐷) / 2) ∈ ℝ)
269		1rp 11836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℝ⁺
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → 1 ∈ ℝ⁺)
271	248	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (abs‘(𝐺‘𝑣)) ∈ ℝ⁺)
272	47	div1d 10793	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
273	272	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / 1) = ((abs‘𝐷) / 2))
274		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))
275	273, 274	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / 1) < (abs‘(𝐺‘𝑣)))
276	268, 270, 271, 275	ltdiv23d 11937	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) < 1)
277	276	adantllr 755	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣))) < 1)
278	265, 266, 267, 277	ltmul2dd 11928	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (𝑦 · (((abs‘𝐷) / 2) / (abs‘(𝐺‘𝑣)))) < (𝑦 · 1))
279	263, 278	eqbrtrd 4675	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) < (𝑦 · 1))
280	258	mulid1d 10057	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) → (𝑦 · 1) = 𝑦)
281	280	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → (𝑦 · 1) = 𝑦)
282	279, 281	breqtrd 4679	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) < 𝑦)
283	282	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((𝑦 · ((abs‘𝐷) / 2)) / (abs‘(𝐺‘𝑣))) < 𝑦)
284	241, 251, 252, 257, 283	lttrd 10198	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → ((abs‘(𝐹‘𝑣)) / (abs‘(𝐺‘𝑣))) < 𝑦)
285	236, 284	eqbrtrd 4675	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) < 𝑦)
286	224, 225, 226, 285	syl21anc 1325	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐹‘𝑣) / (𝐺‘𝑣))) < 𝑦)
287	222, 286	eqbrtrd 4675	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺) ∧ 𝑢 ∈ ℝ⁺) ∧ 𝑣 ∈ 𝐴) ∧ 𝑣 ≠ 𝐸) ∧ ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) ∧ (abs‘(𝐹‘𝑣)) < (𝑦 · ((abs‘𝐷) / 2))) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)
288	128, 150, 186, 287	syl21anc 1325	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) ∧ 𝑣 ∈ 𝐴 ∧ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)
289	288	3exp 1264	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → (𝑣 ∈ 𝐴 → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
290	121, 289	ralrimi 2957	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
291		breq2 4657	. . . . . . . . . . . 12 ⊢ (𝑤 = if(𝑧 ≤ 𝑢, 𝑧, 𝑢) → ((abs‘(𝑣 − 𝐸)) < 𝑤 ↔ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)))
292	291	anbi2d 740	. . . . . . . . . . 11 ⊢ (𝑤 = if(𝑧 ≤ 𝑢, 𝑧, 𝑢) → ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) ↔ (𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢))))
293	292	imbi1d 331	. . . . . . . . . 10 ⊢ (𝑤 = if(𝑧 ≤ 𝑢, 𝑧, 𝑢) → (((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦) ↔ ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
294	293	ralbidv 2986	. . . . . . . . 9 ⊢ (𝑤 = if(𝑧 ≤ 𝑢, 𝑧, 𝑢) → (∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦) ↔ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
295	294	rspcev 3309	. . . . . . . 8 ⊢ ((if(𝑧 ≤ 𝑢, 𝑧, 𝑢) ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < if(𝑧 ≤ 𝑢, 𝑧, 𝑢)) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
296	114, 290, 295	syl2anc 693	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2)))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
297	296	rexlimdv3a 3033	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → (∃𝑢 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑢) → (abs‘((𝐹‘𝑣) − 0)) < (𝑦 · ((abs‘𝐷) / 2))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
298	111, 297	mpd 15	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ⁺) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣)))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
299	298	rexlimdv3a 3033	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (∃𝑧 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑧) → ((abs‘𝐷) / 2) < (abs‘(𝐺‘𝑣))) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦)))
300	89, 299	mpd 15	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
301	300	ralrimiva 2966	. 2 ⊢ (𝜑 → ∀𝑦 ∈ ℝ⁺ ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))
302	193, 10, 13	ellimc3 23643	. 2 ⊢ (𝜑 → (0 ∈ (𝐻 lim_ℂ 𝐸) ↔ (0 ∈ ℂ ∧ ∀𝑦 ∈ ℝ⁺ ∃𝑤 ∈ ℝ⁺ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐸 ∧ (abs‘(𝑣 − 𝐸)) < 𝑤) → (abs‘((𝐻‘𝑣) − 0)) < 𝑦))))
303	1, 301, 302	mpbir2and 957	1 ⊢ (𝜑 → 0 ∈ (𝐻 lim_ℂ 𝐸))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 ∖ cdif 3571 ⊆ wss 3574 ifcif 4086 {csn 4177 class class class wbr 4653 ↦ cmpt 4729 dom cdm 5114 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ≤ cle 10075 − cmin 10266 / cdiv 10684 2c2 11070 ℝ⁺crp 11832 abscabs 13974 lim_ℂ climc 23626

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-fz 12327 df-seq 12802 df-exp 12861 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-plusg 15954 df-mulr 15955 df-starv 15956 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-rest 16083 df-topn 16084 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cnp 21032 df-xms 22125 df-ms 22126 df-limc 23630

This theorem is referenced by: reclimc 39885

W3C validator