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	$⊢ F = (x \in A ⟼ B)$
	0ellimcdiv.g	$⊢ G = (x \in A ⟼ C)$
	0ellimcdiv.h	$⊢ H = (x \in A ⟼ \frac{B}{C})$
	0ellimcdiv.b	$⊢ (φ \land x \in A) \to B \in ℂ$
	0ellimcdiv.c	$⊢ (φ \land x \in A) \to C \in (ℂ ∖ \{0\})$
	0ellimcdiv.0limf	$⊢ φ \to 0 \in (F {lim}_{ℂ} E)$
	0ellimcdiv.d	$⊢ φ \to D \in (G {lim}_{ℂ} E)$
	0ellimcdiv.dne0	$⊢ φ \to D \neq 0$
Assertion	0ellimcdiv	$⊢ φ \to 0 \in (H {lim}_{ℂ} E)$

Proof

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

Metamath Proof Explorer

Theorem 0ellimcdiv

Proof