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\in ℂ$$
2		4cn	$$⊢4\in ℂ$$
3		ax-1cn	$$⊢1\in ℂ$$
4		4p1e5	$$⊢4+1=5$$
5	1 2 3 4	subaddrii	$$⊢5-4=1$$