Description: The division algorithm for ordinal exponentiation. (This version of oeeu gives an explicit expression for the unique solution of the equation, in terms of the solution P to omeu .) (Contributed by Mario Carneiro, 25-May-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | oeeu.1 | |
|
oeeu.2 | |
||
oeeu.3 | |
||
oeeu.4 | |
||
Assertion | oeeui | |