rlimclim1

Description: Forward direction of rlimclim . (Contributed by Mario Carneiro, 16-Sep-2014)

	Ref	Expression
Hypotheses	rlimclim1.1	$⊢ Z = ℤ_{\geq M}$
	rlimclim1.2	$⊢ φ \to M \in ℤ$
	rlimclim1.3	$⊢ φ \to F \underset{ℝ}{⇝} A$
	rlimclim1.4	$⊢ φ \to Z \subseteq dom F$
Assertion	rlimclim1	$⊢ φ \to F ⇝ A$

Proof

Step	Hyp	Ref	Expression
1		rlimclim1.1	$⊢ Z = ℤ_{\geq M}$
2		rlimclim1.2	$⊢ φ \to M \in ℤ$
3		rlimclim1.3	$⊢ φ \to F \underset{ℝ}{⇝} A$
4		rlimclim1.4	$⊢ φ \to Z \subseteq dom F$
5		fvex	$⊢ F (w) \in V$
6	5	rgenw	$⊢ \forall w \in dom F F (w) \in V$
7	6	a1i	$⊢ (φ \land y \in ℝ^{+}) \to \forall w \in dom F F (w) \in V$
8		simpr	$⊢ (φ \land y \in ℝ^{+}) \to y \in ℝ^{+}$
9		rlimf	$⊢ F \underset{ℝ}{⇝} A \to F : dom F ⟶ ℂ$
10	3 9	syl	$⊢ φ \to F : dom F ⟶ ℂ$
11	10	adantr	$⊢ (φ \land y \in ℝ^{+}) \to F : dom F ⟶ ℂ$
12	11	feqmptd	$⊢ (φ \land y \in ℝ^{+}) \to F = (w \in dom F ⟼ F (w))$
13	3	adantr	$⊢ (φ \land y \in ℝ^{+}) \to F \underset{ℝ}{⇝} A$
14	12 13	eqbrtrrd	$⊢ (φ \land y \in ℝ^{+}) \to (w \in dom F ⟼ F (w)) \underset{ℝ}{⇝} A$
15	7 8 14	rlimi	$⊢ (φ \land y \in ℝ^{+}) \to \exists z \in ℝ \forall w \in dom F (z \leq w \to \|F (w) - A\| < y)$
16	2	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \to M \in ℤ$
17		flcl	$⊢ z \in ℝ \to ⌊z⌋ \in ℤ$
18	17	peano2zd	$⊢ z \in ℝ \to ⌊z⌋ + 1 \in ℤ$
19	18	ad2antrl	$⊢ ((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \to ⌊z⌋ + 1 \in ℤ$
20	19 16	ifcld	$⊢ ((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \to if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M) \in ℤ$
21	16	zred	$⊢ ((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \to M \in ℝ$
22	19	zred	$⊢ ((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \to ⌊z⌋ + 1 \in ℝ$
23		max1	$⊢ (M \in ℝ \land ⌊z⌋ + 1 \in ℝ) \to M \leq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)$
24	21 22 23	syl2anc	$⊢ ((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \to M \leq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)$
25		eluz2	$⊢ if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M) \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M) \in ℤ \land M \leq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M))$
26	16 20 24 25	syl3anbrc	$⊢ ((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \to if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M) \in ℤ_{\geq M}$
27	26 1	eleqtrrdi	$⊢ ((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \to if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M) \in Z$
28		simplrl	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to z \in ℝ$
29	18	zred	$⊢ z \in ℝ \to ⌊z⌋ + 1 \in ℝ$
30	28 29	syl	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to ⌊z⌋ + 1 \in ℝ$
31	21	adantr	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to M \in ℝ$
32	30 31	ifcld	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M) \in ℝ$
33		eluzelre	$⊢ k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)} \to k \in ℝ$
34	33	adantl	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to k \in ℝ$
35		fllep1	$⊢ z \in ℝ \to z \leq ⌊z⌋ + 1$
36	28 35	syl	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to z \leq ⌊z⌋ + 1$
37		max2	$⊢ (M \in ℝ \land ⌊z⌋ + 1 \in ℝ) \to ⌊z⌋ + 1 \leq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)$
38	31 30 37	syl2anc	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to ⌊z⌋ + 1 \leq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)$
39	28 30 32 36 38	letrd	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to z \leq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)$
40		eluzle	$⊢ k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)} \to if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M) \leq k$
41	40	adantl	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M) \leq k$
42	28 32 34 39 41	letrd	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to z \leq k$
43		breq2	$⊢ w = k \to (z \leq w \leftrightarrow z \leq k)$
44	43	imbrov2fvoveq	$⊢ w = k \to ((z \leq w \to \|F (w) - A\| < y) \leftrightarrow (z \leq k \to \|F (k) - A\| < y))$
45		simplrr	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to \forall w \in dom F (z \leq w \to \|F (w) - A\| < y)$
46	4	ad3antrrr	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to Z \subseteq dom F$
47	1	uztrn2	$⊢ (if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M) \in Z \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to k \in Z$
48	27 47	sylan	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to k \in Z$
49	46 48	sseldd	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to k \in dom F$
50	44 45 49	rspcdva	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to (z \leq k \to \|F (k) - A\| < y)$
51	42 50	mpd	$⊢ (((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \land k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}) \to \|F (k) - A\| < y$
52	51	ralrimiva	$⊢ ((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \to \forall k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)} \|F (k) - A\| < y$
53		fveq2	$⊢ j = if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M) \to ℤ_{\geq j} = ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)}$
54	53	raleqdv	$⊢ j = if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M) \to (\forall k \in ℤ_{\geq j} \|F (k) - A\| < y \leftrightarrow \forall k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)} \|F (k) - A\| < y)$
55	54	rspcev	$⊢ (if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M) \in Z \land \forall k \in ℤ_{\geq if (M \leq ⌊z⌋ + 1, ⌊z⌋ + 1, M)} \|F (k) - A\| < y) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < y$
56	27 52 55	syl2anc	$⊢ ((φ \land y \in ℝ^{+}) \land (z \in ℝ \land \forall w \in dom F (z \leq w \to \|F (w) - A\| < y))) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < y$
57	15 56	rexlimddv	$⊢ (φ \land y \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < y$
58	57	ralrimiva	$⊢ φ \to \forall y \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < y$
59		rlimpm	$⊢ F \underset{ℝ}{⇝} A \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
60	3 59	syl	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
61		eqidd	$⊢ (φ \land k \in Z) \to F (k) = F (k)$
62		rlimcl	$⊢ F \underset{ℝ}{⇝} A \to A \in ℂ$
63	3 62	syl	$⊢ φ \to A \in ℂ$
64	4	sselda	$⊢ (φ \land k \in Z) \to k \in dom F$
65	10	ffvelrnda	$⊢ (φ \land k \in dom F) \to F (k) \in ℂ$
66	64 65	syldan	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
67	1 2 60 61 63 66	clim2c	$⊢ φ \to (F ⇝ A \leftrightarrow \forall y \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < y)$
68	58 67	mpbird	$⊢ φ \to F ⇝ A$

Metamath Proof Explorer

Theorem rlimclim1

Proof