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) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)

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

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	|- 1 e. CC
2		df-2	|- 2 = ( 1 + 1 )
3	1 1 2	mvrladdi	|- ( 2 - 1 ) = 1