recxpcl

Description: Real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014)

		Ref	Expression
	Assertion	recxpcl	$⊢ (A \in ℝ \land 0 \leq A \land B \in ℝ) \to A^{B} \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		recn	$⊢ B \in ℝ \to B \in ℂ$
3		cxpval	$⊢ (A \in ℂ \land B \in ℂ) \to A^{B} = if (A = 0, if (B = 0, 1, 0), e^{B \log A})$
4	1 2 3	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to A^{B} = if (A = 0, if (B = 0, 1, 0), e^{B \log A})$
5	4	3adant2	$⊢ (A \in ℝ \land 0 \leq A \land B \in ℝ) \to A^{B} = if (A = 0, if (B = 0, 1, 0), e^{B \log A})$
6		1re	$⊢ 1 \in ℝ$
7		0re	$⊢ 0 \in ℝ$
8	6 7	ifcli	$⊢ if (B = 0, 1, 0) \in ℝ$
9	8	a1i	$⊢ ((A \in ℝ \land 0 \leq A \land B \in ℝ) \land A = 0) \to if (B = 0, 1, 0) \in ℝ$
10		df-ne	$⊢ A \neq 0 \leftrightarrow \neg A = 0$
11		simpl3	$⊢ ((A \in ℝ \land 0 \leq A \land B \in ℝ) \land A \neq 0) \to B \in ℝ$
12		simpl1	$⊢ ((A \in ℝ \land 0 \leq A \land B \in ℝ) \land A \neq 0) \to A \in ℝ$
13		simpl2	$⊢ ((A \in ℝ \land 0 \leq A \land B \in ℝ) \land A \neq 0) \to 0 \leq A$
14		simpr	$⊢ ((A \in ℝ \land 0 \leq A \land B \in ℝ) \land A \neq 0) \to A \neq 0$
15	12 13 14	ne0gt0d	$⊢ ((A \in ℝ \land 0 \leq A \land B \in ℝ) \land A \neq 0) \to 0 < A$
16	12 15	elrpd	$⊢ ((A \in ℝ \land 0 \leq A \land B \in ℝ) \land A \neq 0) \to A \in ℝ^{+}$
17	16	relogcld	$⊢ ((A \in ℝ \land 0 \leq A \land B \in ℝ) \land A \neq 0) \to \log A \in ℝ$
18	11 17	remulcld	$⊢ ((A \in ℝ \land 0 \leq A \land B \in ℝ) \land A \neq 0) \to B \log A \in ℝ$
19	18	reefcld	$⊢ ((A \in ℝ \land 0 \leq A \land B \in ℝ) \land A \neq 0) \to e^{B \log A} \in ℝ$
20	10 19	sylan2br	$⊢ ((A \in ℝ \land 0 \leq A \land B \in ℝ) \land \neg A = 0) \to e^{B \log A} \in ℝ$
21	9 20	ifclda	$⊢ (A \in ℝ \land 0 \leq A \land B \in ℝ) \to if (A = 0, if (B = 0, 1, 0), e^{B \log A}) \in ℝ$
22	5 21	eqeltrd	$⊢ (A \in ℝ \land 0 \leq A \land B \in ℝ) \to A^{B} \in ℝ$

Metamath Proof Explorer

Theorem recxpcl

Proof