Metamath Proof Explorer

Theorem lmdvg

Description: If a monotonic sequence of real numbers diverges, it is unbounded. (Contributed by Thierry Arnoux, 4-Aug-2017)

Ref Expression
Hypotheses lmdvg.1 
|- ( ph -> F : NN --> ( 0 [,) +oo ) )
lmdvg.2 
|- ( ( ph /\ k e. NN ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )
lmdvg.3 
|- ( ph -> -. F e. dom ~~> )
Assertion lmdvg 
|- ( ph -> A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < ( F ` k ) )

Proof

Step Hyp Ref Expression
1 lmdvg.1 
 |-  ( ph -> F : NN --> ( 0 [,) +oo ) )
2 lmdvg.2 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )
3 lmdvg.3 
 |-  ( ph -> -. F e. dom ~~> )
4 nnuz 
 |-  NN = ( ZZ>= ` 1 )
5 1zzd 
 |-  ( ( ph /\ E. x e. RR A. j e. NN ( F ` j ) <_ x ) -> 1 e. ZZ )
6 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
7 fss 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : NN --> RR )
8 1 6 7 sylancl 
 |-  ( ph -> F : NN --> RR )
9 8 adantr 
 |-  ( ( ph /\ E. x e. RR A. j e. NN ( F ` j ) <_ x ) -> F : NN --> RR )
10 2 ralrimiva 
 |-  ( ph -> A. k e. NN ( F ` k ) <_ ( F ` ( k + 1 ) ) )
11 fveq2 
 |-  ( k = l -> ( F ` k ) = ( F ` l ) )
12 fvoveq1 
 |-  ( k = l -> ( F ` ( k + 1 ) ) = ( F ` ( l + 1 ) ) )
13 11 12 breq12d 
 |-  ( k = l -> ( ( F ` k ) <_ ( F ` ( k + 1 ) ) <-> ( F ` l ) <_ ( F ` ( l + 1 ) ) ) )
14 13 cbvralvw 
 |-  ( A. k e. NN ( F ` k ) <_ ( F ` ( k + 1 ) ) <-> A. l e. NN ( F ` l ) <_ ( F ` ( l + 1 ) ) )
15 10 14 sylib 
 |-  ( ph -> A. l e. NN ( F ` l ) <_ ( F ` ( l + 1 ) ) )
16 15 r19.21bi 
 |-  ( ( ph /\ l e. NN ) -> ( F ` l ) <_ ( F ` ( l + 1 ) ) )
17 16 adantlr 
 |-  ( ( ( ph /\ E. x e. RR A. j e. NN ( F ` j ) <_ x ) /\ l e. NN ) -> ( F ` l ) <_ ( F ` ( l + 1 ) ) )
18 simpr 
 |-  ( ( ph /\ E. x e. RR A. j e. NN ( F ` j ) <_ x ) -> E. x e. RR A. j e. NN ( F ` j ) <_ x )
19 fveq2 
 |-  ( j = l -> ( F ` j ) = ( F ` l ) )
20 19 breq1d 
 |-  ( j = l -> ( ( F ` j ) <_ x <-> ( F ` l ) <_ x ) )
21 20 cbvralvw 
 |-  ( A. j e. NN ( F ` j ) <_ x <-> A. l e. NN ( F ` l ) <_ x )
22 21 rexbii 
 |-  ( E. x e. RR A. j e. NN ( F ` j ) <_ x <-> E. x e. RR A. l e. NN ( F ` l ) <_ x )
23 18 22 sylib 
 |-  ( ( ph /\ E. x e. RR A. j e. NN ( F ` j ) <_ x ) -> E. x e. RR A. l e. NN ( F ` l ) <_ x )
24 4 5 9 17 23 climsup 
 |-  ( ( ph /\ E. x e. RR A. j e. NN ( F ` j ) <_ x ) -> F ~~> sup ( ran F , RR , < ) )
25 nnex 
 |-  NN e. _V
26 fex 
 |-  ( ( F : NN --> ( 0 [,) +oo ) /\ NN e. _V ) -> F e. _V )
27 1 25 26 sylancl 
 |-  ( ph -> F e. _V )
28 27 adantr 
 |-  ( ( ph /\ F ~~> sup ( ran F , RR , < ) ) -> F e. _V )
29 ltso 
 |-  < Or RR
30 29 supex 
 |-  sup ( ran F , RR , < ) e. _V
31 30 a1i 
 |-  ( ( ph /\ F ~~> sup ( ran F , RR , < ) ) -> sup ( ran F , RR , < ) e. _V )
32 simpr 
 |-  ( ( ph /\ F ~~> sup ( ran F , RR , < ) ) -> F ~~> sup ( ran F , RR , < ) )
33 breldmg 
 |-  ( ( F e. _V /\ sup ( ran F , RR , < ) e. _V /\ F ~~> sup ( ran F , RR , < ) ) -> F e. dom ~~> )
34 28 31 32 33 syl3anc 
 |-  ( ( ph /\ F ~~> sup ( ran F , RR , < ) ) -> F e. dom ~~> )
35 24 34 syldan 
 |-  ( ( ph /\ E. x e. RR A. j e. NN ( F ` j ) <_ x ) -> F e. dom ~~> )
36 3 35 mtand 
 |-  ( ph -> -. E. x e. RR A. j e. NN ( F ` j ) <_ x )
37 ralnex 
 |-  ( A. x e. RR -. A. j e. NN ( F ` j ) <_ x <-> -. E. x e. RR A. j e. NN ( F ` j ) <_ x )
38 36 37 sylibr 
 |-  ( ph -> A. x e. RR -. A. j e. NN ( F ` j ) <_ x )
39 simplr 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> x e. RR )
40 8 adantr 
 |-  ( ( ph /\ x e. RR ) -> F : NN --> RR )
41 40 ffvelrnda 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( F ` j ) e. RR )
42 39 41 ltnled 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( x < ( F ` j ) <-> -. ( F ` j ) <_ x ) )
43 42 rexbidva 
 |-  ( ( ph /\ x e. RR ) -> ( E. j e. NN x < ( F ` j ) <-> E. j e. NN -. ( F ` j ) <_ x ) )
44 rexnal 
 |-  ( E. j e. NN -. ( F ` j ) <_ x <-> -. A. j e. NN ( F ` j ) <_ x )
45 43 44 bitrdi 
 |-  ( ( ph /\ x e. RR ) -> ( E. j e. NN x < ( F ` j ) <-> -. A. j e. NN ( F ` j ) <_ x ) )
46 45 ralbidva 
 |-  ( ph -> ( A. x e. RR E. j e. NN x < ( F ` j ) <-> A. x e. RR -. A. j e. NN ( F ` j ) <_ x ) )
47 38 46 mpbird 
 |-  ( ph -> A. x e. RR E. j e. NN x < ( F ` j ) )
48 47 r19.21bi 
 |-  ( ( ph /\ x e. RR ) -> E. j e. NN x < ( F ` j ) )
49 39 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. NN ) /\ x < ( F ` j ) ) /\ k e. ( ZZ>= ` j ) ) -> x e. RR )
50 41 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. NN ) /\ x < ( F ` j ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` j ) e. RR )
51 40 ad3antrrr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. NN ) /\ x < ( F ` j ) ) /\ k e. ( ZZ>= ` j ) ) -> F : NN --> RR )
52 uznnssnn 
 |-  ( j e. NN -> ( ZZ>= ` j ) C_ NN )
53 52 ad3antlr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. NN ) /\ x < ( F ` j ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ZZ>= ` j ) C_ NN )
54 simpr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. NN ) /\ x < ( F ` j ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. ( ZZ>= ` j ) )
55 53 54 sseldd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. NN ) /\ x < ( F ` j ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
56 51 55 ffvelrnd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. NN ) /\ x < ( F ` j ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. RR )
57 simplr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. NN ) /\ x < ( F ` j ) ) /\ k e. ( ZZ>= ` j ) ) -> x < ( F ` j ) )
58 simp-4l 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. NN ) /\ x < ( F ` j ) ) /\ k e. ( ZZ>= ` j ) ) -> ph )
59 simpllr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. NN ) /\ x < ( F ` j ) ) /\ k e. ( ZZ>= ` j ) ) -> j e. NN )
60 simpr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> k e. ( ZZ>= ` j ) )
61 8 ad3antrrr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) /\ l e. ( j ... k ) ) -> F : NN --> RR )
62 fzssnn 
 |-  ( j e. NN -> ( j ... k ) C_ NN )
63 62 ad3antlr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) /\ l e. ( j ... k ) ) -> ( j ... k ) C_ NN )
64 simpr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) /\ l e. ( j ... k ) ) -> l e. ( j ... k ) )
65 63 64 sseldd 
 |-  ( ( ( ( ph /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) /\ l e. ( j ... k ) ) -> l e. NN )
66 61 65 ffvelrnd 
 |-  ( ( ( ( ph /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) /\ l e. ( j ... k ) ) -> ( F ` l ) e. RR )
67 simplll 
 |-  ( ( ( ( ph /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) /\ l e. ( j ... ( k - 1 ) ) ) -> ph )
68 fzssnn 
 |-  ( j e. NN -> ( j ... ( k - 1 ) ) C_ NN )
69 68 ad3antlr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) /\ l e. ( j ... ( k - 1 ) ) ) -> ( j ... ( k - 1 ) ) C_ NN )
70 simpr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) /\ l e. ( j ... ( k - 1 ) ) ) -> l e. ( j ... ( k - 1 ) ) )
71 69 70 sseldd 
 |-  ( ( ( ( ph /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) /\ l e. ( j ... ( k - 1 ) ) ) -> l e. NN )
72 67 71 16 syl2anc 
 |-  ( ( ( ( ph /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) /\ l e. ( j ... ( k - 1 ) ) ) -> ( F ` l ) <_ ( F ` ( l + 1 ) ) )
73 60 66 72 monoord 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` j ) <_ ( F ` k ) )
74 58 59 54 73 syl21anc 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. NN ) /\ x < ( F ` j ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` j ) <_ ( F ` k ) )
75 49 50 56 57 74 ltletrd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. NN ) /\ x < ( F ` j ) ) /\ k e. ( ZZ>= ` j ) ) -> x < ( F ` k ) )
76 75 ralrimiva 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. NN ) /\ x < ( F ` j ) ) -> A. k e. ( ZZ>= ` j ) x < ( F ` k ) )
77 76 ex 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. NN ) -> ( x < ( F ` j ) -> A. k e. ( ZZ>= ` j ) x < ( F ` k ) ) )
78 77 reximdva 
 |-  ( ( ph /\ x e. RR ) -> ( E. j e. NN x < ( F ` j ) -> E. j e. NN A. k e. ( ZZ>= ` j ) x < ( F ` k ) ) )
79 48 78 mpd 
 |-  ( ( ph /\ x e. RR ) -> E. j e. NN A. k e. ( ZZ>= ` j ) x < ( F ` k ) )
80 79 ralrimiva 
 |-  ( ph -> A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < ( F ` k ) )