Metamath Proof Explorer

Theorem 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 : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) /\ A e. NN ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` A ) )

Proof

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