rlimclim

Description: A sequence on an upper integer set converges in the real sense iff it converges in the integer sense. (Contributed by Mario Carneiro, 16-Sep-2014)

	Ref	Expression
Hypotheses	rlimclim.1	$⊢ Z = ℤ_{\geq M}$
	rlimclim.2	$⊢ φ \to M \in ℤ$
	rlimclim.3	$⊢ φ \to F : Z ⟶ ℂ$
Assertion	rlimclim	$⊢ φ \to (F \underset{ℝ}{⇝} A \leftrightarrow F ⇝ A)$

Proof

Step	Hyp	Ref	Expression
1		rlimclim.1	$⊢ Z = ℤ_{\geq M}$
2		rlimclim.2	$⊢ φ \to M \in ℤ$
3		rlimclim.3	$⊢ φ \to F : Z ⟶ ℂ$
4	2	adantr	$⊢ (φ \land F \underset{ℝ}{⇝} A) \to M \in ℤ$
5		simpr	$⊢ (φ \land F \underset{ℝ}{⇝} A) \to F \underset{ℝ}{⇝} A$
6		fdm	$⊢ F : Z ⟶ ℂ \to dom F = Z$
7		eqimss2	$⊢ dom F = Z \to Z \subseteq dom F$
8	3 6 7	3syl	$⊢ φ \to Z \subseteq dom F$
9	8	adantr	$⊢ (φ \land F \underset{ℝ}{⇝} A) \to Z \subseteq dom F$
10	1 4 5 9	rlimclim1	$⊢ (φ \land F \underset{ℝ}{⇝} A) \to F ⇝ A$
11		climcl	$⊢ F ⇝ A \to A \in ℂ$
12	11	adantl	$⊢ (φ \land F ⇝ A) \to A \in ℂ$
13	2	ad2antrr	$⊢ ((φ \land F ⇝ A) \land y \in ℝ^{+}) \to M \in ℤ$
14		simpr	$⊢ ((φ \land F ⇝ A) \land y \in ℝ^{+}) \to y \in ℝ^{+}$
15		eqidd	$⊢ (((φ \land F ⇝ A) \land y \in ℝ^{+}) \land k \in Z) \to F (k) = F (k)$
16		simplr	$⊢ ((φ \land F ⇝ A) \land y \in ℝ^{+}) \to F ⇝ A$
17	1 13 14 15 16	climi2	$⊢ ((φ \land F ⇝ A) \land y \in ℝ^{+}) \to \exists z \in Z \forall k \in ℤ_{\geq z} \|F (k) - A\| < y$
18		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
19	1 18	eqsstri	$⊢ Z \subseteq ℤ$
20		zssre	$⊢ ℤ \subseteq ℝ$
21	19 20	sstri	$⊢ Z \subseteq ℝ$
22		fveq2	$⊢ k = w \to F (k) = F (w)$
23	22	fvoveq1d	$⊢ k = w \to \|F (k) - A\| = \|F (w) - A\|$
24	23	breq1d	$⊢ k = w \to (\|F (k) - A\| < y \leftrightarrow \|F (w) - A\| < y)$
25		simplrr	$⊢ ((((φ \land F ⇝ A) \land y \in ℝ^{+}) \land (z \in Z \land \forall k \in ℤ_{\geq z} \|F (k) - A\| < y)) \land (w \in Z \land z \leq w)) \to \forall k \in ℤ_{\geq z} \|F (k) - A\| < y$
26		simplrl	$⊢ ((((φ \land F ⇝ A) \land y \in ℝ^{+}) \land (z \in Z \land \forall k \in ℤ_{\geq z} \|F (k) - A\| < y)) \land (w \in Z \land z \leq w)) \to z \in Z$
27	19 26	sselid	$⊢ ((((φ \land F ⇝ A) \land y \in ℝ^{+}) \land (z \in Z \land \forall k \in ℤ_{\geq z} \|F (k) - A\| < y)) \land (w \in Z \land z \leq w)) \to z \in ℤ$
28		simprl	$⊢ ((((φ \land F ⇝ A) \land y \in ℝ^{+}) \land (z \in Z \land \forall k \in ℤ_{\geq z} \|F (k) - A\| < y)) \land (w \in Z \land z \leq w)) \to w \in Z$
29	19 28	sselid	$⊢ ((((φ \land F ⇝ A) \land y \in ℝ^{+}) \land (z \in Z \land \forall k \in ℤ_{\geq z} \|F (k) - A\| < y)) \land (w \in Z \land z \leq w)) \to w \in ℤ$
30		simprr	$⊢ ((((φ \land F ⇝ A) \land y \in ℝ^{+}) \land (z \in Z \land \forall k \in ℤ_{\geq z} \|F (k) - A\| < y)) \land (w \in Z \land z \leq w)) \to z \leq w$
31		eluz2	$⊢ w \in ℤ_{\geq z} \leftrightarrow (z \in ℤ \land w \in ℤ \land z \leq w)$
32	27 29 30 31	syl3anbrc	$⊢ ((((φ \land F ⇝ A) \land y \in ℝ^{+}) \land (z \in Z \land \forall k \in ℤ_{\geq z} \|F (k) - A\| < y)) \land (w \in Z \land z \leq w)) \to w \in ℤ_{\geq z}$
33	24 25 32	rspcdva	$⊢ ((((φ \land F ⇝ A) \land y \in ℝ^{+}) \land (z \in Z \land \forall k \in ℤ_{\geq z} \|F (k) - A\| < y)) \land (w \in Z \land z \leq w)) \to \|F (w) - A\| < y$
34	33	expr	$⊢ ((((φ \land F ⇝ A) \land y \in ℝ^{+}) \land (z \in Z \land \forall k \in ℤ_{\geq z} \|F (k) - A\| < y)) \land w \in Z) \to (z \leq w \to \|F (w) - A\| < y)$
35	34	ralrimiva	$⊢ (((φ \land F ⇝ A) \land y \in ℝ^{+}) \land (z \in Z \land \forall k \in ℤ_{\geq z} \|F (k) - A\| < y)) \to \forall w \in Z (z \leq w \to \|F (w) - A\| < y)$
36	35	expr	$⊢ (((φ \land F ⇝ A) \land y \in ℝ^{+}) \land z \in Z) \to (\forall k \in ℤ_{\geq z} \|F (k) - A\| < y \to \forall w \in Z (z \leq w \to \|F (w) - A\| < y))$
37	36	reximdva	$⊢ ((φ \land F ⇝ A) \land y \in ℝ^{+}) \to (\exists z \in Z \forall k \in ℤ_{\geq z} \|F (k) - A\| < y \to \exists z \in Z \forall w \in Z (z \leq w \to \|F (w) - A\| < y))$
38		ssrexv	$⊢ Z \subseteq ℝ \to (\exists z \in Z \forall w \in Z (z \leq w \to \|F (w) - A\| < y) \to \exists z \in ℝ \forall w \in Z (z \leq w \to \|F (w) - A\| < y))$
39	21 37 38	mpsylsyld	$⊢ ((φ \land F ⇝ A) \land y \in ℝ^{+}) \to (\exists z \in Z \forall k \in ℤ_{\geq z} \|F (k) - A\| < y \to \exists z \in ℝ \forall w \in Z (z \leq w \to \|F (w) - A\| < y))$
40	17 39	mpd	$⊢ ((φ \land F ⇝ A) \land y \in ℝ^{+}) \to \exists z \in ℝ \forall w \in Z (z \leq w \to \|F (w) - A\| < y)$
41	40	ralrimiva	$⊢ (φ \land F ⇝ A) \to \forall y \in ℝ^{+} \exists z \in ℝ \forall w \in Z (z \leq w \to \|F (w) - A\| < y)$
42	3	adantr	$⊢ (φ \land F ⇝ A) \to F : Z ⟶ ℂ$
43	21	a1i	$⊢ (φ \land F ⇝ A) \to Z \subseteq ℝ$
44		eqidd	$⊢ ((φ \land F ⇝ A) \land w \in Z) \to F (w) = F (w)$
45	42 43 44	rlim	$⊢ (φ \land F ⇝ A) \to (F \underset{ℝ}{⇝} A \leftrightarrow (A \in ℂ \land \forall y \in ℝ^{+} \exists z \in ℝ \forall w \in Z (z \leq w \to \|F (w) - A\| < y)))$
46	12 41 45	mpbir2and	$⊢ (φ \land F ⇝ A) \to F \underset{ℝ}{⇝} A$
47	10 46	impbida	$⊢ φ \to (F \underset{ℝ}{⇝} A \leftrightarrow F ⇝ A)$

Metamath Proof Explorer

Theorem rlimclim

Proof