Metamath Proof Explorer


Theorem expge0

Description: A nonnegative real raised to a nonnegative integer is nonnegative. (Contributed by NM, 16-Dec-2005) (Revised by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expge0 AN00A0AN

Proof

Step Hyp Ref Expression
1 breq2 z=A0z0A
2 1 elrab Az|0zA0A
3 ssrab2 z|0z
4 ax-resscn
5 3 4 sstri z|0z
6 breq2 z=x0z0x
7 6 elrab xz|0zx0x
8 breq2 z=y0z0y
9 8 elrab yz|0zy0y
10 breq2 z=xy0z0xy
11 remulcl xyxy
12 11 ad2ant2r x0xy0yxy
13 mulge0 x0xy0y0xy
14 10 12 13 elrabd x0xy0yxyz|0z
15 7 9 14 syl2anb xz|0zyz|0zxyz|0z
16 1re 1
17 0le1 01
18 breq2 z=10z01
19 18 elrab 1z|0z101
20 16 17 19 mpbir2an 1z|0z
21 5 15 20 expcllem Az|0zN0ANz|0z
22 breq2 z=AN0z0AN
23 22 elrab ANz|0zAN0AN
24 23 simprbi ANz|0z0AN
25 21 24 syl Az|0zN00AN
26 2 25 sylanbr A0AN00AN
27 26 3impa A0AN00AN
28 27 3com23 AN00A0AN