climrlim2

Description: Produce a real limit from an integer limit, where the real function is only dependent on the integer part of x . (Contributed by Mario Carneiro, 2-May-2016)

	Ref	Expression
Hypotheses	climrlim2.1	$⊢ Z = ℤ_{\geq M}$
	climrlim2.2	$⊢ n = ⌊x⌋ \to B = C$
	climrlim2.3	$⊢ φ \to A \subseteq ℝ$
	climrlim2.4	$⊢ φ \to M \in ℤ$
	climrlim2.5	$⊢ φ \to (n \in Z ⟼ B) ⇝ D$
	climrlim2.6	$⊢ (φ \land n \in Z) \to B \in ℂ$
	climrlim2.7	$⊢ (φ \land x \in A) \to M \leq x$
Assertion	climrlim2	$⊢ φ \to (x \in A ⟼ C) \underset{ℝ}{⇝} D$

Proof

Step	Hyp	Ref	Expression
1		climrlim2.1	$⊢ Z = ℤ_{\geq M}$
2		climrlim2.2	$⊢ n = ⌊x⌋ \to B = C$
3		climrlim2.3	$⊢ φ \to A \subseteq ℝ$
4		climrlim2.4	$⊢ φ \to M \in ℤ$
5		climrlim2.5	$⊢ φ \to (n \in Z ⟼ B) ⇝ D$
6		climrlim2.6	$⊢ (φ \land n \in Z) \to B \in ℂ$
7		climrlim2.7	$⊢ (φ \land x \in A) \to M \leq x$
8		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
9	8 1	eleq2s	$⊢ j \in Z \to j \in ℤ$
10	9	ad2antlr	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land (x \in A \land j \leq x)) \to j \in ℤ$
11	3	sselda	$⊢ (φ \land x \in A) \to x \in ℝ$
12	11	flcld	$⊢ (φ \land x \in A) \to ⌊x⌋ \in ℤ$
13	12	adantlr	$⊢ ((φ \land y \in ℝ^{+}) \land x \in A) \to ⌊x⌋ \in ℤ$
14	13	ad2ant2r	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land (x \in A \land j \leq x)) \to ⌊x⌋ \in ℤ$
15		simprr	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land (x \in A \land j \leq x)) \to j \leq x$
16	11	adantlr	$⊢ ((φ \land y \in ℝ^{+}) \land x \in A) \to x \in ℝ$
17	16	ad2ant2r	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land (x \in A \land j \leq x)) \to x \in ℝ$
18		flge	$⊢ (x \in ℝ \land j \in ℤ) \to (j \leq x \leftrightarrow j \leq ⌊x⌋)$
19	17 10 18	syl2anc	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land (x \in A \land j \leq x)) \to (j \leq x \leftrightarrow j \leq ⌊x⌋)$
20	15 19	mpbid	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land (x \in A \land j \leq x)) \to j \leq ⌊x⌋$
21		eluz2	$⊢ ⌊x⌋ \in ℤ_{\geq j} \leftrightarrow (j \in ℤ \land ⌊x⌋ \in ℤ \land j \leq ⌊x⌋)$
22	10 14 20 21	syl3anbrc	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land (x \in A \land j \leq x)) \to ⌊x⌋ \in ℤ_{\geq j}$
23		simpr	$⊢ ((n \in Z ⟼ B) (k) \in ℂ \land \|(n \in Z ⟼ B) (k) - D\| < y) \to \|(n \in Z ⟼ B) (k) - D\| < y$
24	23	ralimi	$⊢ \forall k \in ℤ_{\geq j} ((n \in Z ⟼ B) (k) \in ℂ \land \|(n \in Z ⟼ B) (k) - D\| < y) \to \forall k \in ℤ_{\geq j} \|(n \in Z ⟼ B) (k) - D\| < y$
25		fveq2	$⊢ k = ⌊x⌋ \to (n \in Z ⟼ B) (k) = (n \in Z ⟼ B) (⌊x⌋)$
26	25	fvoveq1d	$⊢ k = ⌊x⌋ \to \|(n \in Z ⟼ B) (k) - D\| = \|(n \in Z ⟼ B) (⌊x⌋) - D\|$
27	26	breq1d	$⊢ k = ⌊x⌋ \to (\|(n \in Z ⟼ B) (k) - D\| < y \leftrightarrow \|(n \in Z ⟼ B) (⌊x⌋) - D\| < y)$
28	27	rspcv	$⊢ ⌊x⌋ \in ℤ_{\geq j} \to (\forall k \in ℤ_{\geq j} \|(n \in Z ⟼ B) (k) - D\| < y \to \|(n \in Z ⟼ B) (⌊x⌋) - D\| < y)$
29	22 24 28	syl2im	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land (x \in A \land j \leq x)) \to (\forall k \in ℤ_{\geq j} ((n \in Z ⟼ B) (k) \in ℂ \land \|(n \in Z ⟼ B) (k) - D\| < y) \to \|(n \in Z ⟼ B) (⌊x⌋) - D\| < y)$
30		eqid	$⊢ (n \in Z ⟼ B) = (n \in Z ⟼ B)$
31	4	adantr	$⊢ (φ \land x \in A) \to M \in ℤ$
32		flge	$⊢ (x \in ℝ \land M \in ℤ) \to (M \leq x \leftrightarrow M \leq ⌊x⌋)$
33	11 31 32	syl2anc	$⊢ (φ \land x \in A) \to (M \leq x \leftrightarrow M \leq ⌊x⌋)$
34	7 33	mpbid	$⊢ (φ \land x \in A) \to M \leq ⌊x⌋$
35		eluz2	$⊢ ⌊x⌋ \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land ⌊x⌋ \in ℤ \land M \leq ⌊x⌋)$
36	31 12 34 35	syl3anbrc	$⊢ (φ \land x \in A) \to ⌊x⌋ \in ℤ_{\geq M}$
37	36 1	eleqtrrdi	$⊢ (φ \land x \in A) \to ⌊x⌋ \in Z$
38	2	eleq1d	$⊢ n = ⌊x⌋ \to (B \in ℂ \leftrightarrow C \in ℂ)$
39	6	ralrimiva	$⊢ φ \to \forall n \in Z B \in ℂ$
40	39	adantr	$⊢ (φ \land x \in A) \to \forall n \in Z B \in ℂ$
41	38 40 37	rspcdva	$⊢ (φ \land x \in A) \to C \in ℂ$
42	30 2 37 41	fvmptd3	$⊢ (φ \land x \in A) \to (n \in Z ⟼ B) (⌊x⌋) = C$
43	42	adantlr	$⊢ ((φ \land y \in ℝ^{+}) \land x \in A) \to (n \in Z ⟼ B) (⌊x⌋) = C$
44	43	ad2ant2r	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land (x \in A \land j \leq x)) \to (n \in Z ⟼ B) (⌊x⌋) = C$
45	44	fvoveq1d	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land (x \in A \land j \leq x)) \to \|(n \in Z ⟼ B) (⌊x⌋) - D\| = \|C - D\|$
46	45	breq1d	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land (x \in A \land j \leq x)) \to (\|(n \in Z ⟼ B) (⌊x⌋) - D\| < y \leftrightarrow \|C - D\| < y)$
47	29 46	sylibd	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land (x \in A \land j \leq x)) \to (\forall k \in ℤ_{\geq j} ((n \in Z ⟼ B) (k) \in ℂ \land \|(n \in Z ⟼ B) (k) - D\| < y) \to \|C - D\| < y)$
48	47	expr	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land x \in A) \to (j \leq x \to (\forall k \in ℤ_{\geq j} ((n \in Z ⟼ B) (k) \in ℂ \land \|(n \in Z ⟼ B) (k) - D\| < y) \to \|C - D\| < y))$
49	48	com23	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land x \in A) \to (\forall k \in ℤ_{\geq j} ((n \in Z ⟼ B) (k) \in ℂ \land \|(n \in Z ⟼ B) (k) - D\| < y) \to (j \leq x \to \|C - D\| < y))$
50	49	ralrimdva	$⊢ ((φ \land y \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} ((n \in Z ⟼ B) (k) \in ℂ \land \|(n \in Z ⟼ B) (k) - D\| < y) \to \forall x \in A (j \leq x \to \|C - D\| < y))$
51		eluzelre	$⊢ j \in ℤ_{\geq M} \to j \in ℝ$
52	51 1	eleq2s	$⊢ j \in Z \to j \in ℝ$
53	52	adantl	$⊢ ((φ \land y \in ℝ^{+}) \land j \in Z) \to j \in ℝ$
54	50 53	jctild	$⊢ ((φ \land y \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} ((n \in Z ⟼ B) (k) \in ℂ \land \|(n \in Z ⟼ B) (k) - D\| < y) \to (j \in ℝ \land \forall x \in A (j \leq x \to \|C - D\| < y)))$
55	54	expimpd	$⊢ (φ \land y \in ℝ^{+}) \to ((j \in Z \land \forall k \in ℤ_{\geq j} ((n \in Z ⟼ B) (k) \in ℂ \land \|(n \in Z ⟼ B) (k) - D\| < y)) \to (j \in ℝ \land \forall x \in A (j \leq x \to \|C - D\| < y)))$
56	55	reximdv2	$⊢ (φ \land y \in ℝ^{+}) \to (\exists j \in Z \forall k \in ℤ_{\geq j} ((n \in Z ⟼ B) (k) \in ℂ \land \|(n \in Z ⟼ B) (k) - D\| < y) \to \exists j \in ℝ \forall x \in A (j \leq x \to \|C - D\| < y))$
57	56	ralimdva	$⊢ φ \to (\forall y \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} ((n \in Z ⟼ B) (k) \in ℂ \land \|(n \in Z ⟼ B) (k) - D\| < y) \to \forall y \in ℝ^{+} \exists j \in ℝ \forall x \in A (j \leq x \to \|C - D\| < y))$
58	57	adantld	$⊢ φ \to ((D \in ℂ \land \forall y \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} ((n \in Z ⟼ B) (k) \in ℂ \land \|(n \in Z ⟼ B) (k) - D\| < y)) \to \forall y \in ℝ^{+} \exists j \in ℝ \forall x \in A (j \leq x \to \|C - D\| < y))$
59		climrel	$⊢ Rel ⇝$
60	59	brrelex1i	$⊢ (n \in Z ⟼ B) ⇝ D \to (n \in Z ⟼ B) \in V$
61	5 60	syl	$⊢ φ \to (n \in Z ⟼ B) \in V$
62		eqidd	$⊢ (φ \land k \in Z) \to (n \in Z ⟼ B) (k) = (n \in Z ⟼ B) (k)$
63	1 4 61 62	clim2	$⊢ φ \to ((n \in Z ⟼ B) ⇝ D \leftrightarrow (D \in ℂ \land \forall y \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} ((n \in Z ⟼ B) (k) \in ℂ \land \|(n \in Z ⟼ B) (k) - D\| < y)))$
64	41	ralrimiva	$⊢ φ \to \forall x \in A C \in ℂ$
65		climcl	$⊢ (n \in Z ⟼ B) ⇝ D \to D \in ℂ$
66	5 65	syl	$⊢ φ \to D \in ℂ$
67	64 3 66	rlim2	$⊢ φ \to ((x \in A ⟼ C) \underset{ℝ}{⇝} D \leftrightarrow \forall y \in ℝ^{+} \exists j \in ℝ \forall x \in A (j \leq x \to \|C - D\| < y))$
68	58 63 67	3imtr4d	$⊢ φ \to ((n \in Z ⟼ B) ⇝ D \to (x \in A ⟼ C) \underset{ℝ}{⇝} D)$
69	5 68	mpd	$⊢ φ \to (x \in A ⟼ C) \underset{ℝ}{⇝} D$

Metamath Proof Explorer

Theorem climrlim2

Proof