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 | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) |
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 | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) |