Metamath Proof Explorer


Theorem cxprec

Description: Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxprec ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) = ( 1 / ( 𝐴𝑐 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 rpcn ( 𝐴 ∈ ℝ+𝐴 ∈ ℂ )
2 cxpcl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝑐 𝐵 ) ∈ ℂ )
3 1 2 sylan ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → ( 𝐴𝑐 𝐵 ) ∈ ℂ )
4 rpreccl ( 𝐴 ∈ ℝ+ → ( 1 / 𝐴 ) ∈ ℝ+ )
5 4 rpcnd ( 𝐴 ∈ ℝ+ → ( 1 / 𝐴 ) ∈ ℂ )
6 cxpcl ( ( ( 1 / 𝐴 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) ∈ ℂ )
7 5 6 sylan ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) ∈ ℂ )
8 1 adantr ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
9 rpne0 ( 𝐴 ∈ ℝ+𝐴 ≠ 0 )
10 9 adantr ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → 𝐴 ≠ 0 )
11 simpr ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
12 cxpne0 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴𝑐 𝐵 ) ≠ 0 )
13 8 10 11 12 syl3anc ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → ( 𝐴𝑐 𝐵 ) ≠ 0 )
14 8 10 recidd ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → ( 𝐴 · ( 1 / 𝐴 ) ) = 1 )
15 14 oveq1d ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → ( ( 𝐴 · ( 1 / 𝐴 ) ) ↑𝑐 𝐵 ) = ( 1 ↑𝑐 𝐵 ) )
16 rprege0 ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
17 16 adantr ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
18 4 rprege0d ( 𝐴 ∈ ℝ+ → ( ( 1 / 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝐴 ) ) )
19 18 adantr ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → ( ( 1 / 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝐴 ) ) )
20 mulcxp ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( ( 1 / 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝐴 ) ) ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · ( 1 / 𝐴 ) ) ↑𝑐 𝐵 ) = ( ( 𝐴𝑐 𝐵 ) · ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) ) )
21 17 19 11 20 syl3anc ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → ( ( 𝐴 · ( 1 / 𝐴 ) ) ↑𝑐 𝐵 ) = ( ( 𝐴𝑐 𝐵 ) · ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) ) )
22 1cxp ( 𝐵 ∈ ℂ → ( 1 ↑𝑐 𝐵 ) = 1 )
23 11 22 syl ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → ( 1 ↑𝑐 𝐵 ) = 1 )
24 15 21 23 3eqtr3d ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → ( ( 𝐴𝑐 𝐵 ) · ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) ) = 1 )
25 3 7 13 24 mvllmuld ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℂ ) → ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) = ( 1 / ( 𝐴𝑐 𝐵 ) ) )