MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oeeui Unicode version

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

Proof of Theorem oeeui
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldifi 3625 . . . . . . . . . . . . . . . . . 18
21adantr 465 . . . . . . . . . . . . . . . . 17
32ad2antrr 725 . . . . . . . . . . . . . . . 16
4 simprl 756 . . . . . . . . . . . . . . . 16
5 oecl 7206 . . . . . . . . . . . . . . . 16
63, 4, 5syl2anc 661 . . . . . . . . . . . . . . 15
7 om1 7210 . . . . . . . . . . . . . . 15
86, 7syl 16 . . . . . . . . . . . . . 14
9 df1o2 7161 . . . . . . . . . . . . . . . 16
10 dif1o 7169 . . . . . . . . . . . . . . . . . . . 20
1110simprbi 464 . . . . . . . . . . . . . . . . . . 19
1211ad2antll 728 . . . . . . . . . . . . . . . . . 18
13 eldifi 3625 . . . . . . . . . . . . . . . . . . . . 21
1413ad2antll 728 . . . . . . . . . . . . . . . . . . . 20
15 onelon 4908 . . . . . . . . . . . . . . . . . . . 20
163, 14, 15syl2anc 661 . . . . . . . . . . . . . . . . . . 19
17 on0eln0 4938 . . . . . . . . . . . . . . . . . . 19
1816, 17syl 16 . . . . . . . . . . . . . . . . . 18
1912, 18mpbird 232 . . . . . . . . . . . . . . . . 17
2019snssd 4175 . . . . . . . . . . . . . . . 16
219, 20syl5eqss 3547 . . . . . . . . . . . . . . 15
22 1on 7156 . . . . . . . . . . . . . . . . 17
2322a1i 11 . . . . . . . . . . . . . . . 16
24 omwordi 7239 . . . . . . . . . . . . . . . 16
2523, 16, 6, 24syl3anc 1228 . . . . . . . . . . . . . . 15
2621, 25mpd 15 . . . . . . . . . . . . . 14
278, 26eqsstr3d 3538 . . . . . . . . . . . . 13
28 omcl 7205 . . . . . . . . . . . . . . . 16
296, 16, 28syl2anc 661 . . . . . . . . . . . . . . 15
30 simplrl 761 . . . . . . . . . . . . . . . 16
31 onelon 4908 . . . . . . . . . . . . . . . 16
326, 30, 31syl2anc 661 . . . . . . . . . . . . . . 15
33 oaword1 7220 . . . . . . . . . . . . . . 15
3429, 32, 33syl2anc 661 . . . . . . . . . . . . . 14
35 simplrr 762 . . . . . . . . . . . . . 14
3634, 35sseqtrd 3539 . . . . . . . . . . . . 13
3727, 36sstrd 3513 . . . . . . . . . . . 12
38 oeeu.1 . . . . . . . . . . . . . . 15
3938oeeulem 7269 . . . . . . . . . . . . . 14
4039simp3d 1010 . . . . . . . . . . . . 13
4140ad2antrr 725 . . . . . . . . . . . 12
4239simp1d 1008 . . . . . . . . . . . . . . . 16
4342ad2antrr 725 . . . . . . . . . . . . . . 15
44 suceloni 6648 . . . . . . . . . . . . . . 15
4543, 44syl 16 . . . . . . . . . . . . . 14
46 oecl 7206 . . . . . . . . . . . . . 14
473, 45, 46syl2anc 661 . . . . . . . . . . . . 13
48 ontr2 4930 . . . . . . . . . . . . 13
496, 47, 48syl2anc 661 . . . . . . . . . . . 12
5037, 41, 49mp2and 679 . . . . . . . . . . 11
51 simplll 759 . . . . . . . . . . . 12
52 oeord 7256 . . . . . . . . . . . 12
534, 45, 51, 52syl3anc 1228 . . . . . . . . . . 11
5450, 53mpbird 232 . . . . . . . . . 10
55 onsssuc 4970 . . . . . . . . . . 11
564, 43, 55syl2anc 661 . . . . . . . . . 10
5754, 56mpbird 232 . . . . . . . . 9
5839simp2d 1009 . . . . . . . . . . . . 13
5958ad2antrr 725 . . . . . . . . . . . 12
60 eloni 4893 . . . . . . . . . . . . . . . . 17
613, 60syl 16 . . . . . . . . . . . . . . . 16
62 ordsucss 6653 . . . . . . . . . . . . . . . 16
6361, 14, 62sylc 60 . . . . . . . . . . . . . . 15
64 suceloni 6648 . . . . . . . . . . . . . . . . 17
6516, 64syl 16 . . . . . . . . . . . . . . . 16
66 dif20el 7174 . . . . . . . . . . . . . . . . . 18
6751, 66syl 16 . . . . . . . . . . . . . . . . 17
68 oen0 7254 . . . . . . . . . . . . . . . . 17
693, 4, 67, 68syl21anc 1227 . . . . . . . . . . . . . . . 16
70 omword 7238 . . . . . . . . . . . . . . . 16
7165, 3, 6, 69, 70syl31anc 1231 . . . . . . . . . . . . . . 15
7263, 71mpbid 210 . . . . . . . . . . . . . 14
73 oaord 7215 . . . . . . . . . . . . . . . . . 18
7432, 6, 29, 73syl3anc 1228 . . . . . . . . . . . . . . . . 17
7530, 74mpbid 210 . . . . . . . . . . . . . . . 16
7635, 75eqeltrrd 2546 . . . . . . . . . . . . . . 15
77 odi 7247 . . . . . . . . . . . . . . . . 17
786, 16, 23, 77syl3anc 1228 . . . . . . . . . . . . . . . 16
79 oa1suc 7200 . . . . . . . . . . . . . . . . . 18
8016, 79syl 16 . . . . . . . . . . . . . . . . 17
8180oveq2d 6312 . . . . . . . . . . . . . . . 16
828oveq2d 6312 . . . . . . . . . . . . . . . 16
8378, 81, 823eqtr3d 2506 . . . . . . . . . . . . . . 15
8476, 83eleqtrrd 2548 . . . . . . . . . . . . . 14
8572, 84sseldd 3504 . . . . . . . . . . . . 13
86 oesuc 7196 . . . . . . . . . . . . . 14
873, 4, 86syl2anc 661 . . . . . . . . . . . . 13
8885, 87eleqtrrd 2548 . . . . . . . . . . . 12
89 oecl 7206 . . . . . . . . . . . . . 14
903, 43, 89syl2anc 661 . . . . . . . . . . . . 13
91 suceloni 6648 . . . . . . . . . . . . . . 15
9291ad2antrl 727 . . . . . . . . . . . . . 14
93 oecl 7206 . . . . . . . . . . . . . 14
943, 92, 93syl2anc 661 . . . . . . . . . . . . 13
95 ontr2 4930 . . . . . . . . . . . . 13
9690, 94, 95syl2anc 661 . . . . . . . . . . . 12
9759, 88, 96mp2and 679 . . . . . . . . . . 11
98 oeord 7256 . . . . . . . . . . . 12
9943, 92, 51, 98syl3anc 1228 . . . . . . . . . . 11
10097, 99mpbird 232 . . . . . . . . . 10
101 onsssuc 4970 . . . . . . . . . . 11
10243, 4, 101syl2anc 661 . . . . . . . . . 10
103100, 102mpbird 232 . . . . . . . . 9
10457, 103eqssd 3520 . . . . . . . 8
105104, 16jca 532 . . . . . . 7
106 simprl 756 . . . . . . . . 9
10742ad2antrr 725 . . . . . . . . 9