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