Metamath Proof Explorer


Theorem 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 : m F m < F m + 1 A n k n F k A

Proof

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