Proof of Theorem dp35lemd
Step | Hyp | Ref
| Expression |
1 | | lea 160 |
. . 3
b0 a0 p0 b0 |
2 | | dp35lem.1 |
. . . 4
c0 a1 a2 b1 b2 |
3 | | dp35lem.2 |
. . . 4
c1 a0 a2 b0 b2 |
4 | | dp35lem.3 |
. . . 4
c2 a0 a1 b0 b1 |
5 | | dp35lem.4 |
. . . 4
p0 a1 b1 a2 b2 |
6 | | dp35lem.5 |
. . . 4
a0 b0 a1 b1 a2
b2 |
7 | 2, 3, 4, 5, 6 | dp35leme 1171 |
. . 3
b0 a0 p0 a0 b0 b1 c2
c0 c1 |
8 | 1, 7 | ler2an 173 |
. 2
b0 a0 p0 b0 a0 b0 b1
c2 c0 c1 |
9 | | lea 160 |
. . . 4
b0 b1 c2 c0
c1 b0 |
10 | 9 | mldual2i 1125 |
. . 3
b0 a0 b0 b1
c2 c0 c1 b0 a0
b0 b1 c2 c0
c1 |
11 | | lea 160 |
. . . . 5
b0 a0 b0 |
12 | 11, 9 | lel2or 170 |
. . . 4
b0
a0
b0 b1 c2 c0
c1 b0 |
13 | | ancom 74 |
. . . . . . 7
b0 a0 a0 b0 |
14 | 13 | bile 142 |
. . . . . 6
b0 a0 a0 b0 |
15 | | lear 161 |
. . . . . 6
b0 b1 c2 c0
c1 b1 c2 c0 c1 |
16 | 14, 15 | le2or 168 |
. . . . 5
b0
a0
b0 b1 c2 c0
c1 a0
b0
b1 c2 c0 c1 |
17 | | orass 75 |
. . . . . 6
a0 b0
b1 c2 c0 c1 a0 b0 b1 c2 c0
c1 |
18 | 17 | cm 61 |
. . . . 5
a0
b0
b1 c2 c0 c1 a0
b0
b1 c2 c0 c1 |
19 | 16, 18 | lbtr 139 |
. . . 4
b0
a0
b0 b1 c2 c0
c1 a0 b0
b1 c2 c0 c1 |
20 | 12, 19 | ler2an 173 |
. . 3
b0
a0
b0 b1 c2 c0
c1 b0 a0
b0
b1 c2 c0 c1 |
21 | 10, 20 | bltr 138 |
. 2
b0 a0 b0 b1
c2 c0 c1 b0 a0
b0
b1 c2 c0 c1 |
22 | 8, 21 | letr 137 |
1
b0 a0 p0 b0 a0
b0
b1 c2 c0 c1 |