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

Metamath Proof Explorer

Theorem mulcxp

Description: Complex exponentiation of a product. Proposition 10-4.2(c) of Gleason p. 135. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion mulcxp ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 simp1l ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℝ )
2 1 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
3 2 mul01d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 0 ) = 0 )
4 3 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 0 ) ↑𝑐 𝐶 ) = ( 0 ↑𝑐 𝐶 ) )
5 simp3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
6 2 5 mulcxplem ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( 0 ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 0 ↑𝑐 𝐶 ) ) )
7 4 6 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 0 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 0 ↑𝑐 𝐶 ) ) )
8 oveq2 ⊢ ( 𝐵 = 0 → ( 𝐴 · 𝐵 ) = ( 𝐴 · 0 ) )
9 8 oveq1d ⊢ ( 𝐵 = 0 → ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 · 0 ) ↑𝑐 𝐶 ) )
10 oveq1 ⊢ ( 𝐵 = 0 → ( 𝐵 ↑𝑐 𝐶 ) = ( 0 ↑𝑐 𝐶 ) )
11 10 oveq2d ⊢ ( 𝐵 = 0 → ( ( 𝐴 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 0 ↑𝑐 𝐶 ) ) )
12 9 11 eqeq12d ⊢ ( 𝐵 = 0 → ( ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) ↔ ( ( 𝐴 · 0 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 0 ↑𝑐 𝐶 ) ) ) )
13 7 12 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( 𝐵 = 0 → ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) ) )
14 simp2l ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℝ )
15 14 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
16 15 mul02d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( 0 · 𝐵 ) = 0 )
17 16 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( ( 0 · 𝐵 ) ↑𝑐 𝐶 ) = ( 0 ↑𝑐 𝐶 ) )
18 15 5 mulcxplem ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( 0 ↑𝑐 𝐶 ) = ( ( 𝐵 ↑𝑐 𝐶 ) · ( 0 ↑𝑐 𝐶 ) ) )
19 cxpcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ↑𝑐 𝐶 ) ∈ ℂ )
20 15 5 19 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ↑𝑐 𝐶 ) ∈ ℂ )
21 0cn ⊢ 0 ∈ ℂ
22 cxpcl ⊢ ( ( 0 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 0 ↑𝑐 𝐶 ) ∈ ℂ )
23 21 5 22 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( 0 ↑𝑐 𝐶 ) ∈ ℂ )
24 20 23 mulcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 ↑𝑐 𝐶 ) · ( 0 ↑𝑐 𝐶 ) ) = ( ( 0 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) )
25 18 24 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( 0 ↑𝑐 𝐶 ) = ( ( 0 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) )
26 17 25 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( ( 0 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 0 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) )
27 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 · 𝐵 ) = ( 0 · 𝐵 ) )
28 27 oveq1d ⊢ ( 𝐴 = 0 → ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 0 · 𝐵 ) ↑𝑐 𝐶 ) )
29 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 ↑𝑐 𝐶 ) = ( 0 ↑𝑐 𝐶 ) )
30 29 oveq1d ⊢ ( 𝐴 = 0 → ( ( 𝐴 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) = ( ( 0 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) )
31 28 30 eqeq12d ⊢ ( 𝐴 = 0 → ( ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) ↔ ( ( 0 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 0 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) ) )
32 26 31 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( 𝐴 = 0 → ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) ) )
33 32 a1dd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( 𝐴 = 0 → ( 𝐵 ≠ 0 → ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) ) ) )
34 1 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℝ )
35 simpl1r ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 0 ≤ 𝐴 )
36 simprl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐴 ≠ 0 )
37 34 35 36 ne0gt0d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 0 < 𝐴 )
38 34 37 elrpd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℝ+ )
39 14 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℝ )
40 simpl2r ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 0 ≤ 𝐵 )
41 simprr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ≠ 0 )
42 39 40 41 ne0gt0d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 0 < 𝐵 )
43 39 42 elrpd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℝ+ )
44 38 43 relogmuld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( log ‘ ( 𝐴 · 𝐵 ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) )
45 44 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐶 · ( log ‘ ( 𝐴 · 𝐵 ) ) ) = ( 𝐶 · ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) ) )
46 5 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐶 ∈ ℂ )
47 2 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℂ )
48 47 36 logcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( log ‘ 𝐴 ) ∈ ℂ )
49 15 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℂ )
50 49 41 logcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( log ‘ 𝐵 ) ∈ ℂ )
51 46 48 50 adddid ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐶 · ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) ) = ( ( 𝐶 · ( log ‘ 𝐴 ) ) + ( 𝐶 · ( log ‘ 𝐵 ) ) ) )
52 45 51 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐶 · ( log ‘ ( 𝐴 · 𝐵 ) ) ) = ( ( 𝐶 · ( log ‘ 𝐴 ) ) + ( 𝐶 · ( log ‘ 𝐵 ) ) ) )
53 52 fveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( exp ‘ ( 𝐶 · ( log ‘ ( 𝐴 · 𝐵 ) ) ) ) = ( exp ‘ ( ( 𝐶 · ( log ‘ 𝐴 ) ) + ( 𝐶 · ( log ‘ 𝐵 ) ) ) ) )
54 46 48 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐶 · ( log ‘ 𝐴 ) ) ∈ ℂ )
55 46 50 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐶 · ( log ‘ 𝐵 ) ) ∈ ℂ )
56 efadd ⊢ ( ( ( 𝐶 · ( log ‘ 𝐴 ) ) ∈ ℂ ∧ ( 𝐶 · ( log ‘ 𝐵 ) ) ∈ ℂ ) → ( exp ‘ ( ( 𝐶 · ( log ‘ 𝐴 ) ) + ( 𝐶 · ( log ‘ 𝐵 ) ) ) ) = ( ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) · ( exp ‘ ( 𝐶 · ( log ‘ 𝐵 ) ) ) ) )
57 54 55 56 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( exp ‘ ( ( 𝐶 · ( log ‘ 𝐴 ) ) + ( 𝐶 · ( log ‘ 𝐵 ) ) ) ) = ( ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) · ( exp ‘ ( 𝐶 · ( log ‘ 𝐵 ) ) ) ) )
58 53 57 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( exp ‘ ( 𝐶 · ( log ‘ ( 𝐴 · 𝐵 ) ) ) ) = ( ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) · ( exp ‘ ( 𝐶 · ( log ‘ 𝐵 ) ) ) ) )
59 47 49 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
60 47 49 36 41 mulne0d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 · 𝐵 ) ≠ 0 )
61 cxpef ⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℂ ∧ ( 𝐴 · 𝐵 ) ≠ 0 ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ ( 𝐴 · 𝐵 ) ) ) ) )
62 59 60 46 61 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ ( 𝐴 · 𝐵 ) ) ) ) )
63 cxpef ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) )
64 47 36 46 63 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) )
65 cxpef ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ 𝐵 ) ) ) )
66 49 41 46 65 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( 𝐵 ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ 𝐵 ) ) ) )
67 64 66 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) = ( ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) · ( exp ‘ ( 𝐶 · ( log ‘ 𝐵 ) ) ) ) )
68 58 62 67 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) )
69 68 exp32 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ≠ 0 → ( 𝐵 ≠ 0 → ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) ) ) )
70 33 69 pm2.61dne ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ≠ 0 → ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) ) )
71 13 70 pm2.61dne ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) )