Proof of Theorem xxdp53
Step | Hyp | Ref
| Expression |
1 | | leor 159 |
. 2
a0 |
2 | | leo 158 |
. . 3
a0 a0 b0 b1
c2 c0 c1 |
3 | | xxdp.p |
. . . . . . . 8
a0 b0 a1 b1 a2
b2 |
4 | | anass 76 |
. . . . . . . 8
a0 b0
a1 b1 a2 b2 a0 b0 a1 b1 a2 b2 |
5 | 3, 4 | tr 62 |
. . . . . . 7
a0 b0
a1
b1
a2 b2 |
6 | | xxdp.p0 |
. . . . . . . . . . 11
p0 a1 b1 a2 b2 |
7 | 6 | lan 77 |
. . . . . . . . . 10
a0
b0
p0 a0 b0 a1 b1 a2 b2 |
8 | 7 | cm 61 |
. . . . . . . . 9
a0
b0
a1
b1
a2 b2 a0
b0
p0 |
9 | | leao4 165 |
. . . . . . . . 9
a0
b0
p0 a0 p0 |
10 | 8, 9 | bltr 138 |
. . . . . . . 8
a0
b0
a1
b1
a2 b2 a0 p0 |
11 | | lea 160 |
. . . . . . . . 9
a0
b0
a1
b1
a2 b2 a0 b0 |
12 | | orcom 73 |
. . . . . . . . 9
a0 b0 b0 a0 |
13 | 11, 12 | lbtr 139 |
. . . . . . . 8
a0
b0
a1
b1
a2 b2 b0 a0 |
14 | 10, 13 | ler2an 173 |
. . . . . . 7
a0
b0
a1
b1
a2 b2 a0
p0
b0 a0 |
15 | 5, 14 | bltr 138 |
. . . . . 6
a0 p0
b0 a0 |
16 | | leo 158 |
. . . . . . . 8
a0 a0 p0 |
17 | 16 | mldual2i 1125 |
. . . . . . 7
a0
p0
b0 a0 a0
p0
b0 a0 |
18 | | ancom 74 |
. . . . . . . 8
a0
p0
b0 b0 a0 p0 |
19 | 18 | ror 71 |
. . . . . . 7
a0 p0
b0 a0 b0 a0 p0 a0 |
20 | 17, 19 | tr 62 |
. . . . . 6
a0
p0
b0 a0 b0 a0 p0 a0 |
21 | 15, 20 | lbtr 139 |
. . . . 5
b0 a0 p0 a0 |
22 | 2 | lelor 166 |
. . . . 5
b0
a0 p0 a0 b0 a0 p0 a0
b0 b1 c2 c0
c1 |
23 | 21, 22 | letr 137 |
. . . 4
b0 a0 p0 a0
b0 b1 c2 c0
c1 |
24 | | lea 160 |
. . . . . . . 8
b0 a0 p0 b0 |
25 | | leor 159 |
. . . . . . . . 9
b0 a0 p0 b1 b0 a0 p0 |
26 | | leo 158 |
. . . . . . . . . 10
b1 b1 a0 a1
c0 c1 |
27 | | leo 158 |
. . . . . . . . . . . . . 14
b0 a0 p0 b0 a0 p0 b1 |
28 | 6 | lor 70 |
. . . . . . . . . . . . . . . 16
a0 p0 a0 a1 b1
a2 b2 |
29 | 28 | lan 77 |
. . . . . . . . . . . . . . 15
b0 a0 p0 b0
a0 a1 b1 a2 b2 |
30 | | lear 161 |
. . . . . . . . . . . . . . . 16
b0 a0 a1 b1
a2 b2 a0 a1 b1 a2 b2 |
31 | | lea 160 |
. . . . . . . . . . . . . . . . . 18
a1
b1
a2 b2 a1 b1 |
32 | 31 | lelor 166 |
. . . . . . . . . . . . . . . . 17
a0 a1 b1 a2 b2 a0 a1 b1 |
33 | | ax-a3 32 |
. . . . . . . . . . . . . . . . . 18
a0
a1
b1 a0 a1 b1 |
34 | 33 | cm 61 |
. . . . . . . . . . . . . . . . 17
a0 a1 b1 a0 a1
b1 |
35 | 32, 34 | lbtr 139 |
. . . . . . . . . . . . . . . 16
a0 a1 b1 a2 b2 a0 a1 b1 |
36 | 30, 35 | letr 137 |
. . . . . . . . . . . . . . 15
b0 a0 a1 b1
a2 b2 a0 a1
b1 |
37 | 29, 36 | bltr 138 |
. . . . . . . . . . . . . 14
b0 a0 p0 a0 a1
b1 |
38 | 27, 37 | ler2an 173 |
. . . . . . . . . . . . 13
b0 a0 p0 b0 a0 p0 b1
a0
a1
b1 |
39 | | leor 159 |
. . . . . . . . . . . . . . 15
b1 b0 a0 p0 b1 |
40 | 39 | mldual2i 1125 |
. . . . . . . . . . . . . 14
b0 a0 p0 b1
a0
a1
b1 b0 a0 p0 b1
a0 a1 b1 |
41 | | ancom 74 |
. . . . . . . . . . . . . . 15
b0 a0 p0 b1
a0 a1 a0 a1 b0 a0 p0 b1 |
42 | 41 | ror 71 |
. . . . . . . . . . . . . 14
b0 a0 p0 b1
a0 a1 b1 a0
a1
b0
a0 p0 b1 b1 |
43 | 40, 42 | tr 62 |
. . . . . . . . . . . . 13
b0 a0 p0 b1
a0
a1
b1 a0 a1
b0
a0 p0 b1 b1 |
44 | 38, 43 | lbtr 139 |
. . . . . . . . . . . 12
b0 a0 p0 a0 a1 b0 a0 p0 b1 b1 |
45 | 26 | lelor 166 |
. . . . . . . . . . . 12
a0 a1
b0
a0 p0 b1 b1
a0 a1
b0
a0 p0 b1 b1 a0 a1 c0 c1 |
46 | 44, 45 | letr 137 |
. . . . . . . . . . 11
b0 a0 p0 a0 a1 b0 a0 p0 b1 b1
a0 a1
c0 c1 |
47 | | lea 160 |
. . . . . . . . . . . . . . . 16
a0
a1
b0
a0 p0 b1 a0 a1 |
48 | | xxdp.c0 |
. . . . . . . . . . . . . . . . 17
c0 a1 a2 b1 b2 |
49 | | xxdp.c1 |
. . . . . . . . . . . . . . . . 17
c1 a0 a2 b0 b2 |
50 | 48, 49, 6 | dp15 1160 |
. . . . . . . . . . . . . . . 16
a0
a1
b0
a0 p0 b1 c0
c1
b1 a0 a1 |
51 | 47, 50 | ler2an 173 |
. . . . . . . . . . . . . . 15
a0
a1
b0
a0 p0 b1 a0
a1
c0
c1
b1 a0 a1 |
52 | | lear 161 |
. . . . . . . . . . . . . . . 16
b1 a0 a1 a0 a1 |
53 | 52 | mldual2i 1125 |
. . . . . . . . . . . . . . 15
a0
a1
c0
c1
b1 a0 a1 a0
a1
c0 c1 b1 a0 a1 |
54 | 51, 53 | lbtr 139 |
. . . . . . . . . . . . . 14
a0
a1
b0
a0 p0 b1 a0 a1
c0 c1 b1 a0 a1 |
55 | | lea 160 |
. . . . . . . . . . . . . . 15
b1 a0 a1 b1 |
56 | 55 | lelor 166 |
. . . . . . . . . . . . . 14
a0 a1
c0 c1 b1 a0 a1 a0 a1 c0 c1 b1 |
57 | 54, 56 | letr 137 |
. . . . . . . . . . . . 13
a0
a1
b0
a0 p0 b1 a0 a1
c0 c1 b1 |
58 | | orcom 73 |
. . . . . . . . . . . . 13
a0 a1
c0 c1 b1 b1 a0 a1
c0 c1 |
59 | 57, 58 | lbtr 139 |
. . . . . . . . . . . 12
a0
a1
b0
a0 p0 b1 b1 a0 a1 c0 c1 |
60 | | leid 148 |
. . . . . . . . . . . 12
b1 a0 a1 c0 c1 b1 a0 a1
c0 c1 |
61 | 59, 60 | lel2or 170 |
. . . . . . . . . . 11
a0 a1
b0
a0 p0 b1 b1 a0 a1 c0 c1 b1 a0 a1 c0 c1 |
62 | 46, 61 | letr 137 |
. . . . . . . . . 10
b0 a0 p0 b1 a0 a1 c0 c1 |
63 | 26, 62 | lel2or 170 |
. . . . . . . . 9
b1 b0 a0 p0 b1 a0 a1
c0 c1 |
64 | 25, 63 | letr 137 |
. . . . . . . 8
b0 a0 p0 b1 a0 a1 c0 c1 |
65 | 24, 64 | ler2an 173 |
. . . . . . 7
b0 a0 p0 b0 b1 a0 a1
c0 c1 |
66 | | or32 82 |
. . . . . . . . . . 11
a0 b0
b1 c2 c0 c1 a0 b0 c2 c0 c1 b1 |
67 | | orcom 73 |
. . . . . . . . . . 11
a0 b0
c2 c0 c1 b1 b1 a0 b0 c2 c0 c1 |
68 | | leo 158 |
. . . . . . . . . . . . . . . 16
a0 a0 a1 |
69 | | leo 158 |
. . . . . . . . . . . . . . . 16
b0 b0 b1 |
70 | 68, 69 | le2an 169 |
. . . . . . . . . . . . . . 15
a0 b0 a0 a1 b0 b1 |
71 | | xxdp.c2 |
. . . . . . . . . . . . . . . 16
c2 a0 a1 b0 b1 |
72 | 71 | cm 61 |
. . . . . . . . . . . . . . 15
a0
a1
b0 b1 c2 |
73 | 70, 72 | lbtr 139 |
. . . . . . . . . . . . . 14
a0 b0 c2 |
74 | | leo 158 |
. . . . . . . . . . . . . . . . 17
a0 a0 a2 |
75 | | leo 158 |
. . . . . . . . . . . . . . . . 17
b0 b0 b2 |
76 | 74, 75 | le2an 169 |
. . . . . . . . . . . . . . . 16
a0 b0 a0 a2 b0 b2 |
77 | 49 | cm 61 |
. . . . . . . . . . . . . . . 16
a0
a2
b0 b2 c1 |
78 | 76, 77 | lbtr 139 |
. . . . . . . . . . . . . . 15
a0 b0 c1 |
79 | 78 | lerr 150 |
. . . . . . . . . . . . . 14
a0 b0 c0 c1 |
80 | 73, 79 | ler2an 173 |
. . . . . . . . . . . . 13
a0 b0 c2 c0 c1 |
81 | 80 | df-le2 131 |
. . . . . . . . . . . 12
a0
b0
c2 c0 c1 c2 c0 c1 |
82 | 81 | lor 70 |
. . . . . . . . . . 11
b1 a0 b0 c2 c0 c1 b1 c2 c0 c1 |
83 | 66, 67, 82 | 3tr 65 |
. . . . . . . . . 10
a0 b0
b1 c2 c0 c1 b1 c2 c0
c1 |
84 | 83 | lan 77 |
. . . . . . . . 9
b0 a0
b0
b1 c2 c0 c1 b0 b1 c2 c0
c1 |
85 | 71 | ran 78 |
. . . . . . . . . . . . . 14
c2 c0 c1 a0 a1 b0 b1 c0
c1 |
86 | | an32 83 |
. . . . . . . . . . . . . 14
a0 a1
b0 b1 c0 c1 a0
a1
c0 c1 b0 b1 |
87 | 85, 86 | tr 62 |
. . . . . . . . . . . . 13
c2 c0 c1 a0 a1 c0 c1 b0
b1 |
88 | 87 | lor 70 |
. . . . . . . . . . . 12
b1 c2 c0 c1 b1 a0 a1 c0 c1 b0
b1 |
89 | | leor 159 |
. . . . . . . . . . . . 13
b1 b0 b1 |
90 | 89 | ml2i 1123 |
. . . . . . . . . . . 12
b1 a0
a1
c0 c1 b0 b1 b1
a0 a1
c0 c1 b0 b1 |
91 | | ancom 74 |
. . . . . . . . . . . 12
b1
a0 a1
c0 c1 b0 b1 b0 b1 b1 a0 a1
c0 c1 |
92 | 88, 90, 91 | 3tr 65 |
. . . . . . . . . . 11
b1 c2 c0 c1 b0 b1 b1 a0 a1
c0 c1 |
93 | 92 | lan 77 |
. . . . . . . . . 10
b0 b1 c2 c0
c1 b0 b0 b1 b1 a0 a1
c0 c1 |
94 | | anass 76 |
. . . . . . . . . . 11
b0
b0 b1 b1 a0 a1 c0 c1 b0 b0 b1 b1 a0 a1
c0 c1 |
95 | 94 | cm 61 |
. . . . . . . . . 10
b0 b0 b1 b1 a0 a1
c0 c1 b0 b0 b1 b1
a0 a1
c0 c1 |
96 | | anabs 121 |
. . . . . . . . . . 11
b0 b0 b1 b0 |
97 | 96 | ran 78 |
. . . . . . . . . 10
b0
b0 b1 b1 a0 a1 c0 c1 b0 b1 a0 a1
c0 c1 |
98 | 93, 95, 97 | 3tr 65 |
. . . . . . . . 9
b0 b1 c2 c0
c1 b0 b1 a0 a1
c0 c1 |
99 | 84, 98 | tr 62 |
. . . . . . . 8
b0 a0
b0
b1 c2 c0 c1 b0 b1 a0 a1
c0 c1 |
100 | 99 | cm 61 |
. . . . . . 7
b0 b1 a0 a1
c0 c1 b0
a0 b0 b1
c2 c0 c1 |
101 | 65, 100 | lbtr 139 |
. . . . . 6
b0 a0 p0 b0 a0
b0
b1 c2 c0 c1 |
102 | | orass 75 |
. . . . . . . . . 10
a0 b0
b1 c2 c0 c1 a0 b0 b1 c2 c0
c1 |
103 | | orcom 73 |
. . . . . . . . . 10
a0
b0
b1 c2 c0 c1 b1 c2 c0 c1 a0 b0 |
104 | 102, 103 | tr 62 |
. . . . . . . . 9
a0 b0
b1 c2 c0 c1 b1 c2 c0 c1 a0 b0 |
105 | 104 | lan 77 |
. . . . . . . 8
b0 a0
b0
b1 c2 c0 c1 b0 b1 c2 c0 c1 a0 b0 |
106 | | lear 161 |
. . . . . . . . 9
a0 b0 b0 |
107 | 106 | mldual2i 1125 |
. . . . . . . 8
b0 b1 c2 c0 c1 a0 b0 b0 b1 c2 c0
c1 a0 b0 |
108 | | orcom 73 |
. . . . . . . 8
b0
b1 c2 c0 c1 a0 b0 a0 b0 b0 b1 c2
c0 c1 |
109 | 105, 107,
108 | 3tr 65 |
. . . . . . 7
b0 a0
b0
b1 c2 c0 c1 a0 b0 b0 b1 c2
c0 c1 |
110 | | lea 160 |
. . . . . . . 8
a0 b0 a0 |
111 | 110 | leror 152 |
. . . . . . 7
a0
b0
b0 b1 c2 c0
c1 a0 b0 b1 c2
c0 c1 |
112 | 109, 111 | bltr 138 |
. . . . . 6
b0 a0
b0
b1 c2 c0 c1 a0 b0 b1 c2
c0 c1 |
113 | 101, 112 | letr 137 |
. . . . 5
b0 a0 p0 a0 b0 b1 c2
c0 c1 |
114 | 113 | df-le2 131 |
. . . 4
b0
a0 p0 a0 b0 b1 c2
c0 c1 a0 b0 b1 c2
c0 c1 |
115 | 23, 114 | lbtr 139 |
. . 3
a0 b0
b1 c2 c0 c1 |
116 | 2, 115 | lel2or 170 |
. 2
a0 a0 b0 b1
c2 c0 c1 |
117 | 1, 116 | letr 137 |
1
a0 b0
b1 c2 c0 c1 |