Theorem expge0

Description: Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by NM, 16-Dec-2005) (Revised by Mario Carneiro, 4-Jun-2014)

	Ref	Expression
Assertion	expge0	$$⊢\left(A\in ℝ\wedge N\in {\mathbb{N}}_0\wedge 0\le A\right)\to 0\le A^N$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢z=A\to \left(0\le z\leftrightarrow 0\le A\right)$$
2	1	elrab	$$⊢A\in \left\{z\in ℝ|0\le z\right\}\leftrightarrow \left(A\in ℝ\wedge 0\le A\right)$$
3		ssrab2	$$⊢\left\{z\in ℝ|0\le z\right\}\subseteq ℝ$$
4		ax-resscn	$$⊢ℝ\subseteq ℂ$$
5	3 4	sstri	$$⊢\left\{z\in ℝ|0\le z\right\}\subseteq ℂ$$
6		breq2	$$⊢z=x\to \left(0\le z\leftrightarrow 0\le x\right)$$
7	6	elrab	$$⊢x\in \left\{z\in ℝ|0\le z\right\}\leftrightarrow \left(x\in ℝ\wedge 0\le x\right)$$
8		breq2	$$⊢z=y\to \left(0\le z\leftrightarrow 0\le y\right)$$
9	8	elrab	$$⊢y\in \left\{z\in ℝ|0\le z\right\}\leftrightarrow \left(y\in ℝ\wedge 0\le y\right)$$
10		breq2	$$⊢z=xy\to \left(0\le z\leftrightarrow 0\le xy\right)$$
11		remulcl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to xy\in ℝ$$
12	11	ad2ant2r	$$⊢\left(\left(x\in ℝ\wedge 0\le x\right)\wedge \left(y\in ℝ\wedge 0\le y\right)\right)\to xy\in ℝ$$
13		mulge0	$$⊢\left(\left(x\in ℝ\wedge 0\le x\right)\wedge \left(y\in ℝ\wedge 0\le y\right)\right)\to 0\le xy$$
14	10 12 13	elrabd	$$⊢\left(\left(x\in ℝ\wedge 0\le x\right)\wedge \left(y\in ℝ\wedge 0\le y\right)\right)\to xy\in \left\{z\in ℝ|0\le z\right\}$$
15	7 9 14	syl2anb	$$⊢\left(x\in \left\{z\in ℝ|0\le z\right\}\wedge y\in \left\{z\in ℝ|0\le z\right\}\right)\to xy\in \left\{z\in ℝ|0\le z\right\}$$
16		1re	$$⊢1\in ℝ$$
17		0le1	$$⊢0\le 1$$
18		breq2	$$⊢z=1\to \left(0\le z\leftrightarrow 0\le 1\right)$$
19	18	elrab	$$⊢1\in \left\{z\in ℝ|0\le z\right\}\leftrightarrow \left(1\in ℝ\wedge 0\le 1\right)$$
20	16 17 19	mpbir2an	$$⊢1\in \left\{z\in ℝ|0\le z\right\}$$
21	5 15 20	expcllem	$$⊢\left(A\in \left\{z\in ℝ|0\le z\right\}\wedge N\in {\mathbb{N}}_0\right)\to A^N\in \left\{z\in ℝ|0\le z\right\}$$
22		breq2	$$⊢z=A^N\to \left(0\le z\leftrightarrow 0\le A^N\right)$$
23	22	elrab	$$⊢A^N\in \left\{z\in ℝ|0\le z\right\}\leftrightarrow \left(A^N\in ℝ\wedge 0\le A^N\right)$$
24	23	simprbi	$$⊢A^N\in \left\{z\in ℝ|0\le z\right\}\to 0\le A^N$$
25	21 24	syl	$$⊢\left(A\in \left\{z\in ℝ|0\le z\right\}\wedge N\in {\mathbb{N}}_0\right)\to 0\le A^N$$
26	2 25	sylanbr	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge N\in {\mathbb{N}}_0\right)\to 0\le A^N$$
27	26	3impa	$$⊢\left(A\in ℝ\wedge 0\le A\wedge N\in {\mathbb{N}}_0\right)\to 0\le A^N$$
28	27	3com23	$$⊢\left(A\in ℝ\wedge N\in {\mathbb{N}}_0\wedge 0\le A\right)\to 0\le A^N$$