Theorem logsqrt

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

	Ref	Expression
Assertion	logsqrt	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ ( √ ‘ 𝐴 ) ) = ( ( log ‘ 𝐴 ) / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		relogcl	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
2	1	recnd	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℂ )
3		2cn	⊢ 2 ∈ ℂ
4		2ne0	⊢ 2 ≠ 0
5		divrec2	⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( log ‘ 𝐴 ) / 2 ) = ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) )
6	3 4 5	mp3an23	⊢ ( ( log ‘ 𝐴 ) ∈ ℂ → ( ( log ‘ 𝐴 ) / 2 ) = ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) )
7	2 6	syl	⊢ ( 𝐴 ∈ ℝ+ → ( ( log ‘ 𝐴 ) / 2 ) = ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) )
8		halfre	⊢ ( 1 / 2 ) ∈ ℝ
9		logcxp	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( 1 / 2 ) ∈ ℝ ) → ( log ‘ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) ) = ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) )
10	8 9	mpan2	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) ) = ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) )
11		rpcn	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
12		cxpsqrt	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝐴 ) )
13	11 12	syl	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝐴 ) )
14	13	fveq2d	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) ) = ( log ‘ ( √ ‘ 𝐴 ) ) )
15	7 10 14	3eqtr2rd	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ ( √ ‘ 𝐴 ) ) = ( ( log ‘ 𝐴 ) / 2 ) )