Step |
Hyp |
Ref |
Expression |
1 |
|
olc |
|
2 |
1
|
a1d |
|
3 |
|
nn0z |
|
4 |
|
2z |
|
5 |
|
zltlem1 |
|
6 |
3 4 5
|
sylancl |
|
7 |
|
2m1e1 |
|
8 |
7
|
breq2i |
|
9 |
6 8
|
bitrdi |
|
10 |
|
necom |
|
11 |
|
nn0re |
|
12 |
|
1re |
|
13 |
|
ltlen |
|
14 |
11 12 13
|
sylancl |
|
15 |
|
nn0lt10b |
|
16 |
15
|
biimpa |
|
17 |
16
|
orcd |
|
18 |
17
|
ex |
|
19 |
14 18
|
sylbird |
|
20 |
19
|
expd |
|
21 |
10 20
|
syl7bi |
|
22 |
9 21
|
sylbid |
|
23 |
22
|
imp |
|
24 |
23
|
com12 |
|
25 |
2 24
|
pm2.61ine |
|