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