Description: Ordinal exponentiation with zero base and nonzero exponent. Proposition 8.31(2) of TakeutiZaring p. 67 and its converse. (Contributed by NM, 5-Jan-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | oe0m1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eloni | |
|
2 | ordgt0ge1 | |
|
3 | 1 2 | syl | |
4 | ssdif0 | |
|
5 | oe0m | |
|
6 | 5 | eqeq1d | |
7 | 4 6 | bitr4id | |
8 | 3 7 | bitrd | |