Metamath Proof Explorer


Theorem lenlteq

Description: 'less than or equal to' but not 'less than' implies 'equal' . (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses lenlteq.1 ( 𝜑𝐴 ∈ ℝ )
lenlteq.2 ( 𝜑𝐵 ∈ ℝ )
lenlteq.3 ( 𝜑𝐴𝐵 )
lenlteq.4 ( 𝜑 → ¬ 𝐴 < 𝐵 )
Assertion lenlteq ( 𝜑𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 lenlteq.1 ( 𝜑𝐴 ∈ ℝ )
2 lenlteq.2 ( 𝜑𝐵 ∈ ℝ )
3 lenlteq.3 ( 𝜑𝐴𝐵 )
4 lenlteq.4 ( 𝜑 → ¬ 𝐴 < 𝐵 )
5 3 4 jca ( 𝜑 → ( 𝐴𝐵 ∧ ¬ 𝐴 < 𝐵 ) )
6 eqlelt ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 = 𝐵 ↔ ( 𝐴𝐵 ∧ ¬ 𝐴 < 𝐵 ) ) )
7 1 2 6 syl2anc ( 𝜑 → ( 𝐴 = 𝐵 ↔ ( 𝐴𝐵 ∧ ¬ 𝐴 < 𝐵 ) ) )
8 5 7 mpbird ( 𝜑𝐴 = 𝐵 )