Description: Product of exponents law for ordinal exponentiation. Theorem 8S of Enderton p. 238. Also Proposition 8.42 of TakeutiZaring p. 70. (Contributed by Eric Schmidt, 26-May-2009)
Ref | Expression | ||
---|---|---|---|
Assertion | oeoe | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq2 | |
|
2 | oe0m0 | |
|
3 | 1 2 | eqtrdi | |
4 | 3 | oveq1d | |
5 | oe1m | |
|
6 | 4 5 | sylan9eqr | |
7 | 6 | adantll | |
8 | oveq2 | |
|
9 | 0elon | |
|
10 | oecl | |
|
11 | 9 10 | mpan | |
12 | oe0 | |
|
13 | 11 12 | syl | |
14 | 8 13 | sylan9eqr | |
15 | 14 | adantlr | |
16 | 7 15 | jaodan | |
17 | om00 | |
|
18 | 17 | biimpar | |
19 | 18 | oveq2d | |
20 | 19 2 | eqtrdi | |
21 | 16 20 | eqtr4d | |
22 | on0eln0 | |
|
23 | on0eln0 | |
|
24 | 22 23 | bi2anan9 | |
25 | neanior | |
|
26 | 24 25 | bitrdi | |
27 | oe0m1 | |
|
28 | 27 | biimpa | |
29 | 28 | oveq1d | |
30 | oe0m1 | |
|
31 | 30 | biimpa | |
32 | 29 31 | sylan9eq | |
33 | 32 | an4s | |
34 | om00el | |
|
35 | omcl | |
|
36 | oe0m1 | |
|
37 | 35 36 | syl | |
38 | 34 37 | bitr3d | |
39 | 38 | biimpa | |
40 | 33 39 | eqtr4d | |
41 | 40 | ex | |
42 | 26 41 | sylbird | |
43 | 42 | imp | |
44 | 21 43 | pm2.61dan | |
45 | oveq1 | |
|
46 | 45 | oveq1d | |
47 | oveq1 | |
|
48 | 46 47 | eqeq12d | |
49 | 44 48 | syl5ibr | |
50 | 49 | impcom | |
51 | oveq1 | |
|
52 | 51 | oveq1d | |
53 | oveq1 | |
|
54 | 52 53 | eqeq12d | |
55 | 54 | imbi2d | |
56 | eleq1 | |
|
57 | eleq2 | |
|
58 | 56 57 | anbi12d | |
59 | eleq1 | |
|
60 | eleq2 | |
|
61 | 59 60 | anbi12d | |
62 | 1on | |
|
63 | 0lt1o | |
|
64 | 62 63 | pm3.2i | |
65 | 58 61 64 | elimhyp | |
66 | 65 | simpli | |
67 | 65 | simpri | |
68 | 66 67 | oeoelem | |
69 | 55 68 | dedth | |
70 | 69 | imp | |
71 | 70 | an32s | |
72 | 50 71 | oe0lem | |
73 | 72 | 3impb | |