Metamath Proof Explorer


Theorem cxpmuld

Description: Product of exponents law for complex exponentiation. Proposition 10-4.2(b) of Gleason p. 135. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypotheses rpcxpcld.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„+ )
rpcxpcld.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
cxpmuld.4 โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„‚ )
Assertion cxpmuld ( ๐œ‘ โ†’ ( ๐ด โ†‘๐‘ ( ๐ต ยท ๐ถ ) ) = ( ( ๐ด โ†‘๐‘ ๐ต ) โ†‘๐‘ ๐ถ ) )

Proof

Step Hyp Ref Expression
1 rpcxpcld.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„+ )
2 rpcxpcld.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
3 cxpmuld.4 โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„‚ )
4 cxpmul โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ๐ด โ†‘๐‘ ( ๐ต ยท ๐ถ ) ) = ( ( ๐ด โ†‘๐‘ ๐ต ) โ†‘๐‘ ๐ถ ) )
5 1 2 3 4 syl3anc โŠข ( ๐œ‘ โ†’ ( ๐ด โ†‘๐‘ ( ๐ต ยท ๐ถ ) ) = ( ( ๐ด โ†‘๐‘ ๐ต ) โ†‘๐‘ ๐ถ ) )