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

Proof

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