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