This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

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