Theorem lmdvglim

Description: If a monotonic real number sequence F diverges, it converges in the extended real numbers and its limit is plus infinity. (Contributed by Thierry Arnoux, 3-Aug-2017)

	Ref	Expression
Hypotheses	lmdvglim.j	⊢ 𝐽 = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
	lmdvglim.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) )
	lmdvglim.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
	lmdvglim.3	⊢ ( 𝜑 → ¬ 𝐹 ∈ dom ⇝ )
Assertion	lmdvglim	⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) +∞ )

Proof

Step	Hyp	Ref	Expression
1		lmdvglim.j	⊢ 𝐽 = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
2		lmdvglim.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) )
3		lmdvglim.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
4		lmdvglim.3	⊢ ( 𝜑 → ¬ 𝐹 ∈ dom ⇝ )
5	2 3 4	lmdvg	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) )
6		icossicc	⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
7		fss	⊢ ( ( 𝐹 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) )
8	2 6 7	sylancl	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( 0 [,] +∞ ) )
9		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
10	1 8 9	lmxrge0	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) ) )
11	5 10	mpbird	⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) +∞ )