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 ${⊢}{\phi }\to {F}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
lmdvg.2 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({k}\right)\le {F}\left({k}+1\right)$
lmdvg.3 ${⊢}{\phi }\to ¬{F}\in \mathrm{dom}⇝$
Assertion lmdvg ${⊢}{\phi }\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{F}\left({k}\right)$

Proof

Step Hyp Ref Expression
1 lmdvg.1 ${⊢}{\phi }\to {F}:ℕ⟶\left[0,\mathrm{+\infty }\right)$
2 lmdvg.2 ${⊢}\left({\phi }\wedge {k}\in ℕ\right)\to {F}\left({k}\right)\le {F}\left({k}+1\right)$
3 lmdvg.3 ${⊢}{\phi }\to ¬{F}\in \mathrm{dom}⇝$
4 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
5 1zzd ${⊢}\left({\phi }\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}\right)\to 1\in ℤ$
6 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
7 fss ${⊢}\left({F}:ℕ⟶\left[0,\mathrm{+\infty }\right)\wedge \left[0,\mathrm{+\infty }\right)\subseteq ℝ\right)\to {F}:ℕ⟶ℝ$
8 1 6 7 sylancl ${⊢}{\phi }\to {F}:ℕ⟶ℝ$
9 8 adantr ${⊢}\left({\phi }\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}\right)\to {F}:ℕ⟶ℝ$
10 2 ralrimiva ${⊢}{\phi }\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\le {F}\left({k}+1\right)$
11 fveq2 ${⊢}{k}={l}\to {F}\left({k}\right)={F}\left({l}\right)$
12 fvoveq1 ${⊢}{k}={l}\to {F}\left({k}+1\right)={F}\left({l}+1\right)$
13 11 12 breq12d ${⊢}{k}={l}\to \left({F}\left({k}\right)\le {F}\left({k}+1\right)↔{F}\left({l}\right)\le {F}\left({l}+1\right)\right)$
14 13 cbvralvw ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)\le {F}\left({k}+1\right)↔\forall {l}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)\le {F}\left({l}+1\right)$
15 10 14 sylib ${⊢}{\phi }\to \forall {l}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)\le {F}\left({l}+1\right)$
16 15 r19.21bi ${⊢}\left({\phi }\wedge {l}\in ℕ\right)\to {F}\left({l}\right)\le {F}\left({l}+1\right)$
17 16 adantlr ${⊢}\left(\left({\phi }\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}\right)\wedge {l}\in ℕ\right)\to {F}\left({l}\right)\le {F}\left({l}+1\right)$
18 simpr ${⊢}\left({\phi }\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}$
19 fveq2 ${⊢}{j}={l}\to {F}\left({j}\right)={F}\left({l}\right)$
20 19 breq1d ${⊢}{j}={l}\to \left({F}\left({j}\right)\le {x}↔{F}\left({l}\right)\le {x}\right)$
21 20 cbvralvw ${⊢}\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}↔\forall {l}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)\le {x}$
22 21 rexbii ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {l}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)\le {x}$
23 18 22 sylib ${⊢}\left({\phi }\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {l}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({l}\right)\le {x}$
24 4 5 9 17 23 climsup ${⊢}\left({\phi }\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}\right)\to {F}⇝sup\left(\mathrm{ran}{F},ℝ,<\right)$
25 nnex ${⊢}ℕ\in \mathrm{V}$
26 fex ${⊢}\left({F}:ℕ⟶\left[0,\mathrm{+\infty }\right)\wedge ℕ\in \mathrm{V}\right)\to {F}\in \mathrm{V}$
27 1 25 26 sylancl ${⊢}{\phi }\to {F}\in \mathrm{V}$
28 27 adantr ${⊢}\left({\phi }\wedge {F}⇝sup\left(\mathrm{ran}{F},ℝ,<\right)\right)\to {F}\in \mathrm{V}$
29 ltso ${⊢}<\mathrm{Or}ℝ$
30 29 supex ${⊢}sup\left(\mathrm{ran}{F},ℝ,<\right)\in \mathrm{V}$
31 30 a1i ${⊢}\left({\phi }\wedge {F}⇝sup\left(\mathrm{ran}{F},ℝ,<\right)\right)\to sup\left(\mathrm{ran}{F},ℝ,<\right)\in \mathrm{V}$
32 simpr ${⊢}\left({\phi }\wedge {F}⇝sup\left(\mathrm{ran}{F},ℝ,<\right)\right)\to {F}⇝sup\left(\mathrm{ran}{F},ℝ,<\right)$
33 breldmg ${⊢}\left({F}\in \mathrm{V}\wedge sup\left(\mathrm{ran}{F},ℝ,<\right)\in \mathrm{V}\wedge {F}⇝sup\left(\mathrm{ran}{F},ℝ,<\right)\right)\to {F}\in \mathrm{dom}⇝$
34 28 31 32 33 syl3anc ${⊢}\left({\phi }\wedge {F}⇝sup\left(\mathrm{ran}{F},ℝ,<\right)\right)\to {F}\in \mathrm{dom}⇝$
35 24 34 syldan ${⊢}\left({\phi }\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}\right)\to {F}\in \mathrm{dom}⇝$
36 3 35 mtand ${⊢}{\phi }\to ¬\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}$
37 ralnex ${⊢}\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}¬\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}↔¬\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}$
38 36 37 sylibr ${⊢}{\phi }\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}¬\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}$
39 simplr ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\to {x}\in ℝ$
40 8 adantr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to {F}:ℕ⟶ℝ$
41 40 ffvelrnda ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\to {F}\left({j}\right)\in ℝ$
42 39 41 ltnled ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\to \left({x}<{F}\left({j}\right)↔¬{F}\left({j}\right)\le {x}\right)$
43 42 rexbidva ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{x}<{F}\left({j}\right)↔\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}¬{F}\left({j}\right)\le {x}\right)$
44 rexnal ${⊢}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}¬{F}\left({j}\right)\le {x}↔¬\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}$
45 43 44 syl6bb ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{x}<{F}\left({j}\right)↔¬\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}\right)$
46 45 ralbidva ${⊢}{\phi }\to \left(\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{x}<{F}\left({j}\right)↔\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}¬\forall {j}\in ℕ\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)\le {x}\right)$
47 38 46 mpbird ${⊢}{\phi }\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{x}<{F}\left({j}\right)$
48 47 r19.21bi ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{x}<{F}\left({j}\right)$
49 39 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\wedge {x}<{F}\left({j}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {x}\in ℝ$
50 41 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\wedge {x}<{F}\left({j}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {F}\left({j}\right)\in ℝ$
51 40 ad3antrrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\wedge {x}<{F}\left({j}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {F}:ℕ⟶ℝ$
52 uznnssnn ${⊢}{j}\in ℕ\to {ℤ}_{\ge {j}}\subseteq ℕ$
53 52 ad3antlr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\wedge {x}<{F}\left({j}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {ℤ}_{\ge {j}}\subseteq ℕ$
54 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\wedge {x}<{F}\left({j}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {ℤ}_{\ge {j}}$
55 53 54 sseldd ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\wedge {x}<{F}\left({j}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in ℕ$
56 51 55 ffvelrnd ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\wedge {x}<{F}\left({j}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {F}\left({k}\right)\in ℝ$
57 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\wedge {x}<{F}\left({j}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {x}<{F}\left({j}\right)$
58 simp-4l ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\wedge {x}<{F}\left({j}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {\phi }$
59 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\wedge {x}<{F}\left({j}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {j}\in ℕ$
60 simpr ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {k}\in {ℤ}_{\ge {j}}$
61 8 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {l}\in \left({j}\dots {k}\right)\right)\to {F}:ℕ⟶ℝ$
62 fzssnn ${⊢}{j}\in ℕ\to \left({j}\dots {k}\right)\subseteq ℕ$
63 62 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {l}\in \left({j}\dots {k}\right)\right)\to \left({j}\dots {k}\right)\subseteq ℕ$
64 simpr ${⊢}\left(\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {l}\in \left({j}\dots {k}\right)\right)\to {l}\in \left({j}\dots {k}\right)$
65 63 64 sseldd ${⊢}\left(\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {l}\in \left({j}\dots {k}\right)\right)\to {l}\in ℕ$
66 61 65 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {l}\in \left({j}\dots {k}\right)\right)\to {F}\left({l}\right)\in ℝ$
67 simplll ${⊢}\left(\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {l}\in \left({j}\dots {k}-1\right)\right)\to {\phi }$
68 fzssnn ${⊢}{j}\in ℕ\to \left({j}\dots {k}-1\right)\subseteq ℕ$
69 68 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {l}\in \left({j}\dots {k}-1\right)\right)\to \left({j}\dots {k}-1\right)\subseteq ℕ$
70 simpr ${⊢}\left(\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {l}\in \left({j}\dots {k}-1\right)\right)\to {l}\in \left({j}\dots {k}-1\right)$
71 69 70 sseldd ${⊢}\left(\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {l}\in \left({j}\dots {k}-1\right)\right)\to {l}\in ℕ$
72 67 71 16 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\wedge {l}\in \left({j}\dots {k}-1\right)\right)\to {F}\left({l}\right)\le {F}\left({l}+1\right)$
73 60 66 72 monoord ${⊢}\left(\left({\phi }\wedge {j}\in ℕ\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {F}\left({j}\right)\le {F}\left({k}\right)$
74 58 59 54 73 syl21anc ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\wedge {x}<{F}\left({j}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {F}\left({j}\right)\le {F}\left({k}\right)$
75 49 50 56 57 74 ltletrd ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\wedge {x}<{F}\left({j}\right)\right)\wedge {k}\in {ℤ}_{\ge {j}}\right)\to {x}<{F}\left({k}\right)$
76 75 ralrimiva ${⊢}\left(\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\wedge {x}<{F}\left({j}\right)\right)\to \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{F}\left({k}\right)$
77 76 ex ${⊢}\left(\left({\phi }\wedge {x}\in ℝ\right)\wedge {j}\in ℕ\right)\to \left({x}<{F}\left({j}\right)\to \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{F}\left({k}\right)\right)$
78 77 reximdva ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{x}<{F}\left({j}\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{F}\left({k}\right)\right)$
79 48 78 mpd ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{F}\left({k}\right)$
80 79 ralrimiva ${⊢}{\phi }\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{x}<{F}\left({k}\right)$