This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )