incsequz2

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

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

Proof

Step	Hyp	Ref	Expression
1		incsequz	$⊢ (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1) \land A \in ℕ) \to \exists n \in ℕ F (n) \in ℤ_{\geq A}$
2		nnssre	$⊢ ℕ \subseteq ℝ$
3		ltso	$⊢ < Or ℝ$
4		sopo	$⊢ < Or ℝ \to < Po ℝ$
5	3 4	ax-mp	$⊢ < Po ℝ$
6		poss	$⊢ ℕ \subseteq ℝ \to (< Po ℝ \to < Po ℕ)$
7	2 5 6	mp2	$⊢ < Po ℕ$
8		seqpo	$⊢ (< Po ℕ \land F : ℕ ⟶ ℕ) \to (\forall m \in ℕ F (m) < F (m + 1) \leftrightarrow \forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q))$
9	7 8	mpan	$⊢ F : ℕ ⟶ ℕ \to (\forall m \in ℕ F (m) < F (m + 1) \leftrightarrow \forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q))$
10	9	biimpd	$⊢ F : ℕ ⟶ ℕ \to (\forall m \in ℕ F (m) < F (m + 1) \to \forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q))$
11	10	imdistani	$⊢ (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1)) \to (F : ℕ ⟶ ℕ \land \forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q))$
12		uzp1	$⊢ k \in ℤ_{\geq n} \to (k = n \lor k \in ℤ_{\geq (n + 1)})$
13		fveq2	$⊢ k = n \to F (k) = F (n)$
14	13	adantl	$⊢ ((F : ℕ ⟶ ℕ \land n \in ℕ) \land k = n) \to F (k) = F (n)$
15		ffvelcdm	$⊢ (F : ℕ ⟶ ℕ \land n \in ℕ) \to F (n) \in ℕ$
16	15	nnzd	$⊢ (F : ℕ ⟶ ℕ \land n \in ℕ) \to F (n) \in ℤ$
17		uzid	$⊢ F (n) \in ℤ \to F (n) \in ℤ_{\geq F (n)}$
18	16 17	syl	$⊢ (F : ℕ ⟶ ℕ \land n \in ℕ) \to F (n) \in ℤ_{\geq F (n)}$
19	18	adantr	$⊢ ((F : ℕ ⟶ ℕ \land n \in ℕ) \land k = n) \to F (n) \in ℤ_{\geq F (n)}$
20	14 19	eqeltrd	$⊢ ((F : ℕ ⟶ ℕ \land n \in ℕ) \land k = n) \to F (k) \in ℤ_{\geq F (n)}$
21	20	adantllr	$⊢ (((F : ℕ ⟶ ℕ \land \forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q)) \land n \in ℕ) \land k = n) \to F (k) \in ℤ_{\geq F (n)}$
22		fvoveq1	$⊢ p = n \to ℤ_{\geq (p + 1)} = ℤ_{\geq (n + 1)}$
23		fveq2	$⊢ p = n \to F (p) = F (n)$
24	23	breq1d	$⊢ p = n \to (F (p) < F (q) \leftrightarrow F (n) < F (q))$
25	22 24	raleqbidv	$⊢ p = n \to (\forall q \in ℤ_{\geq (p + 1)} F (p) < F (q) \leftrightarrow \forall q \in ℤ_{\geq (n + 1)} F (n) < F (q))$
26	25	rspccva	$⊢ (\forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q) \land n \in ℕ) \to \forall q \in ℤ_{\geq (n + 1)} F (n) < F (q)$
27		fveq2	$⊢ q = k \to F (q) = F (k)$
28	27	breq2d	$⊢ q = k \to (F (n) < F (q) \leftrightarrow F (n) < F (k))$
29	28	rspccva	$⊢ (\forall q \in ℤ_{\geq (n + 1)} F (n) < F (q) \land k \in ℤ_{\geq (n + 1)}) \to F (n) < F (k)$
30	26 29	sylan	$⊢ ((\forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q) \land n \in ℕ) \land k \in ℤ_{\geq (n + 1)}) \to F (n) < F (k)$
31	30	adantlll	$⊢ (((F : ℕ ⟶ ℕ \land \forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q)) \land n \in ℕ) \land k \in ℤ_{\geq (n + 1)}) \to F (n) < F (k)$
32	16	adantr	$⊢ ((F : ℕ ⟶ ℕ \land n \in ℕ) \land k \in ℤ_{\geq (n + 1)}) \to F (n) \in ℤ$
33		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
34		elnnuz	$⊢ n + 1 \in ℕ \leftrightarrow n + 1 \in ℤ_{\geq 1}$
35	33 34	sylib	$⊢ n \in ℕ \to n + 1 \in ℤ_{\geq 1}$
36		uztrn	$⊢ (k \in ℤ_{\geq (n + 1)} \land n + 1 \in ℤ_{\geq 1}) \to k \in ℤ_{\geq 1}$
37	36	ancoms	$⊢ (n + 1 \in ℤ_{\geq 1} \land k \in ℤ_{\geq (n + 1)}) \to k \in ℤ_{\geq 1}$
38		elnnuz	$⊢ k \in ℕ \leftrightarrow k \in ℤ_{\geq 1}$
39	37 38	sylibr	$⊢ (n + 1 \in ℤ_{\geq 1} \land k \in ℤ_{\geq (n + 1)}) \to k \in ℕ$
40	35 39	sylan	$⊢ (n \in ℕ \land k \in ℤ_{\geq (n + 1)}) \to k \in ℕ$
41		ffvelcdm	$⊢ (F : ℕ ⟶ ℕ \land k \in ℕ) \to F (k) \in ℕ$
42	41	nnzd	$⊢ (F : ℕ ⟶ ℕ \land k \in ℕ) \to F (k) \in ℤ$
43	40 42	sylan2	$⊢ (F : ℕ ⟶ ℕ \land (n \in ℕ \land k \in ℤ_{\geq (n + 1)})) \to F (k) \in ℤ$
44	43	anassrs	$⊢ ((F : ℕ ⟶ ℕ \land n \in ℕ) \land k \in ℤ_{\geq (n + 1)}) \to F (k) \in ℤ$
45		zre	$⊢ F (n) \in ℤ \to F (n) \in ℝ$
46		zre	$⊢ F (k) \in ℤ \to F (k) \in ℝ$
47		ltle	$⊢ (F (n) \in ℝ \land F (k) \in ℝ) \to (F (n) < F (k) \to F (n) \leq F (k))$
48	45 46 47	syl2an	$⊢ (F (n) \in ℤ \land F (k) \in ℤ) \to (F (n) < F (k) \to F (n) \leq F (k))$
49		eluz	$⊢ (F (n) \in ℤ \land F (k) \in ℤ) \to (F (k) \in ℤ_{\geq F (n)} \leftrightarrow F (n) \leq F (k))$
50	48 49	sylibrd	$⊢ (F (n) \in ℤ \land F (k) \in ℤ) \to (F (n) < F (k) \to F (k) \in ℤ_{\geq F (n)})$
51	32 44 50	syl2anc	$⊢ ((F : ℕ ⟶ ℕ \land n \in ℕ) \land k \in ℤ_{\geq (n + 1)}) \to (F (n) < F (k) \to F (k) \in ℤ_{\geq F (n)})$
52	51	adantllr	$⊢ (((F : ℕ ⟶ ℕ \land \forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q)) \land n \in ℕ) \land k \in ℤ_{\geq (n + 1)}) \to (F (n) < F (k) \to F (k) \in ℤ_{\geq F (n)})$
53	31 52	mpd	$⊢ (((F : ℕ ⟶ ℕ \land \forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q)) \land n \in ℕ) \land k \in ℤ_{\geq (n + 1)}) \to F (k) \in ℤ_{\geq F (n)}$
54	21 53	jaodan	$⊢ (((F : ℕ ⟶ ℕ \land \forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q)) \land n \in ℕ) \land (k = n \lor k \in ℤ_{\geq (n + 1)})) \to F (k) \in ℤ_{\geq F (n)}$
55	12 54	sylan2	$⊢ (((F : ℕ ⟶ ℕ \land \forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q)) \land n \in ℕ) \land k \in ℤ_{\geq n}) \to F (k) \in ℤ_{\geq F (n)}$
56		uztrn	$⊢ (F (k) \in ℤ_{\geq F (n)} \land F (n) \in ℤ_{\geq A}) \to F (k) \in ℤ_{\geq A}$
57	56	ex	$⊢ F (k) \in ℤ_{\geq F (n)} \to (F (n) \in ℤ_{\geq A} \to F (k) \in ℤ_{\geq A})$
58	55 57	syl	$⊢ (((F : ℕ ⟶ ℕ \land \forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q)) \land n \in ℕ) \land k \in ℤ_{\geq n}) \to (F (n) \in ℤ_{\geq A} \to F (k) \in ℤ_{\geq A})$
59	58	adantllr	$⊢ ((((F : ℕ ⟶ ℕ \land \forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q)) \land A \in ℕ) \land n \in ℕ) \land k \in ℤ_{\geq n}) \to (F (n) \in ℤ_{\geq A} \to F (k) \in ℤ_{\geq A})$
60	59	ralrimdva	$⊢ (((F : ℕ ⟶ ℕ \land \forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q)) \land A \in ℕ) \land n \in ℕ) \to (F (n) \in ℤ_{\geq A} \to \forall k \in ℤ_{\geq n} F (k) \in ℤ_{\geq A})$
61	60	ex	$⊢ ((F : ℕ ⟶ ℕ \land \forall p \in ℕ \forall q \in ℤ_{\geq (p + 1)} F (p) < F (q)) \land A \in ℕ) \to (n \in ℕ \to (F (n) \in ℤ_{\geq A} \to \forall k \in ℤ_{\geq n} F (k) \in ℤ_{\geq A}))$
62	11 61	stoic3	$⊢ (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1) \land A \in ℕ) \to (n \in ℕ \to (F (n) \in ℤ_{\geq A} \to \forall k \in ℤ_{\geq n} F (k) \in ℤ_{\geq A}))$
63	62	reximdvai	$⊢ (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1) \land A \in ℕ) \to (\exists n \in ℕ F (n) \in ℤ_{\geq A} \to \exists n \in ℕ \forall k \in ℤ_{\geq n} F (k) \in ℤ_{\geq A})$
64	1 63	mpd	$⊢ (F : ℕ ⟶ ℕ \land \forall m \in ℕ F (m) < F (m + 1) \land A \in ℕ) \to \exists n \in ℕ \forall k \in ℤ_{\geq n} F (k) \in ℤ_{\geq A}$

Metamath Proof Explorer

Theorem incsequz2

Proof