climrec

Description: Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	climrec.1	$⊢ Z = ℤ_{\geq M}$
	climrec.2	$⊢ φ \to M \in ℤ$
	climrec.3	$⊢ φ \to G ⇝ A$
	climrec.4	$⊢ φ \to A \neq 0$
	climrec.5	$⊢ (φ \land k \in Z) \to G (k) \in (ℂ ∖ \{0\})$
	climrec.6	$⊢ (φ \land k \in Z) \to H (k) = \frac{1}{G (k)}$
	climrec.7	$⊢ φ \to H \in W$
Assertion	climrec	$⊢ φ \to H ⇝ (\frac{1}{A})$

Proof

Step	Hyp	Ref	Expression
1		climrec.1	$⊢ Z = ℤ_{\geq M}$
2		climrec.2	$⊢ φ \to M \in ℤ$
3		climrec.3	$⊢ φ \to G ⇝ A$
4		climrec.4	$⊢ φ \to A \neq 0$
5		climrec.5	$⊢ (φ \land k \in Z) \to G (k) \in (ℂ ∖ \{0\})$
6		climrec.6	$⊢ (φ \land k \in Z) \to H (k) = \frac{1}{G (k)}$
7		climrec.7	$⊢ φ \to H \in W$
8		climcl	$⊢ G ⇝ A \to A \in ℂ$
9	3 8	syl	$⊢ φ \to A \in ℂ$
10	4	neneqd	$⊢ φ \to \neg A = 0$
11		c0ex	$⊢ 0 \in V$
12	11	elsn2	$⊢ A \in \{0\} \leftrightarrow A = 0$
13	10 12	sylnibr	$⊢ φ \to \neg A \in \{0\}$
14	9 13	eldifd	$⊢ φ \to A \in (ℂ ∖ \{0\})$
15		eqidd	$⊢ (φ \land z \in (ℂ ∖ \{0\})) \to (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) = (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w})$
16		simpr	$⊢ ((φ \land z \in (ℂ ∖ \{0\})) \land w = z) \to w = z$
17	16	oveq2d	$⊢ ((φ \land z \in (ℂ ∖ \{0\})) \land w = z) \to \frac{1}{w} = \frac{1}{z}$
18		simpr	$⊢ (φ \land z \in (ℂ ∖ \{0\})) \to z \in (ℂ ∖ \{0\})$
19	18	eldifad	$⊢ (φ \land z \in (ℂ ∖ \{0\})) \to z \in ℂ$
20		eldifsni	$⊢ z \in (ℂ ∖ \{0\}) \to z \neq 0$
21	20	adantl	$⊢ (φ \land z \in (ℂ ∖ \{0\})) \to z \neq 0$
22	19 21	reccld	$⊢ (φ \land z \in (ℂ ∖ \{0\})) \to \frac{1}{z} \in ℂ$
23	15 17 18 22	fvmptd	$⊢ (φ \land z \in (ℂ ∖ \{0\})) \to (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (z) = \frac{1}{z}$
24	23 22	eqeltrd	$⊢ (φ \land z \in (ℂ ∖ \{0\})) \to (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (z) \in ℂ$
25		eqid	$⊢ if (1 \leq \|A\| x, 1, \|A\| x) (\frac{\|A\|}{2}) = if (1 \leq \|A\| x, 1, \|A\| x) (\frac{\|A\|}{2})$
26	25	reccn2	$⊢ (A \in (ℂ ∖ \{0\}) \land x \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in (ℂ ∖ \{0\}) (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x)$
27	14 26	sylan	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in (ℂ ∖ \{0\}) (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x)$
28		eqidd	$⊢ z \in (ℂ ∖ \{0\}) \to (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) = (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w})$
29		simpr	$⊢ (z \in (ℂ ∖ \{0\}) \land w = z) \to w = z$
30	29	oveq2d	$⊢ (z \in (ℂ ∖ \{0\}) \land w = z) \to \frac{1}{w} = \frac{1}{z}$
31		id	$⊢ z \in (ℂ ∖ \{0\}) \to z \in (ℂ ∖ \{0\})$
32		eldifi	$⊢ z \in (ℂ ∖ \{0\}) \to z \in ℂ$
33	32 20	reccld	$⊢ z \in (ℂ ∖ \{0\}) \to \frac{1}{z} \in ℂ$
34	28 30 31 33	fvmptd	$⊢ z \in (ℂ ∖ \{0\}) \to (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (z) = \frac{1}{z}$
35	34	ad2antlr	$⊢ ((((φ \land x \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \to (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x))) \land z \in (ℂ ∖ \{0\})) \land \|z - A\| < y) \to (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (z) = \frac{1}{z}$
36		eqidd	$⊢ φ \to (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) = (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w})$
37		simpr	$⊢ (φ \land w = A) \to w = A$
38	37	oveq2d	$⊢ (φ \land w = A) \to \frac{1}{w} = \frac{1}{A}$
39	9 4	reccld	$⊢ φ \to \frac{1}{A} \in ℂ$
40	36 38 14 39	fvmptd	$⊢ φ \to (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (A) = \frac{1}{A}$
41	40	ad4antr	$⊢ ((((φ \land x \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \to (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x))) \land z \in (ℂ ∖ \{0\})) \land \|z - A\| < y) \to (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (A) = \frac{1}{A}$
42	35 41	oveq12d	$⊢ ((((φ \land x \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \to (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x))) \land z \in (ℂ ∖ \{0\})) \land \|z - A\| < y) \to (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (z) - (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (A) = (\frac{1}{z}) - (\frac{1}{A})$
43	42	fveq2d	$⊢ ((((φ \land x \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \to (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x))) \land z \in (ℂ ∖ \{0\})) \land \|z - A\| < y) \to \|(w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (z) - (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (A)\| = \|(\frac{1}{z}) - (\frac{1}{A})\|$
44	31	ad2antlr	$⊢ ((((φ \land x \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \to (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x))) \land z \in (ℂ ∖ \{0\})) \land \|z - A\| < y) \to z \in (ℂ ∖ \{0\})$
45		simpr	$⊢ ((((φ \land x \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \to (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x))) \land z \in (ℂ ∖ \{0\})) \land \|z - A\| < y) \to \|z - A\| < y$
46		simpllr	$⊢ ((((φ \land x \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \to (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x))) \land z \in (ℂ ∖ \{0\})) \land \|z - A\| < y) \to (z \in (ℂ ∖ \{0\}) \to (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x))$
47	44 45 46	mp2d	$⊢ ((((φ \land x \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \to (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x))) \land z \in (ℂ ∖ \{0\})) \land \|z - A\| < y) \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x$
48	43 47	eqbrtrd	$⊢ ((((φ \land x \in ℝ^{+}) \land (z \in (ℂ ∖ \{0\}) \to (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x))) \land z \in (ℂ ∖ \{0\})) \land \|z - A\| < y) \to \|(w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (z) - (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (A)\| < x$
49	48	exp41	$⊢ (φ \land x \in ℝ^{+}) \to ((z \in (ℂ ∖ \{0\}) \to (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x)) \to (z \in (ℂ ∖ \{0\}) \to (\|z - A\| < y \to \|(w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (z) - (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (A)\| < x)))$
50	49	ralimdv2	$⊢ (φ \land x \in ℝ^{+}) \to (\forall z \in (ℂ ∖ \{0\}) (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x) \to \forall z \in (ℂ ∖ \{0\}) (\|z - A\| < y \to \|(w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (z) - (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (A)\| < x))$
51	50	reximdv	$⊢ (φ \land x \in ℝ^{+}) \to (\exists y \in ℝ^{+} \forall z \in (ℂ ∖ \{0\}) (\|z - A\| < y \to \|(\frac{1}{z}) - (\frac{1}{A})\| < x) \to \exists y \in ℝ^{+} \forall z \in (ℂ ∖ \{0\}) (\|z - A\| < y \to \|(w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (z) - (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (A)\| < x))$
52	27 51	mpd	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in (ℂ ∖ \{0\}) (\|z - A\| < y \to \|(w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (z) - (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (A)\| < x)$
53		eqidd	$⊢ (φ \land k \in Z) \to (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) = (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w})$
54		oveq2	$⊢ w = G (k) \to \frac{1}{w} = \frac{1}{G (k)}$
55	54	adantl	$⊢ ((φ \land k \in Z) \land w = G (k)) \to \frac{1}{w} = \frac{1}{G (k)}$
56	5	eldifad	$⊢ (φ \land k \in Z) \to G (k) \in ℂ$
57		eldifsni	$⊢ G (k) \in (ℂ ∖ \{0\}) \to G (k) \neq 0$
58	5 57	syl	$⊢ (φ \land k \in Z) \to G (k) \neq 0$
59	56 58	reccld	$⊢ (φ \land k \in Z) \to \frac{1}{G (k)} \in ℂ$
60	53 55 5 59	fvmptd	$⊢ (φ \land k \in Z) \to (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (G (k)) = \frac{1}{G (k)}$
61	6 60	eqtr4d	$⊢ (φ \land k \in Z) \to H (k) = (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (G (k))$
62	1 2 14 24 3 7 52 5 61	climcn1	$⊢ φ \to H ⇝ (w \in (ℂ ∖ \{0\}) ⟼ \frac{1}{w}) (A)$
63	62 40	breqtrd	$⊢ φ \to H ⇝ (\frac{1}{A})$

Metamath Proof Explorer

Theorem climrec

Proof