Theorem logsqrt

Description: Logarithm of a square root. (Contributed by Mario Carneiro, 5-May-2016)

	Ref	Expression
Assertion	logsqrt	$$⊢A\in {ℝ}^{+}\to \log \sqrt{A}=\frac{\log A}{2}$$

Proof

Step	Hyp	Ref	Expression
1		relogcl	$$⊢A\in {ℝ}^{+}\to \log A\in ℝ$$
2	1	recnd	$$⊢A\in {ℝ}^{+}\to \log A\in ℂ$$
3		2cn	$$⊢2\in ℂ$$
4		2ne0	$$⊢2\ne 0$$
5		divrec2	$$⊢\left(\log A\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to \frac{\log A}{2}=\left(\frac{1}{2}\right)\log A$$
6	3 4 5	mp3an23	$$⊢\log A\in ℂ\to \frac{\log A}{2}=\left(\frac{1}{2}\right)\log A$$
7	2 6	syl	$$⊢A\in {ℝ}^{+}\to \frac{\log A}{2}=\left(\frac{1}{2}\right)\log A$$
8		halfre	$$⊢\frac{1}{2}\in ℝ$$
9		logcxp	$$⊢\left(A\in {ℝ}^{+}\wedge \frac{1}{2}\in ℝ\right)\to \log A^{\frac{1}{2}}=\left(\frac{1}{2}\right)\log A$$
10	8 9	mpan2	$$⊢A\in {ℝ}^{+}\to \log A^{\frac{1}{2}}=\left(\frac{1}{2}\right)\log A$$
11		rpcn	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
12		cxpsqrt	$$⊢A\in ℂ\to A^{\frac{1}{2}}=\sqrt{A}$$
13	11 12	syl	$$⊢A\in {ℝ}^{+}\to A^{\frac{1}{2}}=\sqrt{A}$$
14	13	fveq2d	$$⊢A\in {ℝ}^{+}\to \log A^{\frac{1}{2}}=\log \sqrt{A}$$
15	7 10 14	3eqtr2rd	$$⊢A\in {ℝ}^{+}\to \log \sqrt{A}=\frac{\log A}{2}$$