Metamath Proof Explorer


Theorem pltle

Description: "Less than" implies "less than or equal to". ( pssss analog.) (Contributed by NM, 4-Dec-2011)

Ref Expression
Hypotheses pltval.l = ( le ‘ 𝐾 )
pltval.s < = ( lt ‘ 𝐾 )
Assertion pltle ( ( 𝐾𝐴𝑋𝐵𝑌𝐶 ) → ( 𝑋 < 𝑌𝑋 𝑌 ) )

Proof

Step Hyp Ref Expression
1 pltval.l = ( le ‘ 𝐾 )
2 pltval.s < = ( lt ‘ 𝐾 )
3 1 2 pltval ( ( 𝐾𝐴𝑋𝐵𝑌𝐶 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 𝑌𝑋𝑌 ) ) )
4 3 simprbda ( ( ( 𝐾𝐴𝑋𝐵𝑌𝐶 ) ∧ 𝑋 < 𝑌 ) → 𝑋 𝑌 )
5 4 ex ( ( 𝐾𝐴𝑋𝐵𝑌𝐶 ) → ( 𝑋 < 𝑌𝑋 𝑌 ) )