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-\left(\frac{1}{2}\right)=\frac{1}{2}$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		halfcn	$$⊢\frac{1}{2}\in ℂ$$
3		2halves	$$⊢1\in ℂ\to \left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
4	1 3	ax-mp	$$⊢\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
5	1 2 2 4	subaddrii	$$⊢1-\left(\frac{1}{2}\right)=\frac{1}{2}$$