divcxp

Description: Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 8-Sep-2014)

		Ref	Expression
	Assertion	divcxp	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to {(\frac{A}{B})}^{C} = \frac{A^{C}}{B^{C}}$

Proof

Step	Hyp	Ref	Expression
1		simp1l	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to A \in ℝ$
2		simp1r	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to 0 \leq A$
3		simp2	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to B \in ℝ^{+}$
4	3	rpreccld	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to \frac{1}{B} \in ℝ^{+}$
5	4	rpred	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to \frac{1}{B} \in ℝ$
6	4	rpge0d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to 0 \leq \frac{1}{B}$
7		simp3	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to C \in ℂ$
8		mulcxp	$⊢ ((A \in ℝ \land 0 \leq A) \land (\frac{1}{B} \in ℝ \land 0 \leq \frac{1}{B}) \land C \in ℂ) \to {A (\frac{1}{B})}^{C} = A^{C} {(\frac{1}{B})}^{C}$
9	1 2 5 6 7 8	syl221anc	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to {A (\frac{1}{B})}^{C} = A^{C} {(\frac{1}{B})}^{C}$
10		cxprec	$⊢ (B \in ℝ^{+} \land C \in ℂ) \to {(\frac{1}{B})}^{C} = \frac{1}{B^{C}}$
11	3 7 10	syl2anc	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to {(\frac{1}{B})}^{C} = \frac{1}{B^{C}}$
12	11	oveq2d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to A^{C} {(\frac{1}{B})}^{C} = A^{C} (\frac{1}{B^{C}})$
13	9 12	eqtrd	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to {A (\frac{1}{B})}^{C} = A^{C} (\frac{1}{B^{C}})$
14	1	recnd	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to A \in ℂ$
15	3	rpcnd	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to B \in ℂ$
16	3	rpne0d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to B \neq 0$
17	14 15 16	divrecd	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to \frac{A}{B} = A (\frac{1}{B})$
18	17	oveq1d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to {(\frac{A}{B})}^{C} = {A (\frac{1}{B})}^{C}$
19		cxpcl	$⊢ (A \in ℂ \land C \in ℂ) \to A^{C} \in ℂ$
20	14 7 19	syl2anc	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to A^{C} \in ℂ$
21		cxpcl	$⊢ (B \in ℂ \land C \in ℂ) \to B^{C} \in ℂ$
22	15 7 21	syl2anc	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to B^{C} \in ℂ$
23		cxpne0	$⊢ (B \in ℂ \land B \neq 0 \land C \in ℂ) \to B^{C} \neq 0$
24	15 16 7 23	syl3anc	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to B^{C} \neq 0$
25	20 22 24	divrecd	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to \frac{A^{C}}{B^{C}} = A^{C} (\frac{1}{B^{C}})$
26	13 18 25	3eqtr4d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+} \land C \in ℂ) \to {(\frac{A}{B})}^{C} = \frac{A^{C}}{B^{C}}$

Metamath Proof Explorer

Theorem divcxp

Proof