Description: Ordinal exponentiation with zero mantissa 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 |