Metamath Proof Explorer

Theorem cxpcom

Description: Commutative law for real exponentiation. (Contributed by AV, 29-Dec-2022)

Ref Expression
Assertion cxpcom 
|- ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> ( ( A ^c B ) ^c C ) = ( ( A ^c C ) ^c B ) )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( B e. RR -> B e. CC )
2 recn 
 |-  ( C e. RR -> C e. CC )
3 mulcom 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
4 1 2 3 syl2an 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B x. C ) = ( C x. B ) )
5 4 3adant1 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> ( B x. C ) = ( C x. B ) )
6 5 oveq2d 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> ( A ^c ( B x. C ) ) = ( A ^c ( C x. B ) ) )
7 cxpmul 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^c C ) )
8 2 7 syl3an3 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^c C ) )
9 simp1 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> A e. RR+ )
10 simp3 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> C e. RR )
11 1 3ad2ant2 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> B e. CC )
12 9 10 11 cxpmuld 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> ( A ^c ( C x. B ) ) = ( ( A ^c C ) ^c B ) )
13 6 8 12 3eqtr3d 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> ( ( A ^c B ) ^c C ) = ( ( A ^c C ) ^c B ) )