Theorem subhalfhalf

Description: Subtracting the half of a number from the number yields the half of the number. (Contributed by AV, 28-Jun-2021)

	Ref	Expression
Assertion	subhalfhalf	$$⊢A\in ℂ\to A-\left(\frac{A}{2}\right)=\frac{A}{2}$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A\in ℂ\to A\in ℂ$$
2		2cnd	$$⊢A\in ℂ\to 2\in ℂ$$
3		2ne0	$$⊢2\ne 0$$
4	3	a1i	$$⊢A\in ℂ\to 2\ne 0$$
5	1 2 4	divcan1d	$$⊢A\in ℂ\to \left(\frac{A}{2}\right)\cdot 2=A$$
6	5	eqcomd	$$⊢A\in ℂ\to A=\left(\frac{A}{2}\right)\cdot 2$$
7	6	oveq1d	$$⊢A\in ℂ\to A-\left(\frac{A}{2}\right)=\left(\frac{A}{2}\right)\cdot 2-\left(\frac{A}{2}\right)$$
8		halfcl	$$⊢A\in ℂ\to \frac{A}{2}\in ℂ$$
9	8 2	mulcomd	$$⊢A\in ℂ\to \left(\frac{A}{2}\right)\cdot 2=2\left(\frac{A}{2}\right)$$
10	9	oveq1d	$$⊢A\in ℂ\to \left(\frac{A}{2}\right)\cdot 2-\left(\frac{A}{2}\right)=2\left(\frac{A}{2}\right)-\left(\frac{A}{2}\right)$$
11	2 8	mulsubfacd	$$⊢A\in ℂ\to 2\left(\frac{A}{2}\right)-\left(\frac{A}{2}\right)=\left(2-1\right)\left(\frac{A}{2}\right)$$
12		2m1e1	$$⊢2-1=1$$
13	12	a1i	$$⊢A\in ℂ\to 2-1=1$$
14	13	oveq1d	$$⊢A\in ℂ\to \left(2-1\right)\left(\frac{A}{2}\right)=1\left(\frac{A}{2}\right)$$
15	8	mulid2d	$$⊢A\in ℂ\to 1\left(\frac{A}{2}\right)=\frac{A}{2}$$
16	11 14 15	3eqtrd	$$⊢A\in ℂ\to 2\left(\frac{A}{2}\right)-\left(\frac{A}{2}\right)=\frac{A}{2}$$
17	7 10 16	3eqtrd	$$⊢A\in ℂ\to A-\left(\frac{A}{2}\right)=\frac{A}{2}$$