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 A N 0 0 A 0 A N

Proof

Step Hyp Ref Expression
1 breq2 z = A 0 z 0 A
2 1 elrab A z | 0 z A 0 A
3 ssrab2 z | 0 z
4 ax-resscn
5 3 4 sstri z | 0 z
6 breq2 z = x 0 z 0 x
7 6 elrab x z | 0 z x 0 x
8 breq2 z = y 0 z 0 y
9 8 elrab y z | 0 z y 0 y
10 breq2 z = x y 0 z 0 x y
11 remulcl x y x y
12 11 ad2ant2r x 0 x y 0 y x y
13 mulge0 x 0 x y 0 y 0 x y
14 10 12 13 elrabd x 0 x y 0 y x y z | 0 z
15 7 9 14 syl2anb x z | 0 z y z | 0 z x y z | 0 z
16 1re 1
17 0le1 0 1
18 breq2 z = 1 0 z 0 1
19 18 elrab 1 z | 0 z 1 0 1
20 16 17 19 mpbir2an 1 z | 0 z
21 5 15 20 expcllem A z | 0 z N 0 A N z | 0 z
22 breq2 z = A N 0 z 0 A N
23 22 elrab A N z | 0 z A N 0 A N
24 23 simprbi A N z | 0 z 0 A N
25 21 24 syl A z | 0 z N 0 0 A N
26 2 25 sylanbr A 0 A N 0 0 A N
27 26 3impa A 0 A N 0 0 A N
28 27 3com23 A N 0 0 A 0 A N