Theorem divcxp

Description: Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Assertion	divcxp	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 / 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) / ( 𝐵 ↑𝑐 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1l	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℝ )
2		simp1r	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → 0 ≤ 𝐴 )
3		simp2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℝ+ )
4	3	rpreccld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( 1 / 𝐵 ) ∈ ℝ+ )
5	4	rpred	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( 1 / 𝐵 ) ∈ ℝ )
6	4	rpge0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → 0 ≤ ( 1 / 𝐵 ) )
7		simp3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
8		mulcxp	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( ( 1 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝐵 ) ) ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · ( 1 / 𝐵 ) ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( ( 1 / 𝐵 ) ↑𝑐 𝐶 ) ) )
9	1 2 5 6 7 8	syl221anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · ( 1 / 𝐵 ) ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( ( 1 / 𝐵 ) ↑𝑐 𝐶 ) ) )
10		cxprec	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( ( 1 / 𝐵 ) ↑𝑐 𝐶 ) = ( 1 / ( 𝐵 ↑𝑐 𝐶 ) ) )
11	3 7 10	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( ( 1 / 𝐵 ) ↑𝑐 𝐶 ) = ( 1 / ( 𝐵 ↑𝑐 𝐶 ) ) )
12	11	oveq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 ↑𝑐 𝐶 ) · ( ( 1 / 𝐵 ) ↑𝑐 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 1 / ( 𝐵 ↑𝑐 𝐶 ) ) ) )
13	9 12	eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · ( 1 / 𝐵 ) ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 1 / ( 𝐵 ↑𝑐 𝐶 ) ) ) )
14	1	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → 𝐴 ∈ ℂ )
15	3	rpcnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
16	3	rpne0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → 𝐵 ≠ 0 )
17	14 15 16	divrecd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
18	17	oveq1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 / 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 · ( 1 / 𝐵 ) ) ↑𝑐 𝐶 ) )
19		cxpcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℂ )
20	14 7 19	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℂ )
21		cxpcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ↑𝑐 𝐶 ) ∈ ℂ )
22	15 7 21	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ↑𝑐 𝐶 ) ∈ ℂ )
23		cxpne0	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ↑𝑐 𝐶 ) ≠ 0 )
24	15 16 7 23	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ↑𝑐 𝐶 ) ≠ 0 )
25	20 22 24	divrecd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 ↑𝑐 𝐶 ) / ( 𝐵 ↑𝑐 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐶 ) · ( 1 / ( 𝐵 ↑𝑐 𝐶 ) ) ) )
26	13 18 25	3eqtr4d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 / 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) / ( 𝐵 ↑𝑐 𝐶 ) ) )