Metamath Proof Explorer


Theorem 2m1e1OLD

Description: Obsolete version of 2m1e1 as of 10-Jun-2026. (Contributed by David A. Wheeler, 4-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 2m1e1OLD ⊢ 2 − 1 = 1

Proof

Step Hyp Ref Expression
1 2cn ⊢ 2 ∈ ℂ
2 ax-1cn ⊢ 1 ∈ ℂ
3 1p1e2 ⊢ 1 + 1 = 2
4 1 2 2 3 subaddrii ⊢ 2 − 1 = 1