cxprec

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

		Ref	Expression
	Assertion	cxprec	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to {(\frac{1}{A})}^{B} = \frac{1}{A^{B}}$

Proof

Step	Hyp	Ref	Expression
1		rpcn	$⊢ A \in ℝ^{+} \to A \in ℂ$
2		cxpcl	$⊢ (A \in ℂ \land B \in ℂ) \to A^{B} \in ℂ$
3	1 2	sylan	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to A^{B} \in ℂ$
4		rpreccl	$⊢ A \in ℝ^{+} \to \frac{1}{A} \in ℝ^{+}$
5	4	rpcnd	$⊢ A \in ℝ^{+} \to \frac{1}{A} \in ℂ$
6		cxpcl	$⊢ (\frac{1}{A} \in ℂ \land B \in ℂ) \to {(\frac{1}{A})}^{B} \in ℂ$
7	5 6	sylan	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to {(\frac{1}{A})}^{B} \in ℂ$
8	1	adantr	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to A \in ℂ$
9		rpne0	$⊢ A \in ℝ^{+} \to A \neq 0$
10	9	adantr	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to A \neq 0$
11		simpr	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to B \in ℂ$
12		cxpne0	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℂ) \to A^{B} \neq 0$
13	8 10 11 12	syl3anc	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to A^{B} \neq 0$
14	8 10	recidd	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to A (\frac{1}{A}) = 1$
15	14	oveq1d	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to {A (\frac{1}{A})}^{B} = 1^{B}$
16		rprege0	$⊢ A \in ℝ^{+} \to (A \in ℝ \land 0 \leq A)$
17	16	adantr	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to (A \in ℝ \land 0 \leq A)$
18	4	rprege0d	$⊢ A \in ℝ^{+} \to (\frac{1}{A} \in ℝ \land 0 \leq \frac{1}{A})$
19	18	adantr	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to (\frac{1}{A} \in ℝ \land 0 \leq \frac{1}{A})$
20		mulcxp	$⊢ ((A \in ℝ \land 0 \leq A) \land (\frac{1}{A} \in ℝ \land 0 \leq \frac{1}{A}) \land B \in ℂ) \to {A (\frac{1}{A})}^{B} = A^{B} {(\frac{1}{A})}^{B}$
21	17 19 11 20	syl3anc	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to {A (\frac{1}{A})}^{B} = A^{B} {(\frac{1}{A})}^{B}$
22		1cxp	$⊢ B \in ℂ \to 1^{B} = 1$
23	11 22	syl	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to 1^{B} = 1$
24	15 21 23	3eqtr3d	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to A^{B} {(\frac{1}{A})}^{B} = 1$
25	3 7 13 24	mvllmuld	$⊢ (A \in ℝ^{+} \land B \in ℂ) \to {(\frac{1}{A})}^{B} = \frac{1}{A^{B}}$

Metamath Proof Explorer

Theorem cxprec

Proof