2halves

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

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

Metamath Proof Explorer