incsequz

Description: An increasing sequence of positive integers takes on indefinitely large values. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	incsequz	$⊢ (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1) \land A \in ℕ) \to \exists n \in ℕ F (n) \in ℤ_{\geq A}$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ p = 1 \to ℤ_{\geq p} = ℤ_{\geq 1}$
2	1	eleq2d	$⊢ p = 1 \to (F (n) \in ℤ_{\geq p} \leftrightarrow F (n) \in ℤ_{\geq 1})$
3	2	rexbidv	$⊢ p = 1 \to (\exists n \in ℕ F (n) \in ℤ_{\geq p} \leftrightarrow \exists n \in ℕ F (n) \in ℤ_{\geq 1})$
4	3	imbi2d	$⊢ p = 1 \to (((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to \exists n \in ℕ F (n) \in ℤ_{\geq p}) \leftrightarrow ((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to \exists n \in ℕ F (n) \in ℤ_{\geq 1}))$
5		fveq2	$⊢ p = q \to ℤ_{\geq p} = ℤ_{\geq q}$
6	5	eleq2d	$⊢ p = q \to (F (n) \in ℤ_{\geq p} \leftrightarrow F (n) \in ℤ_{\geq q})$
7	6	rexbidv	$⊢ p = q \to (\exists n \in ℕ F (n) \in ℤ_{\geq p} \leftrightarrow \exists n \in ℕ F (n) \in ℤ_{\geq q})$
8	7	imbi2d	$⊢ p = q \to (((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to \exists n \in ℕ F (n) \in ℤ_{\geq p}) \leftrightarrow ((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to \exists n \in ℕ F (n) \in ℤ_{\geq q}))$
9		fveq2	$⊢ p = q + 1 \to ℤ_{\geq p} = ℤ_{\geq (q + 1)}$
10	9	eleq2d	$⊢ p = q + 1 \to (F (n) \in ℤ_{\geq p} \leftrightarrow F (n) \in ℤ_{\geq (q + 1)})$
11	10	rexbidv	$⊢ p = q + 1 \to (\exists n \in ℕ F (n) \in ℤ_{\geq p} \leftrightarrow \exists n \in ℕ F (n) \in ℤ_{\geq (q + 1)})$
12	11	imbi2d	$⊢ p = q + 1 \to (((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to \exists n \in ℕ F (n) \in ℤ_{\geq p}) \leftrightarrow ((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to \exists n \in ℕ F (n) \in ℤ_{\geq (q + 1)}))$
13		fveq2	$⊢ p = A \to ℤ_{\geq p} = ℤ_{\geq A}$
14	13	eleq2d	$⊢ p = A \to (F (n) \in ℤ_{\geq p} \leftrightarrow F (n) \in ℤ_{\geq A})$
15	14	rexbidv	$⊢ p = A \to (\exists n \in ℕ F (n) \in ℤ_{\geq p} \leftrightarrow \exists n \in ℕ F (n) \in ℤ_{\geq A})$
16	15	imbi2d	$⊢ p = A \to (((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to \exists n \in ℕ F (n) \in ℤ_{\geq p}) \leftrightarrow ((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to \exists n \in ℕ F (n) \in ℤ_{\geq A}))$
17		1nn	$⊢ 1 \in ℕ$
18	17	ne0ii	$⊢ ℕ \neq \emptyset$
19		ffvelcdm	$⊢ (F : ℕ ⟶ ℕ \land n \in ℕ) \to F (n) \in ℕ$
20		elnnuz	$⊢ F (n) \in ℕ \leftrightarrow F (n) \in ℤ_{\geq 1}$
21	19 20	sylib	$⊢ (F : ℕ ⟶ ℕ \land n \in ℕ) \to F (n) \in ℤ_{\geq 1}$
22	21	ralrimiva	$⊢ F : ℕ ⟶ ℕ \to \forall n \in ℕ F (n) \in ℤ_{\geq 1}$
23		r19.2z	$⊢ (ℕ \neq \emptyset \land \forall n \in ℕ F (n) \in ℤ_{\geq 1}) \to \exists n \in ℕ F (n) \in ℤ_{\geq 1}$
24	18 22 23	sylancr	$⊢ F : ℕ ⟶ ℕ \to \exists n \in ℕ F (n) \in ℤ_{\geq 1}$
25	24	adantr	$⊢ (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to \exists n \in ℕ F (n) \in ℤ_{\geq 1}$
26		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
27	26	adantl	$⊢ ((q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \land n \in ℕ) \to n + 1 \in ℕ$
28		nnre	$⊢ q \in ℕ \to q \in ℝ$
29	28	ad2antrr	$⊢ ((q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \land n \in ℕ) \to q \in ℝ$
30	19	nnred	$⊢ (F : ℕ ⟶ ℕ \land n \in ℕ) \to F (n) \in ℝ$
31	30	adantlr	$⊢ ((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \land n \in ℕ) \to F (n) \in ℝ$
32	31	adantll	$⊢ ((q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \land n \in ℕ) \to F (n) \in ℝ$
33		1red	$⊢ ((q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \land n \in ℕ) \to 1 \in ℝ$
34	29 32 33	leadd1d	$⊢ ((q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \land n \in ℕ) \to (q \leq F (n) \leftrightarrow q + 1 \leq F (n) + 1)$
35		fveq2	$⊢ m = n \to F (m) = F (n)$
36		fvoveq1	$⊢ m = n \to F (m + 1) = F (n + 1)$
37	35 36	breq12d	$⊢ m = n \to (F (m) < F (m + 1) \leftrightarrow F (n) < F (n + 1))$
38	37	rspcv	$⊢ n \in ℕ \to (\forall m \in ℕ F (m) < F (m + 1) \to F (n) < F (n + 1))$
39	38	imdistani	$⊢ (n \in ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to (n \in ℕ \land F (n) < F (n + 1))$
40		ffvelcdm	$⊢ (F : ℕ ⟶ ℕ \land n + 1 \in ℕ) \to F (n + 1) \in ℕ$
41	26 40	sylan2	$⊢ (F : ℕ ⟶ ℕ \land n \in ℕ) \to F (n + 1) \in ℕ$
42		nnltp1le	$⊢ (F (n) \in ℕ \land F (n + 1) \in ℕ) \to (F (n) < F (n + 1) \leftrightarrow F (n) + 1 \leq F (n + 1))$
43	19 41 42	syl2anc	$⊢ (F : ℕ ⟶ ℕ \land n \in ℕ) \to (F (n) < F (n + 1) \leftrightarrow F (n) + 1 \leq F (n + 1))$
44	43	biimpa	$⊢ ((F : ℕ ⟶ ℕ \land n \in ℕ) \land F (n) < F (n + 1)) \to F (n) + 1 \leq F (n + 1)$
45	44	anasss	$⊢ (F : ℕ ⟶ ℕ \land (n \in ℕ \land F (n) < F (n + 1))) \to F (n) + 1 \leq F (n + 1)$
46	39 45	sylan2	$⊢ (F : ℕ ⟶ ℕ \land (n \in ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \to F (n) + 1 \leq F (n + 1)$
47	46	anass1rs	$⊢ ((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \land n \in ℕ) \to F (n) + 1 \leq F (n + 1)$
48	47	adantll	$⊢ ((q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \land n \in ℕ) \to F (n) + 1 \leq F (n + 1)$
49		peano2re	$⊢ q \in ℝ \to q + 1 \in ℝ$
50	28 49	syl	$⊢ q \in ℕ \to q + 1 \in ℝ$
51	50	ad2antrr	$⊢ ((q \in ℕ \land F : ℕ ⟶ ℕ) \land n \in ℕ) \to q + 1 \in ℝ$
52		peano2nn	$⊢ F (n) \in ℕ \to F (n) + 1 \in ℕ$
53	19 52	syl	$⊢ (F : ℕ ⟶ ℕ \land n \in ℕ) \to F (n) + 1 \in ℕ$
54	53	nnred	$⊢ (F : ℕ ⟶ ℕ \land n \in ℕ) \to F (n) + 1 \in ℝ$
55	54	adantll	$⊢ ((q \in ℕ \land F : ℕ ⟶ ℕ) \land n \in ℕ) \to F (n) + 1 \in ℝ$
56	40	nnred	$⊢ (F : ℕ ⟶ ℕ \land n + 1 \in ℕ) \to F (n + 1) \in ℝ$
57	26 56	sylan2	$⊢ (F : ℕ ⟶ ℕ \land n \in ℕ) \to F (n + 1) \in ℝ$
58	57	adantll	$⊢ ((q \in ℕ \land F : ℕ ⟶ ℕ) \land n \in ℕ) \to F (n + 1) \in ℝ$
59		letr	$⊢ (q + 1 \in ℝ \land F (n) + 1 \in ℝ \land F (n + 1) \in ℝ) \to ((q + 1 \leq F (n) + 1 \land F (n) + 1 \leq F (n + 1)) \to q + 1 \leq F (n + 1))$
60	51 55 58 59	syl3anc	$⊢ ((q \in ℕ \land F : ℕ ⟶ ℕ) \land n \in ℕ) \to ((q + 1 \leq F (n) + 1 \land F (n) + 1 \leq F (n + 1)) \to q + 1 \leq F (n + 1))$
61	60	adantlrr	$⊢ ((q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \land n \in ℕ) \to ((q + 1 \leq F (n) + 1 \land F (n) + 1 \leq F (n + 1)) \to q + 1 \leq F (n + 1))$
62	48 61	mpan2d	$⊢ ((q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \land n \in ℕ) \to (q + 1 \leq F (n) + 1 \to q + 1 \leq F (n + 1))$
63	34 62	sylbid	$⊢ ((q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \land n \in ℕ) \to (q \leq F (n) \to q + 1 \leq F (n + 1))$
64		nnz	$⊢ q \in ℕ \to q \in ℤ$
65	19	nnzd	$⊢ (F : ℕ ⟶ ℕ \land n \in ℕ) \to F (n) \in ℤ$
66		eluz	$⊢ (q \in ℤ \land F (n) \in ℤ) \to (F (n) \in ℤ_{\geq q} \leftrightarrow q \leq F (n))$
67	64 65 66	syl2an	$⊢ (q \in ℕ \land (F : ℕ ⟶ ℕ \land n \in ℕ)) \to (F (n) \in ℤ_{\geq q} \leftrightarrow q \leq F (n))$
68	67	adantrlr	$⊢ (q \in ℕ \land ((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \land n \in ℕ)) \to (F (n) \in ℤ_{\geq q} \leftrightarrow q \leq F (n))$
69	68	anassrs	$⊢ ((q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \land n \in ℕ) \to (F (n) \in ℤ_{\geq q} \leftrightarrow q \leq F (n))$
70	64	peano2zd	$⊢ q \in ℕ \to q + 1 \in ℤ$
71	40	nnzd	$⊢ (F : ℕ ⟶ ℕ \land n + 1 \in ℕ) \to F (n + 1) \in ℤ$
72	26 71	sylan2	$⊢ (F : ℕ ⟶ ℕ \land n \in ℕ) \to F (n + 1) \in ℤ$
73		eluz	$⊢ (q + 1 \in ℤ \land F (n + 1) \in ℤ) \to (F (n + 1) \in ℤ_{\geq (q + 1)} \leftrightarrow q + 1 \leq F (n + 1))$
74	70 72 73	syl2an	$⊢ (q \in ℕ \land (F : ℕ ⟶ ℕ \land n \in ℕ)) \to (F (n + 1) \in ℤ_{\geq (q + 1)} \leftrightarrow q + 1 \leq F (n + 1))$
75	74	adantrlr	$⊢ (q \in ℕ \land ((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \land n \in ℕ)) \to (F (n + 1) \in ℤ_{\geq (q + 1)} \leftrightarrow q + 1 \leq F (n + 1))$
76	75	anassrs	$⊢ ((q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \land n \in ℕ) \to (F (n + 1) \in ℤ_{\geq (q + 1)} \leftrightarrow q + 1 \leq F (n + 1))$
77	63 69 76	3imtr4d	$⊢ ((q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \land n \in ℕ) \to (F (n) \in ℤ_{\geq q} \to F (n + 1) \in ℤ_{\geq (q + 1)})$
78		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
79	78	eleq1d	$⊢ k = n + 1 \to (F (k) \in ℤ_{\geq (q + 1)} \leftrightarrow F (n + 1) \in ℤ_{\geq (q + 1)})$
80	79	rspcev	$⊢ (n + 1 \in ℕ \land F (n + 1) \in ℤ_{\geq (q + 1)}) \to \exists k \in ℕ F (k) \in ℤ_{\geq (q + 1)}$
81	27 77 80	syl6an	$⊢ ((q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \land n \in ℕ) \to (F (n) \in ℤ_{\geq q} \to \exists k \in ℕ F (k) \in ℤ_{\geq (q + 1)})$
82	81	rexlimdva	$⊢ (q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \to (\exists n \in ℕ F (n) \in ℤ_{\geq q} \to \exists k \in ℕ F (k) \in ℤ_{\geq (q + 1)})$
83		fveq2	$⊢ k = n \to F (k) = F (n)$
84	83	eleq1d	$⊢ k = n \to (F (k) \in ℤ_{\geq (q + 1)} \leftrightarrow F (n) \in ℤ_{\geq (q + 1)})$
85	84	cbvrexvw	$⊢ \exists k \in ℕ F (k) \in ℤ_{\geq (q + 1)} \leftrightarrow \exists n \in ℕ F (n) \in ℤ_{\geq (q + 1)}$
86	82 85	imbitrdi	$⊢ (q \in ℕ \land (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1))) \to (\exists n \in ℕ F (n) \in ℤ_{\geq q} \to \exists n \in ℕ F (n) \in ℤ_{\geq (q + 1)})$
87	86	ex	$⊢ q \in ℕ \to ((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to (\exists n \in ℕ F (n) \in ℤ_{\geq q} \to \exists n \in ℕ F (n) \in ℤ_{\geq (q + 1)}))$
88	87	a2d	$⊢ q \in ℕ \to (((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to \exists n \in ℕ F (n) \in ℤ_{\geq q}) \to ((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to \exists n \in ℕ F (n) \in ℤ_{\geq (q + 1)}))$
89	4 8 12 16 25 88	nnind	$⊢ A \in ℕ \to ((F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to \exists n \in ℕ F (n) \in ℤ_{\geq A})$
90	89	com12	$⊢ (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to (A \in ℕ \to \exists n \in ℕ F (n) \in ℤ_{\geq A})$
91	90	3impia	$⊢ (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1) \land A \in ℕ) \to \exists n \in ℕ F (n) \in ℤ_{\geq A}$

Metamath Proof Explorer

Theorem incsequz

Proof