Theorem 1mhlfehlf

Description: Prove that 1 - 1/2 = 1/2. (Contributed by David A. Wheeler, 4-Jan-2017) (Proof shortened by SN, 22-Oct-2025)

	Ref	Expression
Assertion	1mhlfehlf	⊢ ( 1 − ( 1 / 2 ) ) = ( 1 / 2 )

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	⊢ 1 ∈ ℂ
2		halfcn	⊢ ( 1 / 2 ) ∈ ℂ
3		2halves	⊢ ( 1 ∈ ℂ → ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
4	1 3	ax-mp	⊢ ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
5	1 2 2 4	subaddrii	⊢ ( 1 − ( 1 / 2 ) ) = ( 1 / 2 )