Description: An extended real that is not minus infinity, is larger than minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | nemnftgtmnft | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → -∞ < 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → 𝐴 ≠ -∞ ) | |
2 | 1 | neneqd | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → ¬ 𝐴 = -∞ ) |
3 | ngtmnft | ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 = -∞ ↔ ¬ -∞ < 𝐴 ) ) | |
4 | 3 | adantr | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → ( 𝐴 = -∞ ↔ ¬ -∞ < 𝐴 ) ) |
5 | 2 4 | mtbid | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → ¬ ¬ -∞ < 𝐴 ) |
6 | notnotb | ⊢ ( -∞ < 𝐴 ↔ ¬ ¬ -∞ < 𝐴 ) | |
7 | 5 6 | sylibr | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → -∞ < 𝐴 ) |