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

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 / ( 𝐴 ↑𝑐 𝐵 ) ) )