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 φ F : 0 +∞
lmdvg.2 φ k F k F k + 1
lmdvg.3 φ ¬ F dom
Assertion lmdvg φ x j k j x < F k

Proof

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