Description: An extended real that is not +oo is less than +oo . (Contributed by Glauco Siliprandi, 11-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nepnfltpnf.1 | ⊢ ( 𝜑 → 𝐴 ≠ +∞ ) | |
nepnfltpnf.2 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ* ) | ||
Assertion | nepnfltpnf | ⊢ ( 𝜑 → 𝐴 < +∞ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nepnfltpnf.1 | ⊢ ( 𝜑 → 𝐴 ≠ +∞ ) | |
2 | nepnfltpnf.2 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ* ) | |
3 | 1 | neneqd | ⊢ ( 𝜑 → ¬ 𝐴 = +∞ ) |
4 | nltpnft | ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 = +∞ ↔ ¬ 𝐴 < +∞ ) ) | |
5 | 2 4 | syl | ⊢ ( 𝜑 → ( 𝐴 = +∞ ↔ ¬ 𝐴 < +∞ ) ) |
6 | 3 5 | mtbid | ⊢ ( 𝜑 → ¬ ¬ 𝐴 < +∞ ) |
7 | notnotb | ⊢ ( 𝐴 < +∞ ↔ ¬ ¬ 𝐴 < +∞ ) | |
8 | 6 7 | sylibr | ⊢ ( 𝜑 → 𝐴 < +∞ ) |