reclimc

Description: Limit of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	reclimc.f	$⊢ F = (x \in A ⟼ B)$
	reclimc.g	$⊢ G = (x \in A ⟼ \frac{1}{B})$
	reclimc.b	$⊢ (φ \land x \in A) \to B \in (ℂ ∖ \{0\})$
	reclimc.c	$⊢ φ \to C \in (F {lim}_{ℂ} D)$
	reclimc.cne0	$⊢ φ \to C \neq 0$
Assertion	reclimc	$⊢ φ \to \frac{1}{C} \in (G {lim}_{ℂ} D)$

Proof

Step	Hyp	Ref	Expression
1		reclimc.f	$⊢ F = (x \in A ⟼ B)$
2		reclimc.g	$⊢ G = (x \in A ⟼ \frac{1}{B})$
3		reclimc.b	$⊢ (φ \land x \in A) \to B \in (ℂ ∖ \{0\})$
4		reclimc.c	$⊢ φ \to C \in (F {lim}_{ℂ} D)$
5		reclimc.cne0	$⊢ φ \to C \neq 0$
6		eqid	$⊢ (x \in A ⟼ C - B) = (x \in A ⟼ C - B)$
7		eqid	$⊢ (x \in A ⟼ B C) = (x \in A ⟼ B C)$
8		eqid	$⊢ (x \in A ⟼ \frac{C - B}{B C}) = (x \in A ⟼ \frac{C - B}{B C})$
9		limccl	$⊢ F {lim}_{ℂ} D \subseteq ℂ$
10	9 4	sselid	$⊢ φ \to C \in ℂ$
11	10	adantr	$⊢ (φ \land x \in A) \to C \in ℂ$
12	3	eldifad	$⊢ (φ \land x \in A) \to B \in ℂ$
13	11 12	subcld	$⊢ (φ \land x \in A) \to C - B \in ℂ$
14	12 11	mulcld	$⊢ (φ \land x \in A) \to B C \in ℂ$
15		eldifsni	$⊢ B \in (ℂ ∖ \{0\}) \to B \neq 0$
16	3 15	syl	$⊢ (φ \land x \in A) \to B \neq 0$
17	5	adantr	$⊢ (φ \land x \in A) \to C \neq 0$
18	12 11 16 17	mulne0d	$⊢ (φ \land x \in A) \to B C \neq 0$
19	18	neneqd	$⊢ (φ \land x \in A) \to \neg B C = 0$
20		elsng	$⊢ B C \in ℂ \to (B C \in \{0\} \leftrightarrow B C = 0)$
21	14 20	syl	$⊢ (φ \land x \in A) \to (B C \in \{0\} \leftrightarrow B C = 0)$
22	19 21	mtbird	$⊢ (φ \land x \in A) \to \neg B C \in \{0\}$
23	14 22	eldifd	$⊢ (φ \land x \in A) \to B C \in (ℂ ∖ \{0\})$
24		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
25		eqid	$⊢ (x \in A ⟼ - B) = (x \in A ⟼ - B)$
26		eqid	$⊢ (x \in A ⟼ C + (- B)) = (x \in A ⟼ C + (- B))$
27	12	negcld	$⊢ (φ \land x \in A) \to - B \in ℂ$
28	1 12 4	limcmptdm	$⊢ φ \to A \subseteq ℂ$
29		limcrcl	$⊢ C \in (F {lim}_{ℂ} D) \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land D \in ℂ)$
30	4 29	syl	$⊢ φ \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land D \in ℂ)$
31	30	simp3d	$⊢ φ \to D \in ℂ$
32	24 28 10 31	constlimc	$⊢ φ \to C \in ((x \in A ⟼ C) {lim}_{ℂ} D)$
33	1 25 12 4	neglimc	$⊢ φ \to - C \in ((x \in A ⟼ - B) {lim}_{ℂ} D)$
34	24 25 26 11 27 32 33	addlimc	$⊢ φ \to C + (- C) \in ((x \in A ⟼ C + (- B)) {lim}_{ℂ} D)$
35	10	negidd	$⊢ φ \to C + (- C) = 0$
36	11 12	negsubd	$⊢ (φ \land x \in A) \to C + (- B) = C - B$
37	36	mpteq2dva	$⊢ φ \to (x \in A ⟼ C + (- B)) = (x \in A ⟼ C - B)$
38	37	oveq1d	$⊢ φ \to (x \in A ⟼ C + (- B)) {lim}_{ℂ} D = (x \in A ⟼ C - B) {lim}_{ℂ} D$
39	34 35 38	3eltr3d	$⊢ φ \to 0 \in ((x \in A ⟼ C - B) {lim}_{ℂ} D)$
40	1 24 7 12 11 4 32	mullimc	$⊢ φ \to C C \in ((x \in A ⟼ B C) {lim}_{ℂ} D)$
41	10 10 5 5	mulne0d	$⊢ φ \to C C \neq 0$
42	6 7 8 13 23 39 40 41	0ellimcdiv	$⊢ φ \to 0 \in ((x \in A ⟼ \frac{C - B}{B C}) {lim}_{ℂ} D)$
43		1cnd	$⊢ (φ \land x \in A) \to 1 \in ℂ$
44	43 12 43 11 16 17	divsubdivd	$⊢ (φ \land x \in A) \to (\frac{1}{B}) - (\frac{1}{C}) = \frac{1 C - 1 B}{B C}$
45	11	mulid2d	$⊢ (φ \land x \in A) \to 1 C = C$
46	12	mulid2d	$⊢ (φ \land x \in A) \to 1 B = B$
47	45 46	oveq12d	$⊢ (φ \land x \in A) \to 1 C - 1 B = C - B$
48	47	oveq1d	$⊢ (φ \land x \in A) \to \frac{1 C - 1 B}{B C} = \frac{C - B}{B C}$
49	44 48	eqtr2d	$⊢ (φ \land x \in A) \to \frac{C - B}{B C} = (\frac{1}{B}) - (\frac{1}{C})$
50	49	mpteq2dva	$⊢ φ \to (x \in A ⟼ \frac{C - B}{B C}) = (x \in A ⟼ (\frac{1}{B}) - (\frac{1}{C}))$
51	50	oveq1d	$⊢ φ \to (x \in A ⟼ \frac{C - B}{B C}) {lim}_{ℂ} D = (x \in A ⟼ (\frac{1}{B}) - (\frac{1}{C})) {lim}_{ℂ} D$
52	42 51	eleqtrd	$⊢ φ \to 0 \in ((x \in A ⟼ (\frac{1}{B}) - (\frac{1}{C})) {lim}_{ℂ} D)$
53		eqid	$⊢ (x \in A ⟼ (\frac{1}{B}) - (\frac{1}{C})) = (x \in A ⟼ (\frac{1}{B}) - (\frac{1}{C}))$
54	12 16	reccld	$⊢ (φ \land x \in A) \to \frac{1}{B} \in ℂ$
55	10 5	reccld	$⊢ φ \to \frac{1}{C} \in ℂ$
56	2 53 28 54 31 55	ellimcabssub0	$⊢ φ \to (\frac{1}{C} \in (G {lim}_{ℂ} D) \leftrightarrow 0 \in ((x \in A ⟼ (\frac{1}{B}) - (\frac{1}{C})) {lim}_{ℂ} D))$
57	52 56	mpbird	$⊢ φ \to \frac{1}{C} \in (G {lim}_{ℂ} D)$

Metamath Proof Explorer

Theorem reclimc

Proof