rlimdiv

Description: Limit of the quotient of two converging functions. Proposition 12-2.1(a) of Gleason p. 168. (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Hypotheses	rlimadd.3	$⊢ (φ \land x \in A) \to B \in V$
	rlimadd.4	$⊢ (φ \land x \in A) \to C \in V$
	rlimadd.5	$⊢ φ \to (x \in A ⟼ B) \underset{ℝ}{⇝} D$
	rlimadd.6	$⊢ φ \to (x \in A ⟼ C) \underset{ℝ}{⇝} E$
	rlimdiv.7	$⊢ φ \to E \neq 0$
	rlimdiv.8	$⊢ (φ \land x \in A) \to C \neq 0$
Assertion	rlimdiv	$⊢ φ \to (x \in A ⟼ \frac{B}{C}) \underset{ℝ}{⇝} (\frac{D}{E})$

Proof

Step	Hyp	Ref	Expression
1		rlimadd.3	$⊢ (φ \land x \in A) \to B \in V$
2		rlimadd.4	$⊢ (φ \land x \in A) \to C \in V$
3		rlimadd.5	$⊢ φ \to (x \in A ⟼ B) \underset{ℝ}{⇝} D$
4		rlimadd.6	$⊢ φ \to (x \in A ⟼ C) \underset{ℝ}{⇝} E$
5		rlimdiv.7	$⊢ φ \to E \neq 0$
6		rlimdiv.8	$⊢ (φ \land x \in A) \to C \neq 0$
7	1 3	rlimmptrcl	$⊢ (φ \land x \in A) \to B \in ℂ$
8	2 4	rlimmptrcl	$⊢ (φ \land x \in A) \to C \in ℂ$
9	8 6	reccld	$⊢ (φ \land x \in A) \to \frac{1}{C} \in ℂ$
10		eldifsn	$⊢ C \in (ℂ ∖ \{0\}) \leftrightarrow (C \in ℂ \land C \neq 0)$
11	8 6 10	sylanbrc	$⊢ (φ \land x \in A) \to C \in (ℂ ∖ \{0\})$
12	11	fmpttd	$⊢ φ \to (x \in A ⟼ C) : A ⟶ ℂ ∖ \{0\}$
13		rlimcl	$⊢ (x \in A ⟼ C) \underset{ℝ}{⇝} E \to E \in ℂ$
14	4 13	syl	$⊢ φ \to E \in ℂ$
15		eldifsn	$⊢ E \in (ℂ ∖ \{0\}) \leftrightarrow (E \in ℂ \land E \neq 0)$
16	14 5 15	sylanbrc	$⊢ φ \to E \in (ℂ ∖ \{0\})$
17		eldifsn	$⊢ y \in (ℂ ∖ \{0\}) \leftrightarrow (y \in ℂ \land y \neq 0)$
18		reccl	$⊢ (y \in ℂ \land y \neq 0) \to \frac{1}{y} \in ℂ$
19	17 18	sylbi	$⊢ y \in (ℂ ∖ \{0\}) \to \frac{1}{y} \in ℂ$
20	19	adantl	$⊢ (φ \land y \in (ℂ ∖ \{0\})) \to \frac{1}{y} \in ℂ$
21	20	fmpttd	$⊢ φ \to (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) : ℂ ∖ \{0\} ⟶ ℂ$
22		eqid	$⊢ if (1 \leq \|E\| z, 1, \|E\| z) (\frac{\|E\|}{2}) = if (1 \leq \|E\| z, 1, \|E\| z) (\frac{\|E\|}{2})$
23	22	reccn2	$⊢ (E \in (ℂ ∖ \{0\}) \land z \in ℝ^{+}) \to \exists w \in ℝ^{+} \forall v \in (ℂ ∖ \{0\}) (\|v - E\| < w \to \|(\frac{1}{v}) - (\frac{1}{E})\| < z)$
24	16 23	sylan	$⊢ (φ \land z \in ℝ^{+}) \to \exists w \in ℝ^{+} \forall v \in (ℂ ∖ \{0\}) (\|v - E\| < w \to \|(\frac{1}{v}) - (\frac{1}{E})\| < z)$
25		oveq2	$⊢ y = v \to \frac{1}{y} = \frac{1}{v}$
26		eqid	$⊢ (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) = (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y})$
27		ovex	$⊢ \frac{1}{v} \in V$
28	25 26 27	fvmpt	$⊢ v \in (ℂ ∖ \{0\}) \to (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (v) = \frac{1}{v}$
29		oveq2	$⊢ y = E \to \frac{1}{y} = \frac{1}{E}$
30		ovex	$⊢ \frac{1}{E} \in V$
31	29 26 30	fvmpt	$⊢ E \in (ℂ ∖ \{0\}) \to (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (E) = \frac{1}{E}$
32	16 31	syl	$⊢ φ \to (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (E) = \frac{1}{E}$
33	28 32	oveqan12rd	$⊢ (φ \land v \in (ℂ ∖ \{0\})) \to (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (v) - (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (E) = (\frac{1}{v}) - (\frac{1}{E})$
34	33	fveq2d	$⊢ (φ \land v \in (ℂ ∖ \{0\})) \to \|(y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (v) - (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (E)\| = \|(\frac{1}{v}) - (\frac{1}{E})\|$
35	34	breq1d	$⊢ (φ \land v \in (ℂ ∖ \{0\})) \to (\|(y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (v) - (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (E)\| < z \leftrightarrow \|(\frac{1}{v}) - (\frac{1}{E})\| < z)$
36	35	imbi2d	$⊢ (φ \land v \in (ℂ ∖ \{0\})) \to ((\|v - E\| < w \to \|(y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (v) - (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (E)\| < z) \leftrightarrow (\|v - E\| < w \to \|(\frac{1}{v}) - (\frac{1}{E})\| < z))$
37	36	ralbidva	$⊢ φ \to (\forall v \in (ℂ ∖ \{0\}) (\|v - E\| < w \to \|(y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (v) - (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (E)\| < z) \leftrightarrow \forall v \in (ℂ ∖ \{0\}) (\|v - E\| < w \to \|(\frac{1}{v}) - (\frac{1}{E})\| < z))$
38	37	rexbidv	$⊢ φ \to (\exists w \in ℝ^{+} \forall v \in (ℂ ∖ \{0\}) (\|v - E\| < w \to \|(y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (v) - (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (E)\| < z) \leftrightarrow \exists w \in ℝ^{+} \forall v \in (ℂ ∖ \{0\}) (\|v - E\| < w \to \|(\frac{1}{v}) - (\frac{1}{E})\| < z))$
39	38	biimpar	$⊢ (φ \land \exists w \in ℝ^{+} \forall v \in (ℂ ∖ \{0\}) (\|v - E\| < w \to \|(\frac{1}{v}) - (\frac{1}{E})\| < z)) \to \exists w \in ℝ^{+} \forall v \in (ℂ ∖ \{0\}) (\|v - E\| < w \to \|(y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (v) - (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (E)\| < z)$
40	24 39	syldan	$⊢ (φ \land z \in ℝ^{+}) \to \exists w \in ℝ^{+} \forall v \in (ℂ ∖ \{0\}) (\|v - E\| < w \to \|(y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (v) - (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (E)\| < z)$
41	12 16 4 21 40	rlimcn1	$⊢ φ \to ((y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) \circ (x \in A ⟼ C)) \underset{ℝ}{⇝} (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) (E)$
42		eqidd	$⊢ φ \to (x \in A ⟼ C) = (x \in A ⟼ C)$
43		eqidd	$⊢ φ \to (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) = (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y})$
44		oveq2	$⊢ y = C \to \frac{1}{y} = \frac{1}{C}$
45	11 42 43 44	fmptco	$⊢ φ \to (y \in (ℂ ∖ \{0\}) ⟼ \frac{1}{y}) \circ (x \in A ⟼ C) = (x \in A ⟼ \frac{1}{C})$
46	41 45 32	3brtr3d	$⊢ φ \to (x \in A ⟼ \frac{1}{C}) \underset{ℝ}{⇝} (\frac{1}{E})$
47	7 9 3 46	rlimmul	$⊢ φ \to (x \in A ⟼ B (\frac{1}{C})) \underset{ℝ}{⇝} D (\frac{1}{E})$
48	7 8 6	divrecd	$⊢ (φ \land x \in A) \to \frac{B}{C} = B (\frac{1}{C})$
49	48	mpteq2dva	$⊢ φ \to (x \in A ⟼ \frac{B}{C}) = (x \in A ⟼ B (\frac{1}{C}))$
50		rlimcl	$⊢ (x \in A ⟼ B) \underset{ℝ}{⇝} D \to D \in ℂ$
51	3 50	syl	$⊢ φ \to D \in ℂ$
52	51 14 5	divrecd	$⊢ φ \to \frac{D}{E} = D (\frac{1}{E})$
53	47 49 52	3brtr4d	$⊢ φ \to (x \in A ⟼ \frac{B}{C}) \underset{ℝ}{⇝} (\frac{D}{E})$

Metamath Proof Explorer

Theorem rlimdiv

Proof