Metamath Proof Explorer

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