Metamath Proof Explorer

Theorem logsqrt

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

Ref Expression
Assertion logsqrt 
|- ( A e. RR+ -> ( log ` ( sqrt ` A ) ) = ( ( log ` A ) / 2 ) )

Proof

Step Hyp Ref Expression
1 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
2 1 recnd 
 |-  ( A e. RR+ -> ( log ` A ) e. CC )
3 2cn 
 |-  2 e. CC
4 2ne0 
 |-  2 =/= 0
5 divrec2 
 |-  ( ( ( log ` A ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( log ` A ) / 2 ) = ( ( 1 / 2 ) x. ( log ` A ) ) )
6 3 4 5 mp3an23 
 |-  ( ( log ` A ) e. CC -> ( ( log ` A ) / 2 ) = ( ( 1 / 2 ) x. ( log ` A ) ) )
7 2 6 syl 
 |-  ( A e. RR+ -> ( ( log ` A ) / 2 ) = ( ( 1 / 2 ) x. ( log ` A ) ) )
8 halfre 
 |-  ( 1 / 2 ) e. RR
9 logcxp 
 |-  ( ( A e. RR+ /\ ( 1 / 2 ) e. RR ) -> ( log ` ( A ^c ( 1 / 2 ) ) ) = ( ( 1 / 2 ) x. ( log ` A ) ) )
10 8 9 mpan2 
 |-  ( A e. RR+ -> ( log ` ( A ^c ( 1 / 2 ) ) ) = ( ( 1 / 2 ) x. ( log ` A ) ) )
11 rpcn 
 |-  ( A e. RR+ -> A e. CC )
12 cxpsqrt 
 |-  ( A e. CC -> ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) )
13 11 12 syl 
 |-  ( A e. RR+ -> ( A ^c ( 1 / 2 ) ) = ( sqrt ` A ) )
14 13 fveq2d 
 |-  ( A e. RR+ -> ( log ` ( A ^c ( 1 / 2 ) ) ) = ( log ` ( sqrt ` A ) ) )
15 7 10 14 3eqtr2rd 
 |-  ( A e. RR+ -> ( log ` ( sqrt ` A ) ) = ( ( log ` A ) / 2 ) )