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

Metamath Proof Explorer

Theorem abscxp

Description: Absolute value of a power, when the base is real. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion abscxp 
|- ( ( A e. RR+ /\ B e. CC ) -> ( abs ` ( A ^c B ) ) = ( A ^c ( Re ` B ) ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A e. RR+ /\ B e. CC ) -> B e. CC )
2 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
3 2 recnd 
 |-  ( A e. RR+ -> ( log ` A ) e. CC )
4 3 adantr 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( log ` A ) e. CC )
5 1 4 mulcld 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( B x. ( log ` A ) ) e. CC )
6 absef 
 |-  ( ( B x. ( log ` A ) ) e. CC -> ( abs ` ( exp ` ( B x. ( log ` A ) ) ) ) = ( exp ` ( Re ` ( B x. ( log ` A ) ) ) ) )
7 5 6 syl 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( abs ` ( exp ` ( B x. ( log ` A ) ) ) ) = ( exp ` ( Re ` ( B x. ( log ` A ) ) ) ) )
8 remul2 
 |-  ( ( ( log ` A ) e. RR /\ B e. CC ) -> ( Re ` ( ( log ` A ) x. B ) ) = ( ( log ` A ) x. ( Re ` B ) ) )
9 2 8 sylan 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( Re ` ( ( log ` A ) x. B ) ) = ( ( log ` A ) x. ( Re ` B ) ) )
10 1 4 mulcomd 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( B x. ( log ` A ) ) = ( ( log ` A ) x. B ) )
11 10 fveq2d 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( Re ` ( B x. ( log ` A ) ) ) = ( Re ` ( ( log ` A ) x. B ) ) )
12 recl 
 |-  ( B e. CC -> ( Re ` B ) e. RR )
13 12 adantl 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( Re ` B ) e. RR )
14 13 recnd 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( Re ` B ) e. CC )
15 14 4 mulcomd 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( ( Re ` B ) x. ( log ` A ) ) = ( ( log ` A ) x. ( Re ` B ) ) )
16 9 11 15 3eqtr4d 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( Re ` ( B x. ( log ` A ) ) ) = ( ( Re ` B ) x. ( log ` A ) ) )
17 16 fveq2d 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( exp ` ( Re ` ( B x. ( log ` A ) ) ) ) = ( exp ` ( ( Re ` B ) x. ( log ` A ) ) ) )
18 7 17 eqtrd 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( abs ` ( exp ` ( B x. ( log ` A ) ) ) ) = ( exp ` ( ( Re ` B ) x. ( log ` A ) ) ) )
19 rpcn 
 |-  ( A e. RR+ -> A e. CC )
20 19 adantr 
 |-  ( ( A e. RR+ /\ B e. CC ) -> A e. CC )
21 rpne0 
 |-  ( A e. RR+ -> A =/= 0 )
22 21 adantr 
 |-  ( ( A e. RR+ /\ B e. CC ) -> A =/= 0 )
23 cxpef 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
24 20 22 1 23 syl3anc 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
25 24 fveq2d 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( abs ` ( A ^c B ) ) = ( abs ` ( exp ` ( B x. ( log ` A ) ) ) ) )
26 cxpef 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( Re ` B ) e. CC ) -> ( A ^c ( Re ` B ) ) = ( exp ` ( ( Re ` B ) x. ( log ` A ) ) ) )
27 20 22 14 26 syl3anc 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( A ^c ( Re ` B ) ) = ( exp ` ( ( Re ` B ) x. ( log ` A ) ) ) )
28 18 25 27 3eqtr4d 
 |-  ( ( A e. RR+ /\ B e. CC ) -> ( abs ` ( A ^c B ) ) = ( A ^c ( Re ` B ) ) )