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
2 4cn 4
3 ax-1cn 1
4 4p1e5 4 + 1 = 5
5 1 2 3 4 subaddrii 5 4 = 1