Metamath Proof Explorer

Theorem 5m4e1

Description: Prove that 5 - 4 = 1. (Contributed by David A. Wheeler, 31-Jan-2017)

Ref Expression
Assertion 5m4e1 
|- ( 5 - 4 ) = 1

Proof

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