Theorem cxpge0

Description: Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 2-Aug-2014)

	Ref	Expression
Assertion	cxpge0	$$⊢\left(A\in ℝ\wedge 0\le A\wedge B\in ℝ\right)\to 0\le A^B$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2		leloe	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to \left(0\le A\leftrightarrow \left(0<A\vee 0=A\right)\right)$$
3	1 2	mpan	$$⊢A\in ℝ\to \left(0\le A\leftrightarrow \left(0<A\vee 0=A\right)\right)$$
4	3	adantr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0\le A\leftrightarrow \left(0<A\vee 0=A\right)\right)$$
5		elrp	$$⊢A\in {ℝ}^{+}\leftrightarrow \left(A\in ℝ\wedge 0<A\right)$$
6		rpcxpcl	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to A^B\in {ℝ}^{+}$$
7	6	rpge0d	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to 0\le A^B$$
8	7	ex	$$⊢A\in {ℝ}^{+}\to \left(B\in ℝ\to 0\le A^B\right)$$
9	5 8	sylbir	$$⊢\left(A\in ℝ\wedge 0<A\right)\to \left(B\in ℝ\to 0\le A^B\right)$$
10	9	impancom	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0<A\to 0\le A^B\right)$$
11		0le1	$$⊢0\le 1$$
12		0cn	$$⊢0\in ℂ$$
13		cxp0	$$⊢0\in ℂ\to 0^0=1$$
14	12 13	ax-mp	$$⊢0^0=1$$
15	11 14	breqtrri	$$⊢0\le 0^0$$
16		simpr	$$⊢\left(B\in ℝ\wedge B=0\right)\to B=0$$
17	16	oveq2d	$$⊢\left(B\in ℝ\wedge B=0\right)\to 0^B=0^0$$
18	15 17	breqtrrid	$$⊢\left(B\in ℝ\wedge B=0\right)\to 0\le 0^B$$
19		0le0	$$⊢0\le 0$$
20		recn	$$⊢B\in ℝ\to B\in ℂ$$
21		0cxp	$$⊢\left(B\in ℂ\wedge B\ne 0\right)\to 0^B=0$$
22	20 21	sylan	$$⊢\left(B\in ℝ\wedge B\ne 0\right)\to 0^B=0$$
23	19 22	breqtrrid	$$⊢\left(B\in ℝ\wedge B\ne 0\right)\to 0\le 0^B$$
24	18 23	pm2.61dane	$$⊢B\in ℝ\to 0\le 0^B$$
25	24	adantl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to 0\le 0^B$$
26		oveq1	$$⊢0=A\to 0^B=A^B$$
27	26	breq2d	$$⊢0=A\to \left(0\le 0^B\leftrightarrow 0\le A^B\right)$$
28	25 27	syl5ibcom	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0=A\to 0\le A^B\right)$$
29	10 28	jaod	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\left(0<A\vee 0=A\right)\to 0\le A^B\right)$$
30	4 29	sylbid	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(0\le A\to 0\le A^B\right)$$
31	30	3impia	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge 0\le A\right)\to 0\le A^B$$
32	31	3com23	$$⊢\left(A\in ℝ\wedge 0\le A\wedge B\in ℝ\right)\to 0\le A^B$$