Theorem 2halves

Description: Two halves make a whole. (Contributed by NM, 11-Apr-2005)

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

Proof

Step	Hyp	Ref	Expression
1		2times	$$⊢A\in ℂ\to 2A=A+A$$
2	1	oveq1d	$$⊢A\in ℂ\to \frac{2A}{2}=\frac{A+A}{2}$$
3		2cn	$$⊢2\in ℂ$$
4		2ne0	$$⊢2\ne 0$$
5		divcan3	$$⊢\left(A\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to \frac{2A}{2}=A$$
6	3 4 5	mp3an23	$$⊢A\in ℂ\to \frac{2A}{2}=A$$
7		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
8		divdir	$$⊢\left(A\in ℂ\wedge A\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{A+A}{2}=\left(\frac{A}{2}\right)+\left(\frac{A}{2}\right)$$
9	7 8	mp3an3	$$⊢\left(A\in ℂ\wedge A\in ℂ\right)\to \frac{A+A}{2}=\left(\frac{A}{2}\right)+\left(\frac{A}{2}\right)$$
10	9	anidms	$$⊢A\in ℂ\to \frac{A+A}{2}=\left(\frac{A}{2}\right)+\left(\frac{A}{2}\right)$$
11	2 6 10	3eqtr3rd	$$⊢A\in ℂ\to \left(\frac{A}{2}\right)+\left(\frac{A}{2}\right)=A$$