Quantum Logic Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  xdp45lem		Unicode version

---

Theorem xdp45lem 1202

Description: Part of proof (4)=>(5) in Day/Pickering 1982.

Hypotheses

Ref	Expression
xxdp.1	p2 a2 b2
xxdp.c0	c0 a1 a2 b1 b2
xxdp.c1	c1 a0 a2 b0 b2
xxdp.c2	c2 a0 a1 b0 b1
xxdp.d	a2 a0 a1 b1
xxdp.e	b0 a0 p0
xxdp.p	a0 b0 a1 b1 a2 b2
xxdp.p0	p0 a1 b1 a2 b2
xxdp.p2	p2 a0 b0 a1 b1

Assertion

Ref	Expression
xdp45lem	a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1

---

Proof of Theorem xdp45lem

Step	Hyp	Ref	Expression
1		ax-a2 31	. . . . . . . . . . . . . . . . . 18 a0 a1 a1 a0
2		ax-a2 31	. . . . . . . . . . . . . . . . . 18 b1 b1
3	1, 2	2an 79	. . . . . . . . . . . . . . . . 17 a0 a1 b1 a1 a0 b1
4		ancom 74	. . . . . . . . . . . . . . . . 17 a1 a0 b1 b1 a1 a0
5	3, 4	tr 62	. . . . . . . . . . . . . . . 16 a0 a1 b1 b1 a1 a0
6		leor 159	. . . . . . . . . . . . . . . . . 18 b1 a1 b1
7	6	leror 152	. . . . . . . . . . . . . . . . 17 b1 a1 b1
8		leo 158	. . . . . . . . . . . . . . . . 17 a1 a0 a1 a0
9	7, 8	le2an 169	. . . . . . . . . . . . . . . 16 b1 a1 a0 a1 b1 a1 a0
10	5, 9	bltr 138	. . . . . . . . . . . . . . 15 a0 a1 b1 a1 b1 a1 a0
11	10	df2le2 136	. . . . . . . . . . . . . 14 a0 a1 b1 a1 b1 a1 a0 a0 a1 b1
12	11	cm 61	. . . . . . . . . . . . 13 a0 a1 b1 a0 a1 b1 a1 b1 a1 a0
13		anass 76	. . . . . . . . . . . . . 14 a0 a1 b1 a1 b1 a1 a0 a0 a1 b1 a1 b1 a1 a0
14	13	cm 61	. . . . . . . . . . . . 13 a0 a1 b1 a1 b1 a1 a0 a0 a1 b1 a1 b1 a1 a0
15	12, 14	tr 62	. . . . . . . . . . . 12 a0 a1 b1 a0 a1 b1 a1 b1 a1 a0
16		ax-a2 31	. . . . . . . . . . . . . . . . . . . . 21 a1 a0 a0 a1
17	16	ror 71	. . . . . . . . . . . . . . . . . . . 20 a1 a0 a0 a1
18		or32 82	. . . . . . . . . . . . . . . . . . . 20 a0 a1 a0 a1
19	17, 18	tr 62	. . . . . . . . . . . . . . . . . . 19 a1 a0 a0 a1
20	19	lan 77	. . . . . . . . . . . . . . . . . 18 a1 b1 a1 a0 a1 b1 a0 a1
21		ancom 74	. . . . . . . . . . . . . . . . . 18 a1 b1 a0 a1 a0 a1 a1 b1
22	20, 21	tr 62	. . . . . . . . . . . . . . . . 17 a1 b1 a1 a0 a0 a1 a1 b1
23		leor 159	. . . . . . . . . . . . . . . . . . 19 a0
24	23	ler 149	. . . . . . . . . . . . . . . . . 18 a0 a1
25	24	mldual2i 1125	. . . . . . . . . . . . . . . . 17 a0 a1 a1 b1 a0 a1 a1 b1
26		ancom 74	. . . . . . . . . . . . . . . . . . 19 a0 a1 a1 b1 a1 b1 a0 a1
27		leo 158	. . . . . . . . . . . . . . . . . . . 20 a1 a1 b1
28	27	mldual2i 1125	. . . . . . . . . . . . . . . . . . 19 a1 b1 a0 a1 a1 b1 a0 a1
29	26, 28	tr 62	. . . . . . . . . . . . . . . . . 18 a0 a1 a1 b1 a1 b1 a0 a1
30	29	ror 71	. . . . . . . . . . . . . . . . 17 a0 a1 a1 b1 a1 b1 a0 a1
31	22, 25, 30	3tr 65	. . . . . . . . . . . . . . . 16 a1 b1 a1 a0 a1 b1 a0 a1
32		orass 75	. . . . . . . . . . . . . . . 16 a1 b1 a0 a1 a1 b1 a0 a1
33		orcom 73	. . . . . . . . . . . . . . . 16 a1 b1 a0 a1 a1 a1 b1 a0
34	31, 32, 33	3tr 65	. . . . . . . . . . . . . . 15 a1 b1 a1 a0 a1 a1 b1 a0
35		leo 158	. . . . . . . . . . . . . . . 16 a1 a1 a0 a1 b1 a0 b2 a1 b1 b2
36		ancom 74	. . . . . . . . . . . . . . . . . . . . . 22 a0 a1 b1 a1 b1 a0
37	36	cm 61	. . . . . . . . . . . . . . . . . . . . 21 a1 b1 a0 a0 a1 b1
38		xxdp.e	. . . . . . . . . . . . . . . . . . . . . . . . 25 b0 a0 p0
39		xxdp.p0	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 p0 a1 b1 a2 b2
40	39	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a0 p0 a0 a1 b1 a2 b2
41	40	lan 77	. . . . . . . . . . . . . . . . . . . . . . . . 25 b0 a0 p0 b0 a0 a1 b1 a2 b2
42	38, 41	tr 62	. . . . . . . . . . . . . . . . . . . . . . . 24 b0 a0 a1 b1 a2 b2
43	42	lor 70	. . . . . . . . . . . . . . . . . . . . . . 23 a0 a0 b0 a0 a1 b1 a2 b2
44	43	ran 78	. . . . . . . . . . . . . . . . . . . . . 22 a0 a1 b1 a0 b0 a0 a1 b1 a2 b2 a1 b1
45		le1 146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 b0
46	45	leran 153	. . . . . . . . . . . . . . . . . . . . . . . . 25 b0 a0 a1 b1 a2 b2 a0 a1 b1 a2 b2
47	46	lelor 166	. . . . . . . . . . . . . . . . . . . . . . . 24 a0 b0 a0 a1 b1 a2 b2 a0 a0 a1 b1 a2 b2
48	47	leran 153	. . . . . . . . . . . . . . . . . . . . . . 23 a0 b0 a0 a1 b1 a2 b2 a1 b1 a0 a0 a1 b1 a2 b2 a1 b1
49		an1r 107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a0 a1 b1 a2 b2 a0 a1 b1 a2 b2
50	49	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 a0 a1 b1 a2 b2 a0 a0 a1 b1 a2 b2
51		orass 75	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a0 a0 a1 b1 a2 b2 a0 a0 a1 b1 a2 b2
52	51	cm 61	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 a0 a1 b1 a2 b2 a0 a0 a1 b1 a2 b2
53		oridm 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 a0 a0 a0
54	53	ror 71	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a0 a0 a1 b1 a2 b2 a0 a1 b1 a2 b2
55		orcom 73	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 a0 a1 b1 a2 b2 a1 b1 a2 b2 a0
56	54, 55	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 a0 a0 a1 b1 a2 b2 a1 b1 a2 b2 a0
57	50, 52, 56	3tr 65	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a0 a0 a1 b1 a2 b2 a1 b1 a2 b2 a0
58	57	ran 78	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a0 a0 a1 b1 a2 b2 a1 b1 a1 b1 a2 b2 a0 a1 b1
59		lea 160	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a1 b1 a2 b2 a1 b1
60	59	mlduali 1126	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a1 b1 a2 b2 a0 a1 b1 a1 b1 a2 b2 a0 a1 b1
61	58, 60	tr 62	. . . . . . . . . . . . . . . . . . . . . . . . 25 a0 a0 a1 b1 a2 b2 a1 b1 a1 b1 a2 b2 a0 a1 b1
62		lear 161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a1 b1 a2 b2 a2 b2
63	62	leror 152	. . . . . . . . . . . . . . . . . . . . . . . . 25 a1 b1 a2 b2 a0 a1 b1 a2 b2 a0 a1 b1
64	61, 63	bltr 138	. . . . . . . . . . . . . . . . . . . . . . . 24 a0 a0 a1 b1 a2 b2 a1 b1 a2 b2 a0 a1 b1
65		or32 82	. . . . . . . . . . . . . . . . . . . . . . . . 25 a2 b2 a0 a1 b1 a2 a0 a1 b1 b2
66		xxdp.d	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 a2 a0 a1 b1
67	66	ror 71	. . . . . . . . . . . . . . . . . . . . . . . . . 26 b2 a2 a0 a1 b1 b2
68	67	cm 61	. . . . . . . . . . . . . . . . . . . . . . . . 25 a2 a0 a1 b1 b2 b2
69	65, 68	tr 62	. . . . . . . . . . . . . . . . . . . . . . . 24 a2 b2 a0 a1 b1 b2
70	64, 69	lbtr 139	. . . . . . . . . . . . . . . . . . . . . . 23 a0 a0 a1 b1 a2 b2 a1 b1 b2
71	48, 70	letr 137	. . . . . . . . . . . . . . . . . . . . . 22 a0 b0 a0 a1 b1 a2 b2 a1 b1 b2
72	44, 71	bltr 138	. . . . . . . . . . . . . . . . . . . . 21 a0 a1 b1 b2
73	37, 72	bltr 138	. . . . . . . . . . . . . . . . . . . 20 a1 b1 a0 b2
74	73	df2le2 136	. . . . . . . . . . . . . . . . . . 19 a1 b1 a0 b2 a1 b1 a0
75	74	cm 61	. . . . . . . . . . . . . . . . . 18 a1 b1 a0 a1 b1 a0 b2
76		id 59	. . . . . . . . . . . . . . . . . . 19 a1 b1 a0 b2 a1 b1 a0 b2
77	76	cm 61	. . . . . . . . . . . . . . . . . 18 a1 b1 a0 b2 a1 b1 a0 b2
78	75, 77	tr 62	. . . . . . . . . . . . . . . . 17 a1 b1 a0 a1 b1 a0 b2
79		id 59	. . . . . . . . . . . . . . . . . 18 a0 b2 a0 b2
80		id 59	. . . . . . . . . . . . . . . . . 18 a1 b1 b2 a1 b1 b2
81		orcom 73	. . . . . . . . . . . . . . . . . . 19 a0 a1 a1 a0
82		orcom 73	. . . . . . . . . . . . . . . . . . 19 b1 b1
83	81, 82	2an 79	. . . . . . . . . . . . . . . . . 18 a0 a1 b1 a1 a0 b1
84	79, 80, 83, 76	dp34 1179	. . . . . . . . . . . . . . . . 17 a1 b1 a0 b2 a1 a0 a1 b1 a0 b2 a1 b1 b2
85	78, 84	bltr 138	. . . . . . . . . . . . . . . 16 a1 b1 a0 a1 a0 a1 b1 a0 b2 a1 b1 b2
86	35, 85	lel2or 170	. . . . . . . . . . . . . . 15 a1 a1 b1 a0 a1 a0 a1 b1 a0 b2 a1 b1 b2
87	34, 86	bltr 138	. . . . . . . . . . . . . 14 a1 b1 a1 a0 a1 a0 a1 b1 a0 b2 a1 b1 b2
88	87	lelan 167	. . . . . . . . . . . . 13 a0 a1 b1 a1 b1 a1 a0 a0 a1 b1 a1 a0 a1 b1 a0 b2 a1 b1 b2
89	13, 88	bltr 138	. . . . . . . . . . . 12 a0 a1 b1 a1 b1 a1 a0 a0 a1 b1 a1 a0 a1 b1 a0 b2 a1 b1 b2
90	15, 89	bltr 138	. . . . . . . . . . 11 a0 a1 b1 a0 a1 b1 a1 a0 a1 b1 a0 b2 a1 b1 b2
91		mldual 1122	. . . . . . . . . . . 12 a0 a1 b1 a1 a0 a1 b1 a0 b2 a1 b1 b2 a0 a1 b1 a1 a0 a1 b1 a0 b2 a1 b1 b2
92		ancom 74	. . . . . . . . . . . . 13 a0 a1 b1 a0 b2 a1 b1 b2 a0 b2 a1 b1 b2 a0 a1 b1
93	92	lor 70	. . . . . . . . . . . 12 a0 a1 b1 a1 a0 a1 b1 a0 b2 a1 b1 b2 a0 a1 b1 a1 a0 b2 a1 b1 b2 a0 a1 b1
94		lea 160	. . . . . . . . . . . . . 14 a0 a1 b1 a1 a0 a1 b1
95	94	ml2i 1123	. . . . . . . . . . . . 13 a0 a1 b1 a1 a0 b2 a1 b1 b2 a0 a1 b1 a0 a1 b1 a1 a0 b2 a1 b1 b2 a0 a1 b1
96		ancom 74	. . . . . . . . . . . . 13 a0 a1 b1 a1 a0 b2 a1 b1 b2 a0 a1 b1 a0 a1 b1 a0 a1 b1 a1 a0 b2 a1 b1 b2
97		ax-a2 31	. . . . . . . . . . . . . 14 a0 a1 b1 a1 a0 b2 a1 b1 b2 a0 b2 a1 b1 b2 a0 a1 b1 a1
98	97	lan 77	. . . . . . . . . . . . 13 a0 a1 b1 a0 a1 b1 a1 a0 b2 a1 b1 b2 a0 a1 b1 a0 b2 a1 b1 b2 a0 a1 b1 a1
99	95, 96, 98	3tr 65	. . . . . . . . . . . 12 a0 a1 b1 a1 a0 b2 a1 b1 b2 a0 a1 b1 a0 a1 b1 a0 b2 a1 b1 b2 a0 a1 b1 a1
100	91, 93, 99	3tr 65	. . . . . . . . . . 11 a0 a1 b1 a1 a0 a1 b1 a0 b2 a1 b1 b2 a0 a1 b1 a0 b2 a1 b1 b2 a0 a1 b1 a1
101	90, 100	lbtr 139	. . . . . . . . . 10 a0 a1 b1 a0 a1 b1 a0 b2 a1 b1 b2 a0 a1 b1 a1
102		mldual 1122	. . . . . . . . . . . 12 a0 a1 b1 a0 b2 a1 b1 b2 a0 a1 b1 a1 a0 a1 b1 a0 b2 a1 b1 b2 a0 a1 b1 a1
103	3	ran 78	. . . . . . . . . . . . . 14 a0 a1 b1 a1 a1 a0 b1 a1
104		anass 76	. . . . . . . . . . . . . 14 a1 a0 b1 a1 a1 a0 b1 a1
105		leor 159	. . . . . . . . . . . . . . . . . 18 b1
106	105	mldual2i 1125	. . . . . . . . . . . . . . . . 17 b1 a1 b1 a1
107		orcom 73	. . . . . . . . . . . . . . . . 17 b1 a1 b1 a1
108		ancom 74	. . . . . . . . . . . . . . . . . 18 b1 a1 a1 b1
109	108	lor 70	. . . . . . . . . . . . . . . . 17 b1 a1 a1 b1
110	106, 107, 109	3tr 65	. . . . . . . . . . . . . . . 16 b1 a1 a1 b1
111	110	lan 77	. . . . . . . . . . . . . . 15 a1 a0 b1 a1 a1 a0 a1 b1
112		leao1 162	. . . . . . . . . . . . . . . 16 a1 b1 a1 a0
113	112	mldual2i 1125	. . . . . . . . . . . . . . 15 a1 a0 a1 b1 a1 a0 a1 b1
114		orcom 73	. . . . . . . . . . . . . . . 16 a1 a0 a1 b1 a1 b1 a1 a0
115		ancom 74	. . . . . . . . . . . . . . . . 17 a1 a0 a1 a0
116	115	lor 70	. . . . . . . . . . . . . . . 16 a1 b1 a1 a0 a1 b1 a1 a0
117	114, 116	tr 62	. . . . . . . . . . . . . . 15 a1 a0 a1 b1 a1 b1 a1 a0
118	111, 113, 117	3tr 65	. . . . . . . . . . . . . 14 a1 a0 b1 a1 a1 b1 a1 a0
119	103, 104, 118	3tr 65	. . . . . . . . . . . . 13 a0 a1 b1 a1 a1 b1 a1 a0
120	119	lor 70	. . . . . . . . . . . 12 a0 a1 b1 a0 b2 a1 b1 b2 a0 a1 b1 a1 a0 a1 b1 a0 b2 a1 b1 b2 a1 b1 a1 a0
121	102, 120	tr 62	. . . . . . . . . . 11 a0 a1 b1 a0 b2 a1 b1 b2 a0 a1 b1 a1 a0 a1 b1 a0 b2 a1 b1 b2 a1 b1 a1 a0
122		lear 161	. . . . . . . . . . . 12 a0 a1 b1 a0 b2 a1 b1 b2 a0 b2 a1 b1 b2
123	122	leror 152	. . . . . . . . . . 11 a0 a1 b1 a0 b2 a1 b1 b2 a1 b1 a1 a0 a0 b2 a1 b1 b2 a1 b1 a1 a0
124	121, 123	bltr 138	. . . . . . . . . 10 a0 a1 b1 a0 b2 a1 b1 b2 a0 a1 b1 a1 a0 b2 a1 b1 b2 a1 b1 a1 a0
125	101, 124	letr 137	. . . . . . . . 9 a0 a1 b1 a0 b2 a1 b1 b2 a1 b1 a1 a0
126		orcom 73	. . . . . . . . . . . 12 a1 b1 a1 a0 a1 a0 a1 b1
127	126	lor 70	. . . . . . . . . . 11 a0 b2 a1 b1 b2 a1 b1 a1 a0 a0 b2 a1 b1 b2 a1 a0 a1 b1
128		or4 84	. . . . . . . . . . . 12 a0 b2 a1 b1 b2 a1 a0 a1 b1 a0 b2 a1 a0 a1 b1 b2 a1 b1
129		ancom 74	. . . . . . . . . . . . . . 15 a0 b2 b2 a0
130	79, 129	tr 62	. . . . . . . . . . . . . 14 a0 b2 b2 a0
131	130	ror 71	. . . . . . . . . . . . 13 a0 b2 a1 a0 b2 a0 a1 a0
132	80	ror 71	. . . . . . . . . . . . 13 a1 b1 b2 a1 b1 a1 b1 b2 a1 b1
133	131, 132	2or 72	. . . . . . . . . . . 12 a0 b2 a1 a0 a1 b1 b2 a1 b1 b2 a0 a1 a0 a1 b1 b2 a1 b1
134	128, 133	tr 62	. . . . . . . . . . 11 a0 b2 a1 b1 b2 a1 a0 a1 b1 b2 a0 a1 a0 a1 b1 b2 a1 b1
135		leao1 162	. . . . . . . . . . . . 13 a1 a0 b2
136	135	mli 1124	. . . . . . . . . . . 12 b2 a0 a1 a0 b2 a0 a1 a0
137		leao1 162	. . . . . . . . . . . . 13 a1 b1 a1
138	137	mli 1124	. . . . . . . . . . . 12 a1 b1 b2 a1 b1 a1 b1 b2 a1 b1
139	136, 138	2or 72	. . . . . . . . . . 11 b2 a0 a1 a0 a1 b1 b2 a1 b1 b2 a0 a1 a0 a1 b1 b2 a1 b1
140	127, 134, 139	3tr 65	. . . . . . . . . 10 a0 b2 a1 b1 b2 a1 b1 a1 a0 b2 a0 a1 a0 a1 b1 b2 a1 b1
141		or32 82	. . . . . . . . . . . . 13 a0 a1 a0 a0 a1 a0
142		ml3 1128	. . . . . . . . . . . . . . 15 a0 a1 a0 a0 a1 a0
143		orcom 73	. . . . . . . . . . . . . . . . 17 a0 a0
144	143	lan 77	. . . . . . . . . . . . . . . 16 a1 a0 a1 a0
145	144	lor 70	. . . . . . . . . . . . . . 15 a0 a1 a0 a0 a1 a0
146	142, 145	tr 62	. . . . . . . . . . . . . 14 a0 a1 a0 a0 a1 a0
147	146	ror 71	. . . . . . . . . . . . 13 a0 a1 a0 a0 a1 a0
148		or32 82	. . . . . . . . . . . . 13 a0 a1 a0 a0 a1 a0
149	141, 147, 148	3tr 65	. . . . . . . . . . . 12 a0 a1 a0 a0 a1 a0
150	149	lan 77	. . . . . . . . . . 11 b2 a0 a1 a0 b2 a0 a1 a0
151		or32 82	. . . . . . . . . . . . 13 b1 b2 a1 b1 b1 a1 b1 b2
152		orcom 73	. . . . . . . . . . . . . . . . 17 b1 b1
153	152	lan 77	. . . . . . . . . . . . . . . 16 a1 b1 a1 b1
154	153	lor 70	. . . . . . . . . . . . . . 15 b1 a1 b1 b1 a1 b1
155		ml3 1128	. . . . . . . . . . . . . . 15 b1 a1 b1 b1 a1 b1
156	154, 155	tr 62	. . . . . . . . . . . . . 14 b1 a1 b1 b1 a1 b1
157	156	ror 71	. . . . . . . . . . . . 13 b1 a1 b1 b2 b1 a1 b1 b2
158		or32 82	. . . . . . . . . . . . 13 b1 a1 b1 b2 b1 b2 a1 b1
159	151, 157, 158	3tr 65	. . . . . . . . . . . 12 b1 b2 a1 b1 b1 b2 a1 b1
160	159	lan 77	. . . . . . . . . . 11 a1 b1 b2 a1 b1 a1 b1 b2 a1 b1
161	150, 160	2or 72	. . . . . . . . . 10 b2 a0 a1 a0 a1 b1 b2 a1 b1 b2 a0 a1 a0 a1 b1 b2 a1 b1
162	140, 161	tr 62	. . . . . . . . 9 a0 b2 a1 b1 b2 a1 b1 a1 a0 b2 a0 a1 a0 a1 b1 b2 a1 b1
163	125, 162	lbtr 139	. . . . . . . 8 a0 a1 b1 b2 a0 a1 a0 a1 b1 b2 a1 b1
164		lea 160	. . . . . . . . . . . 12 a1 a0 a1
165	27	leran 153	. . . . . . . . . . . . 13 a1 a0 a1 b1 a0
166	165, 73	letr 137	. . . . . . . . . . . 12 a1 a0 b2
167	164, 166	ler2an 173	. . . . . . . . . . 11 a1 a0 a1 b2
168	167	lelor 166	. . . . . . . . . 10 a0 a1 a0 a0 a1 b2
169	168	lelan 167	. . . . . . . . 9 b2 a0 a1 a0 b2 a0 a1 b2
170		lea 160	. . . . . . . . . . . 12 a1 b1
171		lear 161	. . . . . . . . . . . . . 14 a1 b1 a1 b1
172		leao3 164	. . . . . . . . . . . . . 14 a1 b1 a0
173	171, 172	ler2an 173	. . . . . . . . . . . . 13 a1 b1 a1 b1 a0
174	173, 73	letr 137	. . . . . . . . . . . 12 a1 b1 b2
175	170, 174	ler2an 173	. . . . . . . . . . 11 a1 b1 b2
176	175	lelor 166	. . . . . . . . . 10 b1 b2 a1 b1 b1 b2 b2
177	176	lelan 167	. . . . . . . . 9 a1 b1 b2 a1 b1 a1 b1 b2 b2
178	169, 177	le2or 168	. . . . . . . 8 b2 a0 a1 a0 a1 b1 b2 a1 b1 b2 a0 a1 b2 a1 b1 b2 b2
179	163, 178	letr 137	. . . . . . 7 a0 a1 b1 b2 a0 a1 b2 a1 b1 b2 b2
180		ax-a2 31	. . . . . . . . . . . . . . 15 b2 b2
181	180	lan 77	. . . . . . . . . . . . . 14 a1 b2 a1 b2
182	181	lor 70	. . . . . . . . . . . . 13 a1 b2 a1 b2
183		ml3 1128	. . . . . . . . . . . . 13 a1 b2 b2 a1
184	182, 183	tr 62	. . . . . . . . . . . 12 a1 b2 b2 a1
185	184	lor 70	. . . . . . . . . . 11 a0 a1 b2 a0 b2 a1
186		orass 75	. . . . . . . . . . 11 a0 a1 b2 a0 a1 b2
187		orass 75	. . . . . . . . . . 11 a0 b2 a1 a0 b2 a1
188	185, 186, 187	3tr1 63	. . . . . . . . . 10 a0 a1 b2 a0 b2 a1
189	188	lan 77	. . . . . . . . 9 b2 a0 a1 b2 b2 a0 b2 a1
190		ml3 1128	. . . . . . . . . . . 12 b2 b2 b2 b2
191	190	lor 70	. . . . . . . . . . 11 b1 b2 b2 b1 b2 b2
192		orass 75	. . . . . . . . . . 11 b1 b2 b2 b1 b2 b2
193		orass 75	. . . . . . . . . . 11 b1 b2 b2 b1 b2 b2
194	191, 192, 193	3tr1 63	. . . . . . . . . 10 b1 b2 b2 b1 b2 b2
195	194	lan 77	. . . . . . . . 9 a1 b1 b2 b2 a1 b1 b2 b2
196	189, 195	2or 72	. . . . . . . 8 b2 a0 a1 b2 a1 b1 b2 b2 b2 a0 b2 a1 a1 b1 b2 b2
197		leao3 164	. . . . . . . . . . 11 b2 a1 b2
198	197	mldual2i 1125	. . . . . . . . . 10 b2 a0 b2 a1 b2 a0 b2 a1
199	130	ror 71	. . . . . . . . . . 11 a0 b2 b2 a1 b2 a0 b2 a1
200	199	cm 61	. . . . . . . . . 10 b2 a0 b2 a1 a0 b2 b2 a1
201	198, 200	tr 62	. . . . . . . . 9 b2 a0 b2 a1 a0 b2 b2 a1
202		leao3 164	. . . . . . . . . . 11 b2 a1
203	202	mldual2i 1125	. . . . . . . . . 10 a1 b1 b2 b2 a1 b1 b2 b2
204	80	ror 71	. . . . . . . . . . 11 a1 b1 b2 b2 a1 b1 b2 b2
205	204	cm 61	. . . . . . . . . 10 a1 b1 b2 b2 a1 b1 b2 b2
206	203, 205	tr 62	. . . . . . . . 9 a1 b1 b2 b2 a1 b1 b2 b2
207	201, 206	2or 72	. . . . . . . 8 b2 a0 b2 a1 a1 b1 b2 b2 a0 b2 b2 a1 a1 b1 b2 b2
208		or4 84	. . . . . . . . 9 a0 b2 b2 a1 a1 b1 b2 b2 a0 b2 a1 b1 b2 b2 a1 b2
209		orcom 73	. . . . . . . . 9 a0 b2 a1 b1 b2 b2 a1 b2 b2 a1 b2 a0 b2 a1 b1 b2
210		ancom 74	. . . . . . . . . . . . 13 b2 a1 a1 b2
211		leor 159	. . . . . . . . . . . . . 14 b2 b1 b2
212	211	lelan 167	. . . . . . . . . . . . 13 a1 b2 a1 b1 b2
213	210, 212	bltr 138	. . . . . . . . . . . 12 b2 a1 a1 b1 b2
214		leor 159	. . . . . . . . . . . . 13 a0
215	214	leran 153	. . . . . . . . . . . 12 b2 a0 b2
216	213, 215	le2or 168	. . . . . . . . . . 11 b2 a1 b2 a1 b1 b2 a0 b2
217	80, 79	2or 72	. . . . . . . . . . . . 13 a1 b1 b2 a0 b2 a1 b1 b2 a0 b2
218	217	cm 61	. . . . . . . . . . . 12 a1 b1 b2 a0 b2 a1 b1 b2 a0 b2
219		orcom 73	. . . . . . . . . . . 12 a1 b1 b2 a0 b2 a0 b2 a1 b1 b2
220	218, 219	tr 62	. . . . . . . . . . 11 a1 b1 b2 a0 b2 a0 b2 a1 b1 b2
221	216, 220	lbtr 139	. . . . . . . . . 10 b2 a1 b2 a0 b2 a1 b1 b2
222	221	df-le2 131	. . . . . . . . 9 b2 a1 b2 a0 b2 a1 b1 b2 a0 b2 a1 b1 b2
223	208, 209, 222	3tr 65	. . . . . . . 8 a0 b2 b2 a1 a1 b1 b2 b2 a0 b2 a1 b1 b2
224	196, 207, 223	3tr 65	. . . . . . 7 b2 a0 a1 b2 a1 b1 b2 b2 a0 b2 a1 b1 b2
225	179, 224	lbtr 139	. . . . . 6 a0 a1 b1 a0 b2 a1 b1 b2
226	38	ror 71	. . . . . . 7 b1 b0 a0 p0 b1
227	226	lan 77	. . . . . 6 a0 a1 b1 a0 a1 b0 a0 p0 b1
228	66	lor 70	. . . . . . . 8 a0 a0 a2 a0 a1 b1
229	38	ror 71	. . . . . . . 8 b2 b0 a0 p0 b2
230	228, 229	2an 79	. . . . . . 7 a0 b2 a0 a2 a0 a1 b1 b0 a0 p0 b2
231	66	lor 70	. . . . . . . 8 a1 a1 a2 a0 a1 b1
232	231	ran 78	. . . . . . 7 a1 b1 b2 a1 a2 a0 a1 b1 b1 b2
233	230, 232	2or 72	. . . . . 6 a0 b2 a1 b1 b2 a0 a2 a0 a1 b1 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2
234	225, 227, 233	le3tr2 141	. . . . 5 a0 a1 b0 a0 p0 b1 a0 a2 a0 a1 b1 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2
235		or12 80	. . . . . . . 8 a0 a2 a0 a1 b1 a2 a0 a0 a1 b1
236		orabs 120	. . . . . . . . 9 a0 a0 a1 b1 a0
237	236	lor 70	. . . . . . . 8 a2 a0 a0 a1 b1 a2 a0
238		orcom 73	. . . . . . . 8 a2 a0 a0 a2
239	235, 237, 238	3tr 65	. . . . . . 7 a0 a2 a0 a1 b1 a0 a2
240	239	ran 78	. . . . . 6 a0 a2 a0 a1 b1 b0 a0 p0 b2 a0 a2 b0 a0 p0 b2
241		orass 75	. . . . . . . 8 a1 a2 a0 a1 b1 a1 a2 a0 a1 b1
242	241	ran 78	. . . . . . 7 a1 a2 a0 a1 b1 b1 b2 a1 a2 a0 a1 b1 b1 b2
243	242	cm 61	. . . . . 6 a1 a2 a0 a1 b1 b1 b2 a1 a2 a0 a1 b1 b1 b2
244	240, 243	2or 72	. . . . 5 a0 a2 a0 a1 b1 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2 a0 a2 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2
245	234, 244	lbtr 139	. . . 4 a0 a1 b0 a0 p0 b1 a0 a2 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2
246		ax-a2 31	. . . . . . . . . 10 a1 a2 a2 a1
247		ax-a2 31	. . . . . . . . . . 11 a1 b1 b1 a1
248	247	lan 77	. . . . . . . . . 10 a0 a1 b1 a0 b1 a1
249	246, 248	2or 72	. . . . . . . . 9 a1 a2 a0 a1 b1 a2 a1 a0 b1 a1
250		orass 75	. . . . . . . . 9 a2 a1 a0 b1 a1 a2 a1 a0 b1 a1
251	249, 250	tr 62	. . . . . . . 8 a1 a2 a0 a1 b1 a2 a1 a0 b1 a1
252		ml3le 1127	. . . . . . . . 9 a1 a0 b1 a1 a1 b1 a0 a1
253	252	lelor 166	. . . . . . . 8 a2 a1 a0 b1 a1 a2 a1 b1 a0 a1
254	251, 253	bltr 138	. . . . . . 7 a1 a2 a0 a1 b1 a2 a1 b1 a0 a1
255		orass 75	. . . . . . . . 9 a2 a1 b1 a0 a1 a2 a1 b1 a0 a1
256	255	cm 61	. . . . . . . 8 a2 a1 b1 a0 a1 a2 a1 b1 a0 a1
257		ax-a2 31	. . . . . . . . 9 a2 a1 a1 a2
258	257	ror 71	. . . . . . . 8 a2 a1 b1 a0 a1 a1 a2 b1 a0 a1
259	256, 258	tr 62	. . . . . . 7 a2 a1 b1 a0 a1 a1 a2 b1 a0 a1
260	254, 259	lbtr 139	. . . . . 6 a1 a2 a0 a1 b1 a1 a2 b1 a0 a1
261	260	leran 153	. . . . 5 a1 a2 a0 a1 b1 b1 b2 a1 a2 b1 a0 a1 b1 b2
262	261	lelor 166	. . . 4 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
263	245, 262	letr 137	. . 3 a0 a1 b0 a0 p0 b1 a0 a2 b0 a0 p0 b2 a1 a2 b1 a0 a1 b1 b2
264		lea 160	. . . . . . 7 b0 a0 p0 b0
265	264	leror 152	. . . . . 6 b0 a0 p0 b2 b0 b2
266	265	lelan 167	. . . . 5 a0 a2 b0 a0 p0 b2 a0 a2 b0 b2
267		leao1 162	. . . . . . . 8 b1 a0 a1 b1 b2
268	267	mldual2i 1125	. . . . . . 7 b1 b2 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 a0 a1
269		ancom 74	. . . . . . 7 b1 b2 a1 a2 b1 a0 a1 a1 a2 b1 a0 a1 b1 b2
270		ancom 74	. . . . . . . 8 b1 b2 a1 a2 a1 a2 b1 b2
271	270	ror 71	. . . . . . 7 b1 b2 a1 a2 b1 a0 a1 a1 a2 b1 b2 b1 a0 a1
272	268, 269, 271	3tr2 64	. . . . . 6 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 b2 b1 a0 a1
273	272	bile 142	. . . . 5 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 b2 b1 a0 a1
274	266, 273	le2or 168	. . . 4 a0 a2 b0 a0 p0 b2 a1 a2 b1 a0 a1 b1 b2 a0 a2 b0 b2 a1 a2 b1 b2 b1 a0 a1
275		or12 80	. . . 4 a0 a2 b0 b2 a1 a2 b1 b2 b1 a0 a1 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1
276	274, 275	lbtr 139	. . 3 a0 a2 b0 a0 p0 b2 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1
277	263, 276	letr 137	. 2 a0 a1 b0 a0 p0 b1 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1
278		xxdp.c0	. . . . 5 c0 a1 a2 b1 b2
279		xxdp.c1	. . . . . 6 c1 a0 a2 b0 b2
280	279	ror 71	. . . . 5 c1 b1 a0 a1 a0 a2 b0 b2 b1 a0 a1
281	278, 280	2or 72	. . . 4 c0 c1 b1 a0 a1 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1
282	281	cm 61	. . 3 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1 c0 c1 b1 a0 a1
283		orass 75	. . . 4 c0 c1 b1 a0 a1 c0 c1 b1 a0 a1
284	283	cm 61	. . 3 c0 c1 b1 a0 a1 c0 c1 b1 a0 a1
285	282, 284	tr 62	. 2 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1 c0 c1 b1 a0 a1
286	277, 285	lbtr 139	1 a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1

Colors of variables: term

Syntax hints:   wb 1   wle 2   wo 6   wa 7  wt 8

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-ml 1120  ax-arg 1151

This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator