lhop1

Description: L'Hôpital's Rule for limits from the right. If F and G are differentiable real functions on ( A , B ) , and F and G both approach 0 at A , and G ( x ) and G ' ( x ) are not zero on ( A , B ) , and the limit of F ' ( x ) / G ' ( x ) at A is C , then the limit F ( x ) / G ( x ) at A also exists and equals C . (Contributed by Mario Carneiro, 29-Dec-2016)

	Ref	Expression
Hypotheses	lhop1.a	$⊢ φ \to A \in ℝ$
	lhop1.b	$⊢ φ \to B \in ℝ^{*}$
	lhop1.l	$⊢ φ \to A < B$
	lhop1.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
	lhop1.g	$⊢ φ \to G : (A, B) ⟶ ℝ$
	lhop1.if	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
	lhop1.ig	$⊢ φ \to dom G_{ℝ}^{'} = (A, B)$
	lhop1.f0	$⊢ φ \to 0 \in (F {lim}_{ℂ} A)$
	lhop1.g0	$⊢ φ \to 0 \in (G {lim}_{ℂ} A)$
	lhop1.gn0	$⊢ φ \to \neg 0 \in ran G$
	lhop1.gd0	$⊢ φ \to \neg 0 \in ran G_{ℝ}^{'}$
	lhop1.c	$⊢ φ \to C \in ((z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} A)$
Assertion	lhop1	$⊢ φ \to C \in ((z \in (A, B) ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} A)$

Proof

Step	Hyp	Ref	Expression
1		lhop1.a	$⊢ φ \to A \in ℝ$
2		lhop1.b	$⊢ φ \to B \in ℝ^{*}$
3		lhop1.l	$⊢ φ \to A < B$
4		lhop1.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
5		lhop1.g	$⊢ φ \to G : (A, B) ⟶ ℝ$
6		lhop1.if	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
7		lhop1.ig	$⊢ φ \to dom G_{ℝ}^{'} = (A, B)$
8		lhop1.f0	$⊢ φ \to 0 \in (F {lim}_{ℂ} A)$
9		lhop1.g0	$⊢ φ \to 0 \in (G {lim}_{ℂ} A)$
10		lhop1.gn0	$⊢ φ \to \neg 0 \in ran G$
11		lhop1.gd0	$⊢ φ \to \neg 0 \in ran G_{ℝ}^{'}$
12		lhop1.c	$⊢ φ \to C \in ((z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} A)$
13		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
14	13	rphalfcld	$⊢ (φ \land x \in ℝ^{+}) \to \frac{x}{2} \in ℝ^{+}$
15		breq2	$⊢ e = \frac{x}{2} \to (\|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < e \leftrightarrow \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2})$
16	15	imbi2d	$⊢ e = \frac{x}{2} \to (((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < e) \leftrightarrow ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}))$
17	16	rexralbidv	$⊢ e = \frac{x}{2} \to (\exists d \in ℝ^{+} \forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < e) \leftrightarrow \exists d \in ℝ^{+} \forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}))$
18	17	rspcv	$⊢ \frac{x}{2} \in ℝ^{+} \to (\forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < e) \to \exists d \in ℝ^{+} \forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}))$
19	14 18	syl	$⊢ (φ \land x \in ℝ^{+}) \to (\forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < e) \to \exists d \in ℝ^{+} \forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}))$
20		rabid	$⊢ v \in \{v \in (A, B) \| \|v - A\| < d\} \leftrightarrow (v \in (A, B) \land \|v - A\| < d)$
21		eliooord	$⊢ v \in (A, B) \to (A < v \land v < B)$
22	21	adantl	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to (A < v \land v < B)$
23	22	simprd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to v < B$
24	23	biantrurd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to (v < d + A \leftrightarrow (v < B \land v < d + A))$
25		ioossre	$⊢ (A, B) \subseteq ℝ$
26		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to v \in (A, B)$
27	25 26	sseldi	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to v \in ℝ$
28	1	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to A \in ℝ$
29		simpr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to d \in ℝ^{+}$
30	29	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to d \in ℝ$
31	30	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to d \in ℝ$
32	27 28 31	ltsubaddd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to (v - A < d \leftrightarrow v < d + A)$
33	27	rexrd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to v \in ℝ^{*}$
34	2	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to B \in ℝ^{*}$
35	1	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to A \in ℝ$
36	30 35	readdcld	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to d + A \in ℝ$
37	36	rexrd	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to d + A \in ℝ^{*}$
38	37	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to d + A \in ℝ^{*}$
39		xrltmin	$⊢ (v \in ℝ^{} \land B \in ℝ^{} \land d + A \in ℝ^{*}) \to (v < if (B \leq d + A, B, d + A) \leftrightarrow (v < B \land v < d + A))$
40	33 34 38 39	syl3anc	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to (v < if (B \leq d + A, B, d + A) \leftrightarrow (v < B \land v < d + A))$
41	24 32 40	3bitr4rd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to (v < if (B \leq d + A, B, d + A) \leftrightarrow v - A < d)$
42	28	rexrd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to A \in ℝ^{*}$
43	34 38	ifcld	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to if (B \leq d + A, B, d + A) \in ℝ^{*}$
44	22	simpld	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to A < v$
45		elioo5	$⊢ (A \in ℝ^{} \land if (B \leq d + A, B, d + A) \in ℝ^{} \land v \in ℝ^{*}) \to (v \in (A, if (B \leq d + A, B, d + A)) \leftrightarrow (A < v \land v < if (B \leq d + A, B, d + A)))$
46	45	baibd	$⊢ ((A \in ℝ^{} \land if (B \leq d + A, B, d + A) \in ℝ^{} \land v \in ℝ^{*}) \land A < v) \to (v \in (A, if (B \leq d + A, B, d + A)) \leftrightarrow v < if (B \leq d + A, B, d + A))$
47	42 43 33 44 46	syl31anc	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to (v \in (A, if (B \leq d + A, B, d + A)) \leftrightarrow v < if (B \leq d + A, B, d + A))$
48	28 27 44	ltled	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to A \leq v$
49	28 27 48	abssubge0d	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to \|v - A\| = v - A$
50	49	breq1d	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to (\|v - A\| < d \leftrightarrow v - A < d)$
51	41 47 50	3bitr4d	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to (v \in (A, if (B \leq d + A, B, d + A)) \leftrightarrow \|v - A\| < d)$
52	51	rabbi2dva	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to (A, B) \cap (A, if (B \leq d + A, B, d + A)) = \{v \in (A, B) \| \|v - A\| < d\}$
53	2	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to B \in ℝ^{*}$
54		xrmin1	$⊢ (B \in ℝ^{} \land d + A \in ℝ^{}) \to if (B \leq d + A, B, d + A) \leq B$
55	53 37 54	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to if (B \leq d + A, B, d + A) \leq B$
56		iooss2	$⊢ (B \in ℝ^{*} \land if (B \leq d + A, B, d + A) \leq B) \to (A, if (B \leq d + A, B, d + A)) \subseteq (A, B)$
57	53 55 56	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to (A, if (B \leq d + A, B, d + A)) \subseteq (A, B)$
58		sseqin2	$⊢ (A, if (B \leq d + A, B, d + A)) \subseteq (A, B) \leftrightarrow (A, B) \cap (A, if (B \leq d + A, B, d + A)) = (A, if (B \leq d + A, B, d + A))$
59	57 58	sylib	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to (A, B) \cap (A, if (B \leq d + A, B, d + A)) = (A, if (B \leq d + A, B, d + A))$
60	52 59	eqtr3d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to \{v \in (A, B) \| \|v - A\| < d\} = (A, if (B \leq d + A, B, d + A))$
61	60	eleq2d	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to (v \in \{v \in (A, B) \| \|v - A\| < d\} \leftrightarrow v \in (A, if (B \leq d + A, B, d + A)))$
62	20 61	bitr3id	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to ((v \in (A, B) \land \|v - A\| < d) \leftrightarrow v \in (A, if (B \leq d + A, B, d + A)))$
63		lbioo	$⊢ \neg A \in (A, B)$
64		eleq1	$⊢ y = A \to (y \in (A, B) \leftrightarrow A \in (A, B))$
65	63 64	mtbiri	$⊢ y = A \to \neg y \in (A, B)$
66	65	necon2ai	$⊢ y \in (A, B) \to y \neq A$
67	66	biantrurd	$⊢ y \in (A, B) \to (\|y - A\| < d \leftrightarrow (y \neq A \land \|y - A\| < d))$
68	67	bicomd	$⊢ y \in (A, B) \to ((y \neq A \land \|y - A\| < d) \leftrightarrow \|y - A\| < d)$
69		fveq2	$⊢ z = y \to F_{ℝ}^{'} (z) = F_{ℝ}^{'} (y)$
70		fveq2	$⊢ z = y \to G_{ℝ}^{'} (z) = G_{ℝ}^{'} (y)$
71	69 70	oveq12d	$⊢ z = y \to \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)} = \frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}$
72		eqid	$⊢ (z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) = (z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)})$
73		ovex	$⊢ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)} \in V$
74	71 72 73	fvmpt3i	$⊢ y \in (A, B) \to (z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) = \frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}$
75	74	fvoveq1d	$⊢ y \in (A, B) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| = \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\|$
76	75	breq1d	$⊢ y \in (A, B) \to (\|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2} \leftrightarrow \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})$
77	68 76	imbi12d	$⊢ y \in (A, B) \to (((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \leftrightarrow (\|y - A\| < d \to \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2}))$
78	77	ralbiia	$⊢ \forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \leftrightarrow \forall y \in (A, B) (\|y - A\| < d \to \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})$
79		fvoveq1	$⊢ v = y \to \|v - A\| = \|y - A\|$
80	79	breq1d	$⊢ v = y \to (\|v - A\| < d \leftrightarrow \|y - A\| < d)$
81	80	ralrab	$⊢ \forall y \in \{v \in (A, B) \| \|v - A\| < d\} \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2} \leftrightarrow \forall y \in (A, B) (\|y - A\| < d \to \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})$
82	78 81	bitr4i	$⊢ \forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \leftrightarrow \forall y \in \{v \in (A, B) \| \|v - A\| < d\} \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2}$
83	60	adantrr	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A)))) \to \{v \in (A, B) \| \|v - A\| < d\} = (A, if (B \leq d + A, B, d + A))$
84	83	raleqdv	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A)))) \to (\forall y \in \{v \in (A, B) \| \|v - A\| < d\} \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2} \leftrightarrow \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})$
85	1	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to A \in ℝ$
86	2	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to B \in ℝ^{*}$
87	3	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to A < B$
88	4	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to F : (A, B) ⟶ ℝ$
89	5	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to G : (A, B) ⟶ ℝ$
90	6	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to dom F_{ℝ}^{'} = (A, B)$
91	7	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to dom G_{ℝ}^{'} = (A, B)$
92	8	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to 0 \in (F {lim}_{ℂ} A)$
93	9	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to 0 \in (G {lim}_{ℂ} A)$
94	10	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to \neg 0 \in ran G$
95	11	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to \neg 0 \in ran G_{ℝ}^{'}$
96	12	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to C \in ((z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} A)$
97	14	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to \frac{x}{2} \in ℝ^{+}$
98	85	rexrd	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to A \in ℝ^{*}$
99		simprll	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to d \in ℝ^{+}$
100	99	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to d \in ℝ$
101	100 85	readdcld	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to d + A \in ℝ$
102		iocssre	$⊢ (A \in ℝ^{*} \land d + A \in ℝ) \to (A, d + A] \subseteq ℝ$
103	98 101 102	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to (A, d + A] \subseteq ℝ$
104	86	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \land B \leq d + A) \to B \in ℝ^{*}$
105	100	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \land \neg B \leq d + A) \to d \in ℝ$
106	85	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \land \neg B \leq d + A) \to A \in ℝ$
107	105 106	readdcld	$⊢ (((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \land \neg B \leq d + A) \to d + A \in ℝ$
108	107	rexrd	$⊢ (((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \land \neg B \leq d + A) \to d + A \in ℝ^{*}$
109	104 108	ifclda	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to if (B \leq d + A, B, d + A) \in ℝ^{*}$
110	85 99	ltaddrp2d	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to A < d + A$
111	101	rexrd	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to d + A \in ℝ^{*}$
112		xrltmin	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land d + A \in ℝ^{*}) \to (A < if (B \leq d + A, B, d + A) \leftrightarrow (A < B \land A < d + A))$
113	98 86 111 112	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to (A < if (B \leq d + A, B, d + A) \leftrightarrow (A < B \land A < d + A))$
114	87 110 113	mpbir2and	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to A < if (B \leq d + A, B, d + A)$
115		xrmin2	$⊢ (B \in ℝ^{} \land d + A \in ℝ^{}) \to if (B \leq d + A, B, d + A) \leq d + A$
116	86 111 115	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to if (B \leq d + A, B, d + A) \leq d + A$
117		elioc1	$⊢ (A \in ℝ^{} \land d + A \in ℝ^{}) \to (if (B \leq d + A, B, d + A) \in (A, d + A] \leftrightarrow (if (B \leq d + A, B, d + A) \in ℝ^{*} \land A < if (B \leq d + A, B, d + A) \land if (B \leq d + A, B, d + A) \leq d + A))$
118	98 111 117	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to (if (B \leq d + A, B, d + A) \in (A, d + A] \leftrightarrow (if (B \leq d + A, B, d + A) \in ℝ^{*} \land A < if (B \leq d + A, B, d + A) \land if (B \leq d + A, B, d + A) \leq d + A))$
119	109 114 116 118	mpbir3and	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to if (B \leq d + A, B, d + A) \in (A, d + A]$
120	103 119	sseldd	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to if (B \leq d + A, B, d + A) \in ℝ$
121	86 111 54	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to if (B \leq d + A, B, d + A) \leq B$
122		simprlr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to v \in (A, if (B \leq d + A, B, d + A))$
123		simprr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2}$
124		eqid	$⊢ A + (\frac{r}{2}) = A + (\frac{r}{2})$
125	85 86 87 88 89 90 91 92 93 94 95 96 97 120 121 122 123 124	lhop1lem	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to \|(\frac{F (v)}{G (v)}) - C\| < 2 (\frac{x}{2})$
126	13	rpcnd	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℂ$
127		2cnd	$⊢ (φ \land x \in ℝ^{+}) \to 2 \in ℂ$
128		2ne0	$⊢ 2 \neq 0$
129	128	a1i	$⊢ (φ \land x \in ℝ^{+}) \to 2 \neq 0$
130	126 127 129	divcan2d	$⊢ (φ \land x \in ℝ^{+}) \to 2 (\frac{x}{2}) = x$
131	130	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to 2 (\frac{x}{2}) = x$
132	125 131	breqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land ((d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A))) \land \forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2})) \to \|(\frac{F (v)}{G (v)}) - C\| < x$
133	132	expr	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A)))) \to (\forall y \in (A, if (B \leq d + A, B, d + A)) \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2} \to \|(\frac{F (v)}{G (v)}) - C\| < x)$
134	84 133	sylbid	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A)))) \to (\forall y \in \{v \in (A, B) \| \|v - A\| < d\} \|(\frac{F_{ℝ}^{'} (y)}{G_{ℝ}^{'} (y)}) - C\| < \frac{x}{2} \to \|(\frac{F (v)}{G (v)}) - C\| < x)$
135	82 134	syl5bi	$⊢ ((φ \land x \in ℝ^{+}) \land (d \in ℝ^{+} \land v \in (A, if (B \leq d + A, B, d + A)))) \to (\forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \to \|(\frac{F (v)}{G (v)}) - C\| < x)$
136	135	expr	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to (v \in (A, if (B \leq d + A, B, d + A)) \to (\forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \to \|(\frac{F (v)}{G (v)}) - C\| < x))$
137	62 136	sylbid	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to ((v \in (A, B) \land \|v - A\| < d) \to (\forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \to \|(\frac{F (v)}{G (v)}) - C\| < x))$
138	137	expdimp	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to (\|v - A\| < d \to (\forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \to \|(\frac{F (v)}{G (v)}) - C\| < x))$
139		fveq2	$⊢ z = v \to F (z) = F (v)$
140		fveq2	$⊢ z = v \to G (z) = G (v)$
141	139 140	oveq12d	$⊢ z = v \to \frac{F (z)}{G (z)} = \frac{F (v)}{G (v)}$
142		eqid	$⊢ (z \in (A, B) ⟼ \frac{F (z)}{G (z)}) = (z \in (A, B) ⟼ \frac{F (z)}{G (z)})$
143		ovex	$⊢ \frac{F (z)}{G (z)} \in V$
144	141 142 143	fvmpt3i	$⊢ v \in (A, B) \to (z \in (A, B) ⟼ \frac{F (z)}{G (z)}) (v) = \frac{F (v)}{G (v)}$
145	144	fvoveq1d	$⊢ v \in (A, B) \to \|(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) (v) - C\| = \|(\frac{F (v)}{G (v)}) - C\|$
146	145	breq1d	$⊢ v \in (A, B) \to (\|(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) (v) - C\| < x \leftrightarrow \|(\frac{F (v)}{G (v)}) - C\| < x)$
147	146	imbi2d	$⊢ v \in (A, B) \to ((\forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \to \|(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) (v) - C\| < x) \leftrightarrow (\forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \to \|(\frac{F (v)}{G (v)}) - C\| < x))$
148	147	adantl	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to ((\forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \to \|(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) (v) - C\| < x) \leftrightarrow (\forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \to \|(\frac{F (v)}{G (v)}) - C\| < x))$
149	138 148	sylibrd	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to (\|v - A\| < d \to (\forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \to \|(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) (v) - C\| < x))$
150	149	adantld	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to ((v \neq A \land \|v - A\| < d) \to (\forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \to \|(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) (v) - C\| < x))$
151	150	com23	$⊢ (((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \land v \in (A, B)) \to (\forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \to ((v \neq A \land \|v - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) (v) - C\| < x))$
152	151	ralrimdva	$⊢ ((φ \land x \in ℝ^{+}) \land d \in ℝ^{+}) \to (\forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \to \forall v \in (A, B) ((v \neq A \land \|v - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) (v) - C\| < x))$
153	152	reximdva	$⊢ (φ \land x \in ℝ^{+}) \to (\exists d \in ℝ^{+} \forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < \frac{x}{2}) \to \exists d \in ℝ^{+} \forall v \in (A, B) ((v \neq A \land \|v - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) (v) - C\| < x))$
154	19 153	syld	$⊢ (φ \land x \in ℝ^{+}) \to (\forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < e) \to \exists d \in ℝ^{+} \forall v \in (A, B) ((v \neq A \land \|v - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) (v) - C\| < x))$
155	154	ralrimdva	$⊢ φ \to (\forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < e) \to \forall x \in ℝ^{+} \exists d \in ℝ^{+} \forall v \in (A, B) ((v \neq A \land \|v - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) (v) - C\| < x))$
156	155	anim2d	$⊢ φ \to ((C \in ℂ \land \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < e)) \to (C \in ℂ \land \forall x \in ℝ^{+} \exists d \in ℝ^{+} \forall v \in (A, B) ((v \neq A \land \|v - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) (v) - C\| < x)))$
157		dvf	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
158	6	feq2d	$⊢ φ \to (F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \leftrightarrow F_{ℝ}^{'} : (A, B) ⟶ ℂ)$
159	157 158	mpbii	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
160	159	ffvelrnda	$⊢ (φ \land z \in (A, B)) \to F_{ℝ}^{'} (z) \in ℂ$
161		dvf	$⊢ G_{ℝ}^{'} : dom G_{ℝ}^{'} ⟶ ℂ$
162	7	feq2d	$⊢ φ \to (G_{ℝ}^{'} : dom G_{ℝ}^{'} ⟶ ℂ \leftrightarrow G_{ℝ}^{'} : (A, B) ⟶ ℂ)$
163	161 162	mpbii	$⊢ φ \to G_{ℝ}^{'} : (A, B) ⟶ ℂ$
164	163	ffvelrnda	$⊢ (φ \land z \in (A, B)) \to G_{ℝ}^{'} (z) \in ℂ$
165	11	adantr	$⊢ (φ \land z \in (A, B)) \to \neg 0 \in ran G_{ℝ}^{'}$
166	163	ffnd	$⊢ φ \to G_{ℝ}^{'} Fn (A, B)$
167		fnfvelrn	$⊢ (G_{ℝ}^{'} Fn (A, B) \land z \in (A, B)) \to G_{ℝ}^{'} (z) \in ran G_{ℝ}^{'}$
168	166 167	sylan	$⊢ (φ \land z \in (A, B)) \to G_{ℝ}^{'} (z) \in ran G_{ℝ}^{'}$
169		eleq1	$⊢ G_{ℝ}^{'} (z) = 0 \to (G_{ℝ}^{'} (z) \in ran G_{ℝ}^{'} \leftrightarrow 0 \in ran G_{ℝ}^{'})$
170	168 169	syl5ibcom	$⊢ (φ \land z \in (A, B)) \to (G_{ℝ}^{'} (z) = 0 \to 0 \in ran G_{ℝ}^{'})$
171	170	necon3bd	$⊢ (φ \land z \in (A, B)) \to (\neg 0 \in ran G_{ℝ}^{'} \to G_{ℝ}^{'} (z) \neq 0)$
172	165 171	mpd	$⊢ (φ \land z \in (A, B)) \to G_{ℝ}^{'} (z) \neq 0$
173	160 164 172	divcld	$⊢ (φ \land z \in (A, B)) \to \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)} \in ℂ$
174	173	fmpttd	$⊢ φ \to (z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) : (A, B) ⟶ ℂ$
175		ax-resscn	$⊢ ℝ \subseteq ℂ$
176	25 175	sstri	$⊢ (A, B) \subseteq ℂ$
177	176	a1i	$⊢ φ \to (A, B) \subseteq ℂ$
178	1	recnd	$⊢ φ \to A \in ℂ$
179	174 177 178	ellimc3	$⊢ φ \to (C \in ((z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} A) \leftrightarrow (C \in ℂ \land \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall y \in (A, B) ((y \neq A \land \|y - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) (y) - C\| < e)))$
180	4	ffvelrnda	$⊢ (φ \land z \in (A, B)) \to F (z) \in ℝ$
181	180	recnd	$⊢ (φ \land z \in (A, B)) \to F (z) \in ℂ$
182	5	ffvelrnda	$⊢ (φ \land z \in (A, B)) \to G (z) \in ℝ$
183	182	recnd	$⊢ (φ \land z \in (A, B)) \to G (z) \in ℂ$
184	10	adantr	$⊢ (φ \land z \in (A, B)) \to \neg 0 \in ran G$
185	5	ffnd	$⊢ φ \to G Fn (A, B)$
186		fnfvelrn	$⊢ (G Fn (A, B) \land z \in (A, B)) \to G (z) \in ran G$
187	185 186	sylan	$⊢ (φ \land z \in (A, B)) \to G (z) \in ran G$
188		eleq1	$⊢ G (z) = 0 \to (G (z) \in ran G \leftrightarrow 0 \in ran G)$
189	187 188	syl5ibcom	$⊢ (φ \land z \in (A, B)) \to (G (z) = 0 \to 0 \in ran G)$
190	189	necon3bd	$⊢ (φ \land z \in (A, B)) \to (\neg 0 \in ran G \to G (z) \neq 0)$
191	184 190	mpd	$⊢ (φ \land z \in (A, B)) \to G (z) \neq 0$
192	181 183 191	divcld	$⊢ (φ \land z \in (A, B)) \to \frac{F (z)}{G (z)} \in ℂ$
193	192	fmpttd	$⊢ φ \to (z \in (A, B) ⟼ \frac{F (z)}{G (z)}) : (A, B) ⟶ ℂ$
194	193 177 178	ellimc3	$⊢ φ \to (C \in ((z \in (A, B) ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} A) \leftrightarrow (C \in ℂ \land \forall x \in ℝ^{+} \exists d \in ℝ^{+} \forall v \in (A, B) ((v \neq A \land \|v - A\| < d) \to \|(z \in (A, B) ⟼ \frac{F (z)}{G (z)}) (v) - C\| < x)))$
195	156 179 194	3imtr4d	$⊢ φ \to (C \in ((z \in (A, B) ⟼ \frac{F_{ℝ}^{'} (z)}{G_{ℝ}^{'} (z)}) {lim}_{ℂ} A) \to C \in ((z \in (A, B) ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} A))$
196	12 195	mpd	$⊢ φ \to C \in ((z \in (A, B) ⟼ \frac{F (z)}{G (z)}) {lim}_{ℂ} A)$

Metamath Proof Explorer

Theorem lhop1

Proof