0ellimcdiv

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)

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

Proof

Step	Hyp	Ref	Expression
1		0ellimcdiv.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		0ellimcdiv.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
3		0ellimcdiv.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 / 𝐶 ) )
4		0ellimcdiv.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
5		0ellimcdiv.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ( ℂ ∖ { 0 } ) )
6		0ellimcdiv.0limf	⊢ ( 𝜑 → 0 ∈ ( 𝐹 lim_ℂ 𝐸 ) )
7		0ellimcdiv.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐺 lim_ℂ 𝐸 ) )
8		0ellimcdiv.dne0	⊢ ( 𝜑 → 𝐷 ≠ 0 )
9		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
10	5	eldifad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
11	10 2	fmptd	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ℂ )
12	1 4 6	limcmptdm	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
13		limcrcl	⊢ ( 𝐷 ∈ ( 𝐺 lim_ℂ 𝐸 ) → ( 𝐺 : dom 𝐺 ⟶ ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ ) )
14	7 13	syl	⊢ ( 𝜑 → ( 𝐺 : dom 𝐺 ⟶ ℂ ∧ dom 𝐺 ⊆ ℂ ∧ 𝐸 ∈ ℂ ) )
15	14	simp3d	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
16	11 12 15	ellimc3	⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝐺 lim_ℂ 𝐸 ) ↔ ( 𝐷 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < 𝑦 ) ) ) )
17	7 16	mpbid	⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < 𝑦 ) ) )
18	17	simprd	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < 𝑦 ) )
19	17	simpld	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
20	19 8	absrpcld	⊢ ( 𝜑 → ( abs ‘ 𝐷 ) ∈ ℝ⁺ )
21	20	rphalfcld	⊢ ( 𝜑 → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℝ⁺ )
22		breq2	⊢ ( 𝑦 = ( ( abs ‘ 𝐷 ) / 2 ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) )
23	22	imbi2d	⊢ ( 𝑦 = ( ( abs ‘ 𝐷 ) / 2 ) → ( ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < 𝑦 ) ↔ ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
24	23	rexralbidv	⊢ ( 𝑦 = ( ( abs ‘ 𝐷 ) / 2 ) → ( ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < 𝑦 ) ↔ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
25	24	rspccva	⊢ ( ( ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < 𝑦 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℝ⁺ ) → ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) )
26	18 21 25	syl2anc	⊢ ( 𝜑 → ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) )
27		simpl1l	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ) ∧ ( 𝑣 ∈ 𝐴 → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) ) → 𝜑 )
28		simpl3	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ) ∧ ( 𝑣 ∈ 𝐴 → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) ) → 𝑣 ∈ 𝐴 )
29		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ) ∧ ( 𝑣 ∈ 𝐴 → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) ) → ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) )
30		simpl2	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ) ∧ ( 𝑣 ∈ 𝐴 → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) ) → ( 𝑣 ∈ 𝐴 → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
31	28 29 30	mp2d	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ) ∧ ( 𝑣 ∈ 𝐴 → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) )
32	20	rpcnd	⊢ ( 𝜑 → ( abs ‘ 𝐷 ) ∈ ℂ )
33	32	2halvesd	⊢ ( 𝜑 → ( ( ( abs ‘ 𝐷 ) / 2 ) + ( ( abs ‘ 𝐷 ) / 2 ) ) = ( abs ‘ 𝐷 ) )
34	33	eqcomd	⊢ ( 𝜑 → ( abs ‘ 𝐷 ) = ( ( ( abs ‘ 𝐷 ) / 2 ) + ( ( abs ‘ 𝐷 ) / 2 ) ) )
35	34	oveq1d	⊢ ( 𝜑 → ( ( abs ‘ 𝐷 ) − ( ( abs ‘ 𝐷 ) / 2 ) ) = ( ( ( ( abs ‘ 𝐷 ) / 2 ) + ( ( abs ‘ 𝐷 ) / 2 ) ) − ( ( abs ‘ 𝐷 ) / 2 ) ) )
36		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
37		2ne0	⊢ 2 ≠ 0
38	37	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
39	19 36 38	absdivd	⊢ ( 𝜑 → ( abs ‘ ( 𝐷 / 2 ) ) = ( ( abs ‘ 𝐷 ) / ( abs ‘ 2 ) ) )
40		2re	⊢ 2 ∈ ℝ
41	40	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
42		0le2	⊢ 0 ≤ 2
43	42	a1i	⊢ ( 𝜑 → 0 ≤ 2 )
44	41 43	absidd	⊢ ( 𝜑 → ( abs ‘ 2 ) = 2 )
45	44	oveq2d	⊢ ( 𝜑 → ( ( abs ‘ 𝐷 ) / ( abs ‘ 2 ) ) = ( ( abs ‘ 𝐷 ) / 2 ) )
46	39 45	eqtr2d	⊢ ( 𝜑 → ( ( abs ‘ 𝐷 ) / 2 ) = ( abs ‘ ( 𝐷 / 2 ) ) )
47	46	oveq2d	⊢ ( 𝜑 → ( ( abs ‘ 𝐷 ) − ( ( abs ‘ 𝐷 ) / 2 ) ) = ( ( abs ‘ 𝐷 ) − ( abs ‘ ( 𝐷 / 2 ) ) ) )
48	21	rpcnd	⊢ ( 𝜑 → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℂ )
49	48 48	pncand	⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐷 ) / 2 ) + ( ( abs ‘ 𝐷 ) / 2 ) ) − ( ( abs ‘ 𝐷 ) / 2 ) ) = ( ( abs ‘ 𝐷 ) / 2 ) )
50	35 47 49	3eqtr3rd	⊢ ( 𝜑 → ( ( abs ‘ 𝐷 ) / 2 ) = ( ( abs ‘ 𝐷 ) − ( abs ‘ ( 𝐷 / 2 ) ) ) )
51	50	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ 𝐷 ) / 2 ) = ( ( abs ‘ 𝐷 ) − ( abs ‘ ( 𝐷 / 2 ) ) ) )
52	46	eqcomd	⊢ ( 𝜑 → ( abs ‘ ( 𝐷 / 2 ) ) = ( ( abs ‘ 𝐷 ) / 2 ) )
53	52	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ ( 𝐷 / 2 ) ) = ( ( abs ‘ 𝐷 ) / 2 ) )
54	53	oveq2d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ 𝐷 ) − ( abs ‘ ( 𝐷 / 2 ) ) ) = ( ( abs ‘ 𝐷 ) − ( ( abs ‘ 𝐷 ) / 2 ) ) )
55	19	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝐷 ∈ ℂ )
56	55	abscld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ 𝐷 ) ∈ ℝ )
57	56	3adant3	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ 𝐷 ) ∈ ℝ )
58	11	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑣 ) ∈ ℂ )
59	58	3adant3	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( 𝐺 ‘ 𝑣 ) ∈ ℂ )
60	59	abscld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ∈ ℝ )
61	19	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → 𝐷 ∈ ℂ )
62	61 59	subcld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( 𝐷 − ( 𝐺 ‘ 𝑣 ) ) ∈ ℂ )
63	62	abscld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ ( 𝐷 − ( 𝐺 ‘ 𝑣 ) ) ) ∈ ℝ )
64	60 63	readdcld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) + ( abs ‘ ( 𝐷 − ( 𝐺 ‘ 𝑣 ) ) ) ) ∈ ℝ )
65	57	rehalfcld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℝ )
66	60 65	readdcld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) + ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ )
67	58 55	pncan3d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑣 ) + ( 𝐷 − ( 𝐺 ‘ 𝑣 ) ) ) = 𝐷 )
68	67	eqcomd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝐷 = ( ( 𝐺 ‘ 𝑣 ) + ( 𝐷 − ( 𝐺 ‘ 𝑣 ) ) ) )
69	68	fveq2d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ 𝐷 ) = ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) + ( 𝐷 − ( 𝐺 ‘ 𝑣 ) ) ) ) )
70	55 58	subcld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐷 − ( 𝐺 ‘ 𝑣 ) ) ∈ ℂ )
71	58 70	abstrid	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) + ( 𝐷 − ( 𝐺 ‘ 𝑣 ) ) ) ) ≤ ( ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) + ( abs ‘ ( 𝐷 − ( 𝐺 ‘ 𝑣 ) ) ) ) )
72	69 71	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ 𝐷 ) ≤ ( ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) + ( abs ‘ ( 𝐷 − ( 𝐺 ‘ 𝑣 ) ) ) ) )
73	72	3adant3	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ 𝐷 ) ≤ ( ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) + ( abs ‘ ( 𝐷 − ( 𝐺 ‘ 𝑣 ) ) ) ) )
74	61 59	abssubd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ ( 𝐷 − ( 𝐺 ‘ 𝑣 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) )
75		simp3	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) )
76	74 75	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ ( 𝐷 − ( 𝐺 ‘ 𝑣 ) ) ) < ( ( abs ‘ 𝐷 ) / 2 ) )
77	63 65 60 76	ltadd2dd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) + ( abs ‘ ( 𝐷 − ( 𝐺 ‘ 𝑣 ) ) ) ) < ( ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) + ( ( abs ‘ 𝐷 ) / 2 ) ) )
78	57 64 66 73 77	lelttrd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ 𝐷 ) < ( ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) + ( ( abs ‘ 𝐷 ) / 2 ) ) )
79	58	abscld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ∈ ℝ )
80	79	3adant3	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ∈ ℝ )
81	57 65 80	ltsubaddd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( ( abs ‘ 𝐷 ) − ( ( abs ‘ 𝐷 ) / 2 ) ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ↔ ( abs ‘ 𝐷 ) < ( ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) + ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
82	78 81	mpbird	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ 𝐷 ) − ( ( abs ‘ 𝐷 ) / 2 ) ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) )
83	54 82	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ 𝐷 ) − ( abs ‘ ( 𝐷 / 2 ) ) ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) )
84	51 83	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) )
85	27 28 31 84	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ) ∧ ( 𝑣 ∈ 𝐴 → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) )
86	85	3exp1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ) → ( ( 𝑣 ∈ 𝐴 → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( 𝑣 ∈ 𝐴 → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ) )
87	86	ralimdv2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ⁺ ) → ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) )
88	87	reximdva	⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑣 ) − 𝐷 ) ) < ( ( abs ‘ 𝐷 ) / 2 ) ) → ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) )
89	26 88	mpd	⊢ ( 𝜑 → ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) )
90	89	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) )
91		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → 𝑦 ∈ ℝ⁺ )
92	19	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → 𝐷 ∈ ℂ )
93	8	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → 𝐷 ≠ 0 )
94	92 93	absrpcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( abs ‘ 𝐷 ) ∈ ℝ⁺ )
95	94	rphalfcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℝ⁺ )
96	91 95	rpmulcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ⁺ )
97	96	ex	⊢ ( 𝜑 → ( 𝑦 ∈ ℝ⁺ → ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ⁺ ) )
98	97	imdistani	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( 𝜑 ∧ ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ⁺ ) )
99		eleq1	⊢ ( 𝑤 = ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) → ( 𝑤 ∈ ℝ⁺ ↔ ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ⁺ ) )
100	99	anbi2d	⊢ ( 𝑤 = ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( 𝜑 ∧ 𝑤 ∈ ℝ⁺ ) ↔ ( 𝜑 ∧ ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ⁺ ) ) )
101		breq2	⊢ ( 𝑤 = ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < 𝑤 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
102	101	imbi2d	⊢ ( 𝑤 = ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < 𝑤 ) ↔ ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) )
103	102	rexralbidv	⊢ ( 𝑤 = ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < 𝑤 ) ↔ ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) )
104	100 103	imbi12d	⊢ ( 𝑤 = ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) → ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ⁺ ) → ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < 𝑤 ) ) ↔ ( ( 𝜑 ∧ ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ⁺ ) → ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ) )
105	4 1	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
106	105 12 15	ellimc3	⊢ ( 𝜑 → ( 0 ∈ ( 𝐹 lim_ℂ 𝐸 ) ↔ ( 0 ∈ ℂ ∧ ∀ 𝑤 ∈ ℝ⁺ ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < 𝑤 ) ) ) )
107	6 106	mpbid	⊢ ( 𝜑 → ( 0 ∈ ℂ ∧ ∀ 𝑤 ∈ ℝ⁺ ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < 𝑤 ) ) )
108	107	simprd	⊢ ( 𝜑 → ∀ 𝑤 ∈ ℝ⁺ ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < 𝑤 ) )
109	108	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ⁺ ) → ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < 𝑤 ) )
110	104 109	vtoclg	⊢ ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ⁺ → ( ( 𝜑 ∧ ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ⁺ ) → ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) )
111	96 98 110	sylc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
112	111	3ad2ant1	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) → ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
113		simp12	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → 𝑧 ∈ ℝ⁺ )
114		simp2	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → 𝑢 ∈ ℝ⁺ )
115	113 114	ifcld	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ∈ ℝ⁺ )
116		nfv	⊢ Ⅎ 𝑣 ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ )
117		nfv	⊢ Ⅎ 𝑣 𝑧 ∈ ℝ⁺
118		nfra1	⊢ Ⅎ 𝑣 ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) )
119	116 117 118	nf3an	⊢ Ⅎ 𝑣 ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) )
120		nfv	⊢ Ⅎ 𝑣 𝑢 ∈ ℝ⁺
121		nfra1	⊢ Ⅎ 𝑣 ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) )
122	119 120 121	nf3an	⊢ Ⅎ 𝑣 ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
123		simp111	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) )
124		simp112	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → 𝑧 ∈ ℝ⁺ )
125		simp12	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → 𝑢 ∈ ℝ⁺ )
126	123 124 125	jca31	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ) ∧ 𝑢 ∈ ℝ⁺ ) )
127		simp2	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → 𝑣 ∈ 𝐴 )
128		simp3l	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → 𝑣 ≠ 𝐸 )
129	126 127 128	jca31	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ) ∧ 𝑢 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑣 ≠ 𝐸 ) )
130	12	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → 𝐴 ⊆ ℂ )
131	130	3ad2ant1	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) → 𝐴 ⊆ ℂ )
132	131	3ad2ant1	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → 𝐴 ⊆ ℂ )
133	132	3ad2ant1	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → 𝐴 ⊆ ℂ )
134	133 127	sseldd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → 𝑣 ∈ ℂ )
135	15	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → 𝐸 ∈ ℂ )
136	135	3ad2ant1	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) → 𝐸 ∈ ℂ )
137	136	3ad2ant1	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → 𝐸 ∈ ℂ )
138	137	3ad2ant1	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → 𝐸 ∈ ℂ )
139	134 138	subcld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ( 𝑣 − 𝐸 ) ∈ ℂ )
140	139	abscld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ( abs ‘ ( 𝑣 − 𝐸 ) ) ∈ ℝ )
141	124	rpred	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → 𝑧 ∈ ℝ )
142	125	rpred	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → 𝑢 ∈ ℝ )
143	141 142	ifcld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ∈ ℝ )
144		simp3r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) )
145		min1	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ ) → if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ≤ 𝑧 )
146	141 142 145	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ≤ 𝑧 )
147	140 143 141 144 146	ltletrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 )
148		simp113	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) )
149		rspa	⊢ ( ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) )
150	148 127 149	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) )
151	128 147 150	mp2and	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) )
152		simp13	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
153		rspa	⊢ ( ( ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
154	152 127 153	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
155		min2	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ ) → if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ≤ 𝑢 )
156	141 142 155	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ≤ 𝑢 )
157	140 143 142 144 156	ltletrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 )
158	128 157	jca	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) )
159	123	simpld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → 𝜑 )
160	159	3ad2ant1	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) ∧ ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) ) → 𝜑 )
161		simp12	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) ∧ ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) ) → 𝑣 ∈ 𝐴 )
162		nfv	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑣 ∈ 𝐴 )
163		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
164	1 163	nfcxfr	⊢ Ⅎ 𝑥 𝐹
165		nfcv	⊢ Ⅎ 𝑥 𝑣
166	164 165	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑣 )
167	166	nfel1	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑣 ) ∈ ℂ
168	162 167	nfim	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑣 ) ∈ ℂ )
169		eleq1	⊢ ( 𝑥 = 𝑣 → ( 𝑥 ∈ 𝐴 ↔ 𝑣 ∈ 𝐴 ) )
170	169	anbi2d	⊢ ( 𝑥 = 𝑣 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ) )
171		fveq2	⊢ ( 𝑥 = 𝑣 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑣 ) )
172	171	eleq1d	⊢ ( 𝑥 = 𝑣 → ( ( 𝐹 ‘ 𝑥 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑣 ) ∈ ℂ ) )
173	170 172	imbi12d	⊢ ( 𝑥 = 𝑣 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑣 ) ∈ ℂ ) ) )
174		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
175	1	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℂ ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
176	174 4 175	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
177	176 4	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
178	168 173 177	chvarfv	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑣 ) ∈ ℂ )
179	178	subid1d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑣 ) − 0 ) = ( 𝐹 ‘ 𝑣 ) )
180	179	eqcomd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑣 ) = ( ( 𝐹 ‘ 𝑣 ) − 0 ) )
181	180	fveq2d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) )
182	160 161 181	syl2anc	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) ∧ ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) )
183		simp3	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) ∧ ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) ) → ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) )
184		simp2	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) ∧ ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) ) → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) )
185	183 184	mpd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) ∧ ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) )
186	182 185	eqbrtrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) ∧ ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) )
187	154 158 186	mpd3an23	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) )
188		simp-7l	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ) ∧ 𝑢 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑣 ≠ 𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → 𝜑 )
189		simp-4r	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ) ∧ 𝑢 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑣 ≠ 𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → 𝑣 ∈ 𝐴 )
190		eldifsni	⊢ ( 𝐶 ∈ ( ℂ ∖ { 0 } ) → 𝐶 ≠ 0 )
191	5 190	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≠ 0 )
192	4 10 191	divcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 / 𝐶 ) ∈ ℂ )
193	192 3	fmptd	⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ ℂ )
194	193	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑣 ) ∈ ℂ )
195	194	subid1d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑣 ) − 0 ) = ( 𝐻 ‘ 𝑣 ) )
196		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 / 𝐶 ) )
197	3 196	nfcxfr	⊢ Ⅎ 𝑥 𝐻
198	197 165	nffv	⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑣 )
199		nfcv	⊢ Ⅎ 𝑥 /
200		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
201	2 200	nfcxfr	⊢ Ⅎ 𝑥 𝐺
202	201 165	nffv	⊢ Ⅎ 𝑥 ( 𝐺 ‘ 𝑣 )
203	166 199 202	nfov	⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) )
204	198 203	nfeq	⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑣 ) = ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) )
205	162 204	nfim	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑣 ) = ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) )
206		fveq2	⊢ ( 𝑥 = 𝑣 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑣 ) )
207		fveq2	⊢ ( 𝑥 = 𝑣 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑣 ) )
208	171 207	oveq12d	⊢ ( 𝑥 = 𝑣 → ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) )
209	206 208	eqeq12d	⊢ ( 𝑥 = 𝑣 → ( ( 𝐻 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝐻 ‘ 𝑣 ) = ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) ) )
210	170 209	imbi12d	⊢ ( 𝑥 = 𝑣 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑣 ) = ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) ) ) )
211	3	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐵 / 𝐶 ) ∈ ℂ ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐵 / 𝐶 ) )
212	174 192 211	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐵 / 𝐶 ) )
213	176	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = ( 𝐹 ‘ 𝑥 ) )
214	2	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐺 ‘ 𝑥 ) = 𝐶 )
215	174 5 214	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = 𝐶 )
216	215	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 = ( 𝐺 ‘ 𝑥 ) )
217	213 216	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 / 𝐶 ) = ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) )
218	212 217	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) )
219	205 210 218	chvarfv	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑣 ) = ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) )
220	195 219	eqtrd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑣 ) − 0 ) = ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) )
221	220	fveq2d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) ) )
222	188 189 221	syl2anc	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ) ∧ 𝑢 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑣 ≠ 𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) ) )
223		simp-6l	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ) ∧ 𝑢 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑣 ≠ 𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) )
224	223 189	jca	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ) ∧ 𝑢 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑣 ≠ 𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) )
225		simplr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ) ∧ 𝑢 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑣 ≠ 𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) )
226		simpr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ) ∧ 𝑢 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑣 ≠ 𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) )
227		nfcv	⊢ Ⅎ 𝑥 0
228	202 227	nfne	⊢ Ⅎ 𝑥 ( 𝐺 ‘ 𝑣 ) ≠ 0
229	162 228	nfim	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑣 ) ≠ 0 )
230	207	neeq1d	⊢ ( 𝑥 = 𝑣 → ( ( 𝐺 ‘ 𝑥 ) ≠ 0 ↔ ( 𝐺 ‘ 𝑣 ) ≠ 0 ) )
231	170 230	imbi12d	⊢ ( 𝑥 = 𝑣 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ≠ 0 ) ↔ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑣 ) ≠ 0 ) ) )
232	215 191	eqnetrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ≠ 0 )
233	229 231 232	chvarfv	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑣 ) ≠ 0 )
234	178 58 233	absdivd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) )
235	234	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) )
236	235	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) )
237	178	abscld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) ∈ ℝ )
238	58 233	absne0d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ≠ 0 )
239	237 79 238	redivcld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∈ ℝ )
240	239	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∈ ℝ )
241	240	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∈ ℝ )
242		rpre	⊢ ( 𝑦 ∈ ℝ⁺ → 𝑦 ∈ ℝ )
243	242	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
244	21	rpred	⊢ ( 𝜑 → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℝ )
245	244	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℝ )
246	243 245	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) → ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ )
247	246	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ∈ ℝ )
248	58 233	absrpcld	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ∈ ℝ⁺ )
249	248	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ∈ ℝ⁺ )
250	249	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ∈ ℝ⁺ )
251	247 250	rerpdivcld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∈ ℝ )
252	243	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → 𝑦 ∈ ℝ )
253		simp-4l	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → 𝜑 )
254		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → 𝑣 ∈ 𝐴 )
255	253 254 237	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) ∈ ℝ )
256		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) )
257	255 247 250 256	ltdiv1dd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) < ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) )
258	243	recnd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) → 𝑦 ∈ ℂ )
259	48	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℂ )
260	249	rpcnd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ∈ ℂ )
261	238	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) → ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ≠ 0 )
262	258 259 260 261	divassd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) = ( 𝑦 · ( ( ( abs ‘ 𝐷 ) / 2 ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) )
263	262	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) = ( 𝑦 · ( ( ( abs ‘ 𝐷 ) / 2 ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) )
264	245 249	rerpdivcld	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) → ( ( ( abs ‘ 𝐷 ) / 2 ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∈ ℝ )
265	264	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → ( ( ( abs ‘ 𝐷 ) / 2 ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∈ ℝ )
266		1red	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → 1 ∈ ℝ )
267		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → 𝑦 ∈ ℝ⁺ )
268	244	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → ( ( abs ‘ 𝐷 ) / 2 ) ∈ ℝ )
269		1rp	⊢ 1 ∈ ℝ⁺
270	269	a1i	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → 1 ∈ ℝ⁺ )
271	248	adantr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ∈ ℝ⁺ )
272	48	div1d	⊢ ( 𝜑 → ( ( ( abs ‘ 𝐷 ) / 2 ) / 1 ) = ( ( abs ‘ 𝐷 ) / 2 ) )
273	272	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → ( ( ( abs ‘ 𝐷 ) / 2 ) / 1 ) = ( ( abs ‘ 𝐷 ) / 2 ) )
274		simpr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) )
275	273 274	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → ( ( ( abs ‘ 𝐷 ) / 2 ) / 1 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) )
276	268 270 271 275	ltdiv23d	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → ( ( ( abs ‘ 𝐷 ) / 2 ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) < 1 )
277	276	adantllr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → ( ( ( abs ‘ 𝐷 ) / 2 ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) < 1 )
278	265 266 267 277	ltmul2dd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → ( 𝑦 · ( ( ( abs ‘ 𝐷 ) / 2 ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) < ( 𝑦 · 1 ) )
279	263 278	eqbrtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) < ( 𝑦 · 1 ) )
280	258	mulid1d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) → ( 𝑦 · 1 ) = 𝑦 )
281	280	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → ( 𝑦 · 1 ) = 𝑦 )
282	279 281	breqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) < 𝑦 )
283	282	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) < 𝑦 )
284	241 251 252 257 283	lttrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) / ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) < 𝑦 )
285	236 284	eqbrtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) ) < 𝑦 )
286	224 225 226 285	syl21anc	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ) ∧ 𝑢 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑣 ≠ 𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) / ( 𝐺 ‘ 𝑣 ) ) ) < 𝑦 )
287	222 286	eqbrtrd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ) ∧ 𝑢 ∈ ℝ⁺ ) ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑣 ≠ 𝐸 ) ∧ ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑣 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) < 𝑦 )
288	129 151 187 287	syl21anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) < 𝑦 )
289	288	3exp	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → ( 𝑣 ∈ 𝐴 → ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) < 𝑦 ) ) )
290	122 289	ralrimi	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) < 𝑦 ) )
291		brimralrspcev	⊢ ( ( if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < if ( 𝑧 ≤ 𝑢 , 𝑧 , 𝑢 ) ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) < 𝑦 ) ) → ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) < 𝑦 ) )
292	115 290 291	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) ∧ 𝑢 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) ) → ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) < 𝑦 ) )
293	292	rexlimdv3a	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) → ( ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑢 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − 0 ) ) < ( 𝑦 · ( ( abs ‘ 𝐷 ) / 2 ) ) ) → ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) < 𝑦 ) ) )
294	112 293	mpd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑧 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) ) → ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) < 𝑦 ) )
295	294	rexlimdv3a	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑧 ) → ( ( abs ‘ 𝐷 ) / 2 ) < ( abs ‘ ( 𝐺 ‘ 𝑣 ) ) ) → ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) < 𝑦 ) ) )
296	90 295	mpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) < 𝑦 ) )
297	296	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) < 𝑦 ) )
298	193 12 15	ellimc3	⊢ ( 𝜑 → ( 0 ∈ ( 𝐻 lim_ℂ 𝐸 ) ↔ ( 0 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑣 ∈ 𝐴 ( ( 𝑣 ≠ 𝐸 ∧ ( abs ‘ ( 𝑣 − 𝐸 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑣 ) − 0 ) ) < 𝑦 ) ) ) )
299	9 297 298	mpbir2and	⊢ ( 𝜑 → 0 ∈ ( 𝐻 lim_ℂ 𝐸 ) )

Metamath Proof Explorer

Theorem 0ellimcdiv

Proof