Proof of Theorem dp15leme
Step | Hyp | Ref
| Expression |
1 | | ax-a2 31 |
. . . . . . 7
a1 a2 a2 a1 |
2 | | ax-a2 31 |
. . . . . . . 8
a1 b1 b1 a1 |
3 | 2 | lan 77 |
. . . . . . 7
a0 a1 b1 a0
b1 a1 |
4 | 1, 3 | 2or 72 |
. . . . . 6
a1
a2
a0 a1 b1 a2 a1 a0 b1 a1 |
5 | | orass 75 |
. . . . . 6
a2
a1
a0 b1 a1 a2 a1 a0
b1 a1 |
6 | 4, 5 | tr 62 |
. . . . 5
a1
a2
a0 a1 b1 a2 a1 a0
b1 a1 |
7 | | ml3le 1127 |
. . . . . 6
a1 a0 b1 a1 a1 b1 a0
a1 |
8 | 7 | lelor 166 |
. . . . 5
a2 a1 a0 b1
a1 a2 a1 b1 a0
a1 |
9 | 6, 8 | bltr 138 |
. . . 4
a1
a2
a0 a1 b1 a2 a1 b1
a0 a1 |
10 | | orass 75 |
. . . . . 6
a2
a1
b1 a0 a1 a2 a1 b1
a0 a1 |
11 | 10 | cm 61 |
. . . . 5
a2 a1 b1 a0
a1 a2 a1 b1 a0 a1 |
12 | | ax-a2 31 |
. . . . . 6
a2 a1 a1 a2 |
13 | 12 | ror 71 |
. . . . 5
a2
a1
b1 a0 a1 a1 a2 b1 a0 a1 |
14 | 11, 13 | tr 62 |
. . . 4
a2 a1 b1 a0
a1 a1 a2 b1 a0 a1 |
15 | 9, 14 | lbtr 139 |
. . 3
a1
a2
a0 a1 b1 a1 a2 b1 a0 a1 |
16 | 15 | leran 153 |
. 2
a1 a2
a0 a1 b1 b1 b2 a1 a2 b1 a0 a1 b1 b2 |
17 | 16 | lelor 166 |
1
a0 a2
b0
a0 p0 b2 a1 a2
a0 a1 b1 b1 b2 a0 a2 b0 a0 p0 b2 a1 a2 b1 a0 a1 b1 b2 |