Theorem 2m1e1OLD

Description: Obsolete version of 2m1e1 as of 10-Jun-2026. (Contributed by David A. Wheeler, 4-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	2m1e1OLD	⊢ ( 2 − 1 ) = 1

Proof

Step	Hyp	Ref	Expression
1		2cn	⊢ 2 ∈ ℂ
2		ax-1cn	⊢ 1 ∈ ℂ
3		1p1e2	⊢ ( 1 + 1 ) = 2
4	1 2 2 3	subaddrii	⊢ ( 2 − 1 ) = 1