Description: 2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 . (Contributed by David A. Wheeler, 4-Jan-2017) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 2m1e1 | ⊢ ( 2 − 1 ) = 1 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-1cn | ⊢ 1 ∈ ℂ | |
| 2 | df-2 | ⊢ 2 = ( 1 + 1 ) | |
| 3 | 1 1 2 | mvrladdi | ⊢ ( 2 − 1 ) = 1 |