Proof of Theorem dp41lemh
Step | Hyp | Ref
| Expression |
1 | | lea 160 |
. . . . 5
a0 a1 b1 a0 |
2 | | leo 158 |
. . . . . . 7
a0 a0 b0 |
3 | 2 | leran 153 |
. . . . . 6
a0 a1 b1 a0 b0
a1 b1 |
4 | | dp41lem.5 |
. . . . . . . 8
p2 a0 b0 a1 b1 |
5 | 4 | cm 61 |
. . . . . . 7
a0
b0
a1 b1 p2 |
6 | | dp41lem.6 |
. . . . . . 7
p2 a2 b2 |
7 | 5, 6 | bltr 138 |
. . . . . 6
a0
b0
a1 b1 a2 b2 |
8 | 3, 7 | letr 137 |
. . . . 5
a0 a1 b1 a2 b2 |
9 | 1, 8 | ler2an 173 |
. . . 4
a0 a1 b1 a0 a2 b2 |
10 | 9 | lelor 166 |
. . 3
a1
a2
a0 a1 b1 a1 a2 a0 a2 b2 |
11 | 10 | lelan 167 |
. 2
b1
b2
a1
a2
a0 a1 b1 b1 b2 a1 a2 a0 a2 b2 |
12 | | lea 160 |
. . . . 5
b1 a0 b0 b1 |
13 | | lear 161 |
. . . . . . 7
b1 a0 b0 a0 b0 |
14 | | leao3 164 |
. . . . . . 7
b1 a0 b0 a1 b1 |
15 | 13, 14 | ler2an 173 |
. . . . . 6
b1 a0 b0 a0 b0
a1 b1 |
16 | 15, 7 | letr 137 |
. . . . 5
b1 a0 b0 a2 b2 |
17 | 12, 16 | ler2an 173 |
. . . 4
b1 a0 b0 b1 a2 b2 |
18 | 17 | lelor 166 |
. . 3
b0
b2
b1 a0 b0 b0 b2 b1 a2 b2 |
19 | 18 | lelan 167 |
. 2
a0
a2
b0
b2
b1 a0 b0 a0 a2 b0 b2 b1 a2 b2 |
20 | 11, 19 | le2or 168 |
1
b1 b2
a1
a2
a0 a1 b1 a0 a2 b0 b2 b1 a0 b0 b1 b2
a1
a2
a0 a2 b2 a0 a2 b0 b2 b1 a2 b2 |