Description: An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | xgepnf | ⊢ ( 𝐴 ∈ ℝ* → ( +∞ ≤ 𝐴 ↔ 𝐴 = +∞ ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pnfxr | ⊢ +∞ ∈ ℝ* | |
2 | xrlenlt | ⊢ ( ( +∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( +∞ ≤ 𝐴 ↔ ¬ 𝐴 < +∞ ) ) | |
3 | 1 2 | mpan | ⊢ ( 𝐴 ∈ ℝ* → ( +∞ ≤ 𝐴 ↔ ¬ 𝐴 < +∞ ) ) |
4 | nltpnft | ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 = +∞ ↔ ¬ 𝐴 < +∞ ) ) | |
5 | 3 4 | bitr4d | ⊢ ( 𝐴 ∈ ℝ* → ( +∞ ≤ 𝐴 ↔ 𝐴 = +∞ ) ) |