Theorem 1mhlfehlf

Description: Prove that 1 - 1/2 = 1/2. (Contributed by David A. Wheeler, 4-Jan-2017)

	Ref	Expression
Assertion	1mhlfehlf	$$⊢1-\left(\frac{1}{2}\right)=\frac{1}{2}$$

Proof

Step	Hyp	Ref	Expression
1		2cn	$$⊢2\in ℂ$$
2		ax-1cn	$$⊢1\in ℂ$$
3		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
4		divsubdir	$$⊢\left(2\in ℂ\wedge 1\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{2-1}{2}=\left(\frac{2}{2}\right)-\left(\frac{1}{2}\right)$$
5	1 2 3 4	mp3an	$$⊢\frac{2-1}{2}=\left(\frac{2}{2}\right)-\left(\frac{1}{2}\right)$$
6		2m1e1	$$⊢2-1=1$$
7	6	oveq1i	$$⊢\frac{2-1}{2}=\frac{1}{2}$$
8		2div2e1	$$⊢\frac{2}{2}=1$$
9	8	oveq1i	$$⊢\left(\frac{2}{2}\right)-\left(\frac{1}{2}\right)=1-\left(\frac{1}{2}\right)$$
10	5 7 9	3eqtr3ri	$$⊢1-\left(\frac{1}{2}\right)=\frac{1}{2}$$