Metamath Proof Explorer


Theorem oeeu

Description: The division algorithm for ordinal exponentiation. (Contributed by Mario Carneiro, 25-May-2015)

Ref Expression
Assertion oeeu A On 2 𝑜 B On 1 𝑜 ∃! w x On y A 1 𝑜 z A 𝑜 x w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B

Proof

Step Hyp Ref Expression
1 eqid a On | B A 𝑜 a = a On | B A 𝑜 a
2 1 oeeulem A On 2 𝑜 B On 1 𝑜 a On | B A 𝑜 a On A 𝑜 a On | B A 𝑜 a B B A 𝑜 suc a On | B A 𝑜 a
3 2 simp1d A On 2 𝑜 B On 1 𝑜 a On | B A 𝑜 a On
4 fvexd A On 2 𝑜 B On 1 𝑜 1 st ι d | b On c A 𝑜 a On | B A 𝑜 a d = b c A 𝑜 a On | B A 𝑜 a 𝑜 b + 𝑜 c = B V
5 fvexd A On 2 𝑜 B On 1 𝑜 2 nd ι d | b On c A 𝑜 a On | B A 𝑜 a d = b c A 𝑜 a On | B A 𝑜 a 𝑜 b + 𝑜 c = B V
6 eqid ι d | b On c A 𝑜 a On | B A 𝑜 a d = b c A 𝑜 a On | B A 𝑜 a 𝑜 b + 𝑜 c = B = ι d | b On c A 𝑜 a On | B A 𝑜 a d = b c A 𝑜 a On | B A 𝑜 a 𝑜 b + 𝑜 c = B
7 eqid 1 st ι d | b On c A 𝑜 a On | B A 𝑜 a d = b c A 𝑜 a On | B A 𝑜 a 𝑜 b + 𝑜 c = B = 1 st ι d | b On c A 𝑜 a On | B A 𝑜 a d = b c A 𝑜 a On | B A 𝑜 a 𝑜 b + 𝑜 c = B
8 eqid 2 nd ι d | b On c A 𝑜 a On | B A 𝑜 a d = b c A 𝑜 a On | B A 𝑜 a 𝑜 b + 𝑜 c = B = 2 nd ι d | b On c A 𝑜 a On | B A 𝑜 a d = b c A 𝑜 a On | B A 𝑜 a 𝑜 b + 𝑜 c = B
9 1 6 7 8 oeeui A On 2 𝑜 B On 1 𝑜 x On y A 1 𝑜 z A 𝑜 x A 𝑜 x 𝑜 y + 𝑜 z = B x = a On | B A 𝑜 a y = 1 st ι d | b On c A 𝑜 a On | B A 𝑜 a d = b c A 𝑜 a On | B A 𝑜 a 𝑜 b + 𝑜 c = B z = 2 nd ι d | b On c A 𝑜 a On | B A 𝑜 a d = b c A 𝑜 a On | B A 𝑜 a 𝑜 b + 𝑜 c = B
10 3 4 5 9 euotd A On 2 𝑜 B On 1 𝑜 ∃! w x y z w = x y z x On y A 1 𝑜 z A 𝑜 x A 𝑜 x 𝑜 y + 𝑜 z = B
11 df-3an x On y A 1 𝑜 z A 𝑜 x x On y A 1 𝑜 z A 𝑜 x
12 11 biancomi x On y A 1 𝑜 z A 𝑜 x z A 𝑜 x x On y A 1 𝑜
13 12 anbi1i x On y A 1 𝑜 z A 𝑜 x A 𝑜 x 𝑜 y + 𝑜 z = B z A 𝑜 x x On y A 1 𝑜 A 𝑜 x 𝑜 y + 𝑜 z = B
14 13 anbi2i w = x y z x On y A 1 𝑜 z A 𝑜 x A 𝑜 x 𝑜 y + 𝑜 z = B w = x y z z A 𝑜 x x On y A 1 𝑜 A 𝑜 x 𝑜 y + 𝑜 z = B
15 an12 w = x y z z A 𝑜 x x On y A 1 𝑜 A 𝑜 x 𝑜 y + 𝑜 z = B z A 𝑜 x x On y A 1 𝑜 w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B
16 anass z A 𝑜 x x On y A 1 𝑜 w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B z A 𝑜 x x On y A 1 𝑜 w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B
17 14 15 16 3bitri w = x y z x On y A 1 𝑜 z A 𝑜 x A 𝑜 x 𝑜 y + 𝑜 z = B z A 𝑜 x x On y A 1 𝑜 w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B
18 17 exbii z w = x y z x On y A 1 𝑜 z A 𝑜 x A 𝑜 x 𝑜 y + 𝑜 z = B z z A 𝑜 x x On y A 1 𝑜 w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B
19 df-rex z A 𝑜 x x On y A 1 𝑜 w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B z z A 𝑜 x x On y A 1 𝑜 w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B
20 r19.42v z A 𝑜 x x On y A 1 𝑜 w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B x On y A 1 𝑜 z A 𝑜 x w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B
21 18 19 20 3bitr2i z w = x y z x On y A 1 𝑜 z A 𝑜 x A 𝑜 x 𝑜 y + 𝑜 z = B x On y A 1 𝑜 z A 𝑜 x w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B
22 21 2exbii x y z w = x y z x On y A 1 𝑜 z A 𝑜 x A 𝑜 x 𝑜 y + 𝑜 z = B x y x On y A 1 𝑜 z A 𝑜 x w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B
23 r2ex x On y A 1 𝑜 z A 𝑜 x w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B x y x On y A 1 𝑜 z A 𝑜 x w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B
24 22 23 bitr4i x y z w = x y z x On y A 1 𝑜 z A 𝑜 x A 𝑜 x 𝑜 y + 𝑜 z = B x On y A 1 𝑜 z A 𝑜 x w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B
25 24 eubii ∃! w x y z w = x y z x On y A 1 𝑜 z A 𝑜 x A 𝑜 x 𝑜 y + 𝑜 z = B ∃! w x On y A 1 𝑜 z A 𝑜 x w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B
26 10 25 sylib A On 2 𝑜 B On 1 𝑜 ∃! w x On y A 1 𝑜 z A 𝑜 x w = x y z A 𝑜 x 𝑜 y + 𝑜 z = B