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 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) )
lmdvg.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
lmdvg.3 ⊢ ( 𝜑 → ¬ 𝐹 ∈ dom ⇝ )
Assertion lmdvg ( 𝜑 → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) )

Proof

Step Hyp Ref Expression
1 lmdvg.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) )
2 lmdvg.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
3 lmdvg.3 ⊢ ( 𝜑 → ¬ 𝐹 ∈ dom ⇝ )
4 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
5 1zzd ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → 1 ∈ ℤ )
6 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
7 fss ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝐹 : ℕ ⟶ ℝ )
8 1 6 7 sylancl ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℝ )
9 8 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → 𝐹 : ℕ ⟶ ℝ )
10 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
11 fveq2 ⊢ ( 𝑘 = 𝑙 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑙 ) )
12 fvoveq1 ⊢ ( 𝑘 = 𝑙 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑙 + 1 ) ) )
13 11 12 breq12d ⊢ ( 𝑘 = 𝑙 → ( ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝐹 ‘ 𝑙 ) ≤ ( 𝐹 ‘ ( 𝑙 + 1 ) ) ) )
14 13 cbvralvw ⊢ ( ∀ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ↔ ∀ 𝑙 ∈ ℕ ( 𝐹 ‘ 𝑙 ) ≤ ( 𝐹 ‘ ( 𝑙 + 1 ) ) )
15 10 14 sylib ⊢ ( 𝜑 → ∀ 𝑙 ∈ ℕ ( 𝐹 ‘ 𝑙 ) ≤ ( 𝐹 ‘ ( 𝑙 + 1 ) ) )
16 15 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( 𝐹 ‘ 𝑙 ) ≤ ( 𝐹 ‘ ( 𝑙 + 1 ) ) )
17 16 adantlr ⊢ ( ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑙 ∈ ℕ ) → ( 𝐹 ‘ 𝑙 ) ≤ ( 𝐹 ‘ ( 𝑙 + 1 ) ) )
18 simpr ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
19 fveq2 ⊢ ( 𝑗 = 𝑙 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑙 ) )
20 19 breq1d ⊢ ( 𝑗 = 𝑙 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
21 20 cbvralvw ⊢ ( ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑙 ∈ ℕ ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
22 21 rexbii ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ ℕ ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
23 18 22 sylib ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ ℕ ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
24 4 5 9 17 23 climsup ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → 𝐹 ⇝ sup ( ran 𝐹 , ℝ , < ) )
25 nnex ⊢ ℕ ∈ V
26 fex ⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ℕ ∈ V ) → 𝐹 ∈ V )
27 1 25 26 sylancl ⊢ ( 𝜑 → 𝐹 ∈ V )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ sup ( ran 𝐹 , ℝ , < ) ) → 𝐹 ∈ V )
29 ltso ⊢ < Or ℝ
30 29 supex ⊢ sup ( ran 𝐹 , ℝ , < ) ∈ V
31 30 a1i ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ sup ( ran 𝐹 , ℝ , < ) ) → sup ( ran 𝐹 , ℝ , < ) ∈ V )
32 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ sup ( ran 𝐹 , ℝ , < ) ) → 𝐹 ⇝ sup ( ran 𝐹 , ℝ , < ) )
33 breldmg ⊢ ( ( 𝐹 ∈ V ∧ sup ( ran 𝐹 , ℝ , < ) ∈ V ∧ 𝐹 ⇝ sup ( ran 𝐹 , ℝ , < ) ) → 𝐹 ∈ dom ⇝ )
34 28 31 32 33 syl3anc ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ sup ( ran 𝐹 , ℝ , < ) ) → 𝐹 ∈ dom ⇝ )
35 24 34 syldan ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → 𝐹 ∈ dom ⇝ )
36 3 35 mtand ⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
37 ralnex ⊢ ( ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
38 36 37 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
39 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → 𝑥 ∈ ℝ )
40 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐹 : ℕ ⟶ ℝ )
41 40 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
42 39 41 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑥 < ( 𝐹 ‘ 𝑗 ) ↔ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
43 42 rexbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑗 ∈ ℕ 𝑥 < ( 𝐹 ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ℕ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
44 rexnal ⊢ ( ∃ 𝑗 ∈ ℕ ¬ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ¬ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
45 43 44 bitrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑗 ∈ ℕ 𝑥 < ( 𝐹 ‘ 𝑗 ) ↔ ¬ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
46 45 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ ℕ 𝑥 < ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑗 ∈ ℕ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
47 38 46 mpbird ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ ℕ 𝑥 < ( 𝐹 ‘ 𝑗 ) )
48 47 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑗 ∈ ℕ 𝑥 < ( 𝐹 ‘ 𝑗 ) )
49 39 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑥 ∈ ℝ )
50 41 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
51 40 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝐹 : ℕ ⟶ ℝ )
52 uznnssnn ⊢ ( 𝑗 ∈ ℕ → ( ℤ≥ ‘ 𝑗 ) ⊆ ℕ )
53 52 ad3antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ℤ≥ ‘ 𝑗 ) ⊆ ℕ )
54 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) )
55 53 54 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ ℕ )
56 51 55 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
57 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑥 < ( 𝐹 ‘ 𝑗 ) )
58 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝜑 )
59 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑗 ∈ ℕ )
60 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) )
61 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑙 ∈ ( 𝑗 ... 𝑘 ) ) → 𝐹 : ℕ ⟶ ℝ )
62 fzssnn ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 ... 𝑘 ) ⊆ ℕ )
63 62 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑙 ∈ ( 𝑗 ... 𝑘 ) ) → ( 𝑗 ... 𝑘 ) ⊆ ℕ )
64 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑙 ∈ ( 𝑗 ... 𝑘 ) ) → 𝑙 ∈ ( 𝑗 ... 𝑘 ) )
65 63 64 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑙 ∈ ( 𝑗 ... 𝑘 ) ) → 𝑙 ∈ ℕ )
66 61 65 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑙 ∈ ( 𝑗 ... 𝑘 ) ) → ( 𝐹 ‘ 𝑙 ) ∈ ℝ )
67 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑙 ∈ ( 𝑗 ... ( 𝑘 − 1 ) ) ) → 𝜑 )
68 fzssnn ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 ... ( 𝑘 − 1 ) ) ⊆ ℕ )
69 68 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑙 ∈ ( 𝑗 ... ( 𝑘 − 1 ) ) ) → ( 𝑗 ... ( 𝑘 − 1 ) ) ⊆ ℕ )
70 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑙 ∈ ( 𝑗 ... ( 𝑘 − 1 ) ) ) → 𝑙 ∈ ( 𝑗 ... ( 𝑘 − 1 ) ) )
71 69 70 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑙 ∈ ( 𝑗 ... ( 𝑘 − 1 ) ) ) → 𝑙 ∈ ℕ )
72 67 71 16 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑙 ∈ ( 𝑗 ... ( 𝑘 − 1 ) ) ) → ( 𝐹 ‘ 𝑙 ) ≤ ( 𝐹 ‘ ( 𝑙 + 1 ) ) )
73 60 66 72 monoord ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ ( 𝐹 ‘ 𝑘 ) )
74 58 59 54 73 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ≤ ( 𝐹 ‘ 𝑘 ) )
75 49 50 56 57 74 ltletrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑥 < ( 𝐹 ‘ 𝑘 ) )
76 75 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) )
77 76 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑥 < ( 𝐹 ‘ 𝑗 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) ) )
78 77 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑗 ∈ ℕ 𝑥 < ( 𝐹 ‘ 𝑗 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) ) )
79 48 78 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) )
80 79 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) )