Metamath Proof Explorer


Theorem 2m1e1

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)

Ref Expression
Assertion 2m1e1
|- ( 2 - 1 ) = 1

Proof

Step Hyp Ref Expression
1 2cn
 |-  2 e. CC
2 ax-1cn
 |-  1 e. CC
3 1p1e2
 |-  ( 1 + 1 ) = 2
4 1 2 2 3 subaddrii
 |-  ( 2 - 1 ) = 1