Description: 'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lt.1 | ⊢ 𝐴 ∈ ℝ | |
lt.2 | ⊢ 𝐵 ∈ ℝ | ||
ltlei.1 | ⊢ 𝐴 < 𝐵 | ||
Assertion | ltleii | ⊢ 𝐴 ≤ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lt.1 | ⊢ 𝐴 ∈ ℝ | |
2 | lt.2 | ⊢ 𝐵 ∈ ℝ | |
3 | ltlei.1 | ⊢ 𝐴 < 𝐵 | |
4 | 1 2 | ltlei | ⊢ ( 𝐴 < 𝐵 → 𝐴 ≤ 𝐵 ) |
5 | 3 4 | ax-mp | ⊢ 𝐴 ≤ 𝐵 |