Description: A real between 0 and 1 inclusive raised to a nonnegative integer power is less than or equal to 1. (Contributed by Paul Chapman, 29-Dec-2007) (Revised by Mario Carneiro, 5-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | exple1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl1 | |
|
2 | 0nn0 | |
|
3 | 2 | a1i | |
4 | simpr | |
|
5 | nn0uz | |
|
6 | 4 5 | eleqtrdi | |
7 | simpl2 | |
|
8 | simpl3 | |
|
9 | leexp2r | |
|
10 | 1 3 6 7 8 9 | syl32anc | |
11 | 1 | recnd | |
12 | exp0 | |
|
13 | 11 12 | syl | |
14 | 10 13 | breqtrd | |