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 ≤ 𝐵 ) ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 𝐵 ↑𝑐 𝐶 ) ) )