lmnn

Description: A condition that implies convergence. (Contributed by NM, 8-Jun-2007) (Revised by Mario Carneiro, 1-May-2014)

	Ref	Expression
Hypotheses	lmnn.2	$⊢ J = MetOpen (D)$
	lmnn.3	$⊢ φ \to D \in ∞Met (X)$
	lmnn.4	$⊢ φ \to P \in X$
	lmnn.5	$⊢ φ \to F : ℕ ⟶ X$
	lmnn.6	$⊢ (φ \land k \in ℕ) \to F (k) D P < \frac{1}{k}$
Assertion	lmnn	$⊢ φ \to F \underset{t}{⇝} (J) P$

Proof

Step	Hyp	Ref	Expression
1		lmnn.2	$⊢ J = MetOpen (D)$
2		lmnn.3	$⊢ φ \to D \in ∞Met (X)$
3		lmnn.4	$⊢ φ \to P \in X$
4		lmnn.5	$⊢ φ \to F : ℕ ⟶ X$
5		lmnn.6	$⊢ (φ \land k \in ℕ) \to F (k) D P < \frac{1}{k}$
6		rpreccl	$⊢ x \in ℝ^{+} \to \frac{1}{x} \in ℝ^{+}$
7	6	adantl	$⊢ (φ \land x \in ℝ^{+}) \to \frac{1}{x} \in ℝ^{+}$
8	7	rpred	$⊢ (φ \land x \in ℝ^{+}) \to \frac{1}{x} \in ℝ$
9	7	rpge0d	$⊢ (φ \land x \in ℝ^{+}) \to 0 \leq \frac{1}{x}$
10		flge0nn0	$⊢ (\frac{1}{x} \in ℝ \land 0 \leq \frac{1}{x}) \to ⌊\frac{1}{x}⌋ \in ℕ_{0}$
11	8 9 10	syl2anc	$⊢ (φ \land x \in ℝ^{+}) \to ⌊\frac{1}{x}⌋ \in ℕ_{0}$
12		nn0p1nn	$⊢ ⌊\frac{1}{x}⌋ \in ℕ_{0} \to ⌊\frac{1}{x}⌋ + 1 \in ℕ$
13	11 12	syl	$⊢ (φ \land x \in ℝ^{+}) \to ⌊\frac{1}{x}⌋ + 1 \in ℕ$
14	2	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to D \in ∞Met (X)$
15	4	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to F : ℕ ⟶ X$
16		eluznn	$⊢ (⌊\frac{1}{x}⌋ + 1 \in ℕ \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to k \in ℕ$
17	13 16	sylan	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to k \in ℕ$
18	15 17	ffvelrnd	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to F (k) \in X$
19	3	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to P \in X$
20		xmetcl	$⊢ (D \in ∞Met (X) \land F (k) \in X \land P \in X) \to F (k) D P \in ℝ^{*}$
21	14 18 19 20	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to F (k) D P \in ℝ^{*}$
22	17	nnrecred	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to \frac{1}{k} \in ℝ$
23	22	rexrd	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to \frac{1}{k} \in ℝ^{*}$
24		rpxr	$⊢ x \in ℝ^{+} \to x \in ℝ^{*}$
25	24	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to x \in ℝ^{*}$
26	5	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℕ) \to F (k) D P < \frac{1}{k}$
27	17 26	syldan	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to F (k) D P < \frac{1}{k}$
28	8	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to \frac{1}{x} \in ℝ$
29	13	nnred	$⊢ (φ \land x \in ℝ^{+}) \to ⌊\frac{1}{x}⌋ + 1 \in ℝ$
30	29	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to ⌊\frac{1}{x}⌋ + 1 \in ℝ$
31	17	nnred	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to k \in ℝ$
32		flltp1	$⊢ \frac{1}{x} \in ℝ \to \frac{1}{x} < ⌊\frac{1}{x}⌋ + 1$
33	28 32	syl	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to \frac{1}{x} < ⌊\frac{1}{x}⌋ + 1$
34		eluzle	$⊢ k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)} \to ⌊\frac{1}{x}⌋ + 1 \leq k$
35	34	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to ⌊\frac{1}{x}⌋ + 1 \leq k$
36	28 30 31 33 35	ltletrd	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to \frac{1}{x} < k$
37		simplr	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to x \in ℝ^{+}$
38		rpregt0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 < x)$
39		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
40	39	rpregt0d	$⊢ k \in ℕ \to (k \in ℝ \land 0 < k)$
41		ltrec1	$⊢ ((x \in ℝ \land 0 < x) \land (k \in ℝ \land 0 < k)) \to (\frac{1}{x} < k \leftrightarrow \frac{1}{k} < x)$
42	38 40 41	syl2an	$⊢ (x \in ℝ^{+} \land k \in ℕ) \to (\frac{1}{x} < k \leftrightarrow \frac{1}{k} < x)$
43	37 17 42	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to (\frac{1}{x} < k \leftrightarrow \frac{1}{k} < x)$
44	36 43	mpbid	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to \frac{1}{k} < x$
45	21 23 25 27 44	xrlttrd	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}) \to F (k) D P < x$
46	45	ralrimiva	$⊢ (φ \land x \in ℝ^{+}) \to \forall k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)} F (k) D P < x$
47		fveq2	$⊢ j = ⌊\frac{1}{x}⌋ + 1 \to ℤ_{\geq j} = ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)}$
48	47	raleqdv	$⊢ j = ⌊\frac{1}{x}⌋ + 1 \to (\forall k \in ℤ_{\geq j} F (k) D P < x \leftrightarrow \forall k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)} F (k) D P < x)$
49	48	rspcev	$⊢ (⌊\frac{1}{x}⌋ + 1 \in ℕ \land \forall k \in ℤ_{\geq (⌊\frac{1}{x}⌋ + 1)} F (k) D P < x) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) D P < x$
50	13 46 49	syl2anc	$⊢ (φ \land x \in ℝ^{+}) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) D P < x$
51	50	ralrimiva	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) D P < x$
52		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
53		1zzd	$⊢ φ \to 1 \in ℤ$
54		eqidd	$⊢ (φ \land k \in ℕ) \to F (k) = F (k)$
55	1 2 52 53 54 4	lmmbrf	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (P \in X \land \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) D P < x))$
56	3 51 55	mpbir2and	$⊢ φ \to F \underset{t}{⇝} (J) P$

Metamath Proof Explorer

Theorem lmnn

Proof