Description: The extended real numbers are unbounded above. (Contributed by Mario Carneiro, 7-May-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | xrsup | ⊢ sup ( ℝ* , ℝ* , < ) = +∞ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid | ⊢ ℝ* ⊆ ℝ* | |
2 | pnfxr | ⊢ +∞ ∈ ℝ* | |
3 | supxrpnf | ⊢ ( ( ℝ* ⊆ ℝ* ∧ +∞ ∈ ℝ* ) → sup ( ℝ* , ℝ* , < ) = +∞ ) | |
4 | 1 2 3 | mp2an | ⊢ sup ( ℝ* , ℝ* , < ) = +∞ |