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

---

Theorem xdp41 1196

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

Hypotheses

Ref	Expression
xdp41.c0	c0 a1 a2 b1 b2
xdp41.c1	c1 a0 a2 b0 b2
xdp41.c2	c2 a0 a1 b0 b1
xdp41.p	a0 b0 a1 b1 a2 b2
xdp41.p2	p2 a0 b0 a1 b1
xdp41.1	p2 a2 b2

Assertion

Ref	Expression
xdp41	c2 c0 c1

---

Proof of Theorem xdp41

Step	Hyp	Ref	Expression
1		xdp41.c2	. . . . . . . . . . . 12 c2 a0 a1 b0 b1
2		ancom 74	. . . . . . . . . . . 12 a0 a1 b0 b1 b0 b1 a0 a1
3	1, 2	tr 62	. . . . . . . . . . 11 c2 b0 b1 a0 a1
4		leor 159	. . . . . . . . . . . . 13 b0 a0 b0
5	4	leror 152	. . . . . . . . . . . 12 b0 b1 a0 b0 b1
6		leo 158	. . . . . . . . . . . 12 a0 a1 a0 a1 b1
7	5, 6	le2an 169	. . . . . . . . . . 11 b0 b1 a0 a1 a0 b0 b1 a0 a1 b1
8	3, 7	bltr 138	. . . . . . . . . 10 c2 a0 b0 b1 a0 a1 b1
9	8	df2le2 136	. . . . . . . . 9 c2 a0 b0 b1 a0 a1 b1 c2
10	9	cm 61	. . . . . . . 8 c2 c2 a0 b0 b1 a0 a1 b1
11		anass 76	. . . . . . . . 9 c2 a0 b0 b1 a0 a1 b1 c2 a0 b0 b1 a0 a1 b1
12	11	cm 61	. . . . . . . 8 c2 a0 b0 b1 a0 a1 b1 c2 a0 b0 b1 a0 a1 b1
13	10, 12	tr 62	. . . . . . 7 c2 c2 a0 b0 b1 a0 a1 b1
14		ax-a2 31	. . . . . . . . . . . . . . . 16 a0 a1 a1 a0
15	14	ror 71	. . . . . . . . . . . . . . 15 a0 a1 b1 a1 a0 b1
16		or32 82	. . . . . . . . . . . . . . 15 a1 a0 b1 a1 b1 a0
17	15, 16	tr 62	. . . . . . . . . . . . . 14 a0 a1 b1 a1 b1 a0
18	17	lan 77	. . . . . . . . . . . . 13 a0 b0 b1 a0 a1 b1 a0 b0 b1 a1 b1 a0
19		ancom 74	. . . . . . . . . . . . 13 a0 b0 b1 a1 b1 a0 a1 b1 a0 a0 b0 b1
20	18, 19	tr 62	. . . . . . . . . . . 12 a0 b0 b1 a0 a1 b1 a1 b1 a0 a0 b0 b1
21		leor 159	. . . . . . . . . . . . . 14 b1 a1 b1
22	21	ler 149	. . . . . . . . . . . . 13 b1 a1 b1 a0
23	22	mldual2i 1125	. . . . . . . . . . . 12 a1 b1 a0 a0 b0 b1 a1 b1 a0 a0 b0 b1
24		ancom 74	. . . . . . . . . . . . . 14 a1 b1 a0 a0 b0 a0 b0 a1 b1 a0
25		leo 158	. . . . . . . . . . . . . . 15 a0 a0 b0
26	25	mldual2i 1125	. . . . . . . . . . . . . 14 a0 b0 a1 b1 a0 a0 b0 a1 b1 a0
27	24, 26	tr 62	. . . . . . . . . . . . 13 a1 b1 a0 a0 b0 a0 b0 a1 b1 a0
28	27	ror 71	. . . . . . . . . . . 12 a1 b1 a0 a0 b0 b1 a0 b0 a1 b1 a0 b1
29	20, 23, 28	3tr 65	. . . . . . . . . . 11 a0 b0 b1 a0 a1 b1 a0 b0 a1 b1 a0 b1
30		orass 75	. . . . . . . . . . 11 a0 b0 a1 b1 a0 b1 a0 b0 a1 b1 a0 b1
31		orcom 73	. . . . . . . . . . 11 a0 b0 a1 b1 a0 b1 a0 b1 a0 b0 a1 b1
32	29, 30, 31	3tr 65	. . . . . . . . . 10 a0 b0 b1 a0 a1 b1 a0 b1 a0 b0 a1 b1
33		leo 158	. . . . . . . . . . 11 a0 b1 a0 b1 c2 c0 c1
34		xdp41.p2	. . . . . . . . . . . . . . . . 17 p2 a0 b0 a1 b1
35	34	cm 61	. . . . . . . . . . . . . . . 16 a0 b0 a1 b1 p2
36		xdp41.1	. . . . . . . . . . . . . . . 16 p2 a2 b2
37	35, 36	bltr 138	. . . . . . . . . . . . . . 15 a0 b0 a1 b1 a2 b2
38	37	df2le2 136	. . . . . . . . . . . . . 14 a0 b0 a1 b1 a2 b2 a0 b0 a1 b1
39	38	cm 61	. . . . . . . . . . . . 13 a0 b0 a1 b1 a0 b0 a1 b1 a2 b2
40		xdp41.p	. . . . . . . . . . . . . 14 a0 b0 a1 b1 a2 b2
41	40	cm 61	. . . . . . . . . . . . 13 a0 b0 a1 b1 a2 b2
42	39, 41	tr 62	. . . . . . . . . . . 12 a0 b0 a1 b1
43		xdp41.c0	. . . . . . . . . . . . 13 c0 a1 a2 b1 b2
44		xdp41.c1	. . . . . . . . . . . . 13 c1 a0 a2 b0 b2
45	43, 44, 1, 40	dp34 1179	. . . . . . . . . . . 12 a0 b1 c2 c0 c1
46	42, 45	bltr 138	. . . . . . . . . . 11 a0 b0 a1 b1 a0 b1 c2 c0 c1
47	33, 46	lel2or 170	. . . . . . . . . 10 a0 b1 a0 b0 a1 b1 a0 b1 c2 c0 c1
48	32, 47	bltr 138	. . . . . . . . 9 a0 b0 b1 a0 a1 b1 a0 b1 c2 c0 c1
49	48	lelan 167	. . . . . . . 8 c2 a0 b0 b1 a0 a1 b1 c2 a0 b1 c2 c0 c1
50	11, 49	bltr 138	. . . . . . 7 c2 a0 b0 b1 a0 a1 b1 c2 a0 b1 c2 c0 c1
51	13, 50	bltr 138	. . . . . 6 c2 c2 a0 b1 c2 c0 c1
52		mldual 1122	. . . . . . 7 c2 a0 b1 c2 c0 c1 c2 a0 b1 c2 c0 c1
53		ancom 74	. . . . . . . 8 c2 c0 c1 c0 c1 c2
54	53	lor 70	. . . . . . 7 c2 a0 b1 c2 c0 c1 c2 a0 b1 c0 c1 c2
55		lea 160	. . . . . . . . 9 c2 a0 b1 c2
56	55	ml2i 1123	. . . . . . . 8 c2 a0 b1 c0 c1 c2 c2 a0 b1 c0 c1 c2
57		ancom 74	. . . . . . . 8 c2 a0 b1 c0 c1 c2 c2 c2 a0 b1 c0 c1
58		ax-a2 31	. . . . . . . . 9 c2 a0 b1 c0 c1 c0 c1 c2 a0 b1
59	58	lan 77	. . . . . . . 8 c2 c2 a0 b1 c0 c1 c2 c0 c1 c2 a0 b1
60	56, 57, 59	3tr 65	. . . . . . 7 c2 a0 b1 c0 c1 c2 c2 c0 c1 c2 a0 b1
61	52, 54, 60	3tr 65	. . . . . 6 c2 a0 b1 c2 c0 c1 c2 c0 c1 c2 a0 b1
62	51, 61	lbtr 139	. . . . 5 c2 c2 c0 c1 c2 a0 b1
63		mldual 1122	. . . . . . 7 c2 c0 c1 c2 a0 b1 c2 c0 c1 c2 a0 b1
64	1	ran 78	. . . . . . . . 9 c2 a0 b1 a0 a1 b0 b1 a0 b1
65		anass 76	. . . . . . . . 9 a0 a1 b0 b1 a0 b1 a0 a1 b0 b1 a0 b1
66		leor 159	. . . . . . . . . . . . 13 b1 b0 b1
67	66	mldual2i 1125	. . . . . . . . . . . 12 b0 b1 a0 b1 b0 b1 a0 b1
68		orcom 73	. . . . . . . . . . . 12 b0 b1 a0 b1 b1 b0 b1 a0
69		ancom 74	. . . . . . . . . . . . 13 b0 b1 a0 a0 b0 b1
70	69	lor 70	. . . . . . . . . . . 12 b1 b0 b1 a0 b1 a0 b0 b1
71	67, 68, 70	3tr 65	. . . . . . . . . . 11 b0 b1 a0 b1 b1 a0 b0 b1
72	71	lan 77	. . . . . . . . . 10 a0 a1 b0 b1 a0 b1 a0 a1 b1 a0 b0 b1
73		leao1 162	. . . . . . . . . . 11 a0 b0 b1 a0 a1
74	73	mldual2i 1125	. . . . . . . . . 10 a0 a1 b1 a0 b0 b1 a0 a1 b1 a0 b0 b1
75		orcom 73	. . . . . . . . . . 11 a0 a1 b1 a0 b0 b1 a0 b0 b1 a0 a1 b1
76		ancom 74	. . . . . . . . . . . 12 a0 a1 b1 b1 a0 a1
77	76	lor 70	. . . . . . . . . . 11 a0 b0 b1 a0 a1 b1 a0 b0 b1 b1 a0 a1
78	75, 77	tr 62	. . . . . . . . . 10 a0 a1 b1 a0 b0 b1 a0 b0 b1 b1 a0 a1
79	72, 74, 78	3tr 65	. . . . . . . . 9 a0 a1 b0 b1 a0 b1 a0 b0 b1 b1 a0 a1
80	64, 65, 79	3tr 65	. . . . . . . 8 c2 a0 b1 a0 b0 b1 b1 a0 a1
81	80	lor 70	. . . . . . 7 c2 c0 c1 c2 a0 b1 c2 c0 c1 a0 b0 b1 b1 a0 a1
82	63, 81	tr 62	. . . . . 6 c2 c0 c1 c2 a0 b1 c2 c0 c1 a0 b0 b1 b1 a0 a1
83		lear 161	. . . . . . 7 c2 c0 c1 c0 c1
84	83	leror 152	. . . . . 6 c2 c0 c1 a0 b0 b1 b1 a0 a1 c0 c1 a0 b0 b1 b1 a0 a1
85	82, 84	bltr 138	. . . . 5 c2 c0 c1 c2 a0 b1 c0 c1 a0 b0 b1 b1 a0 a1
86	62, 85	letr 137	. . . 4 c2 c0 c1 a0 b0 b1 b1 a0 a1
87		orcom 73	. . . . . . 7 a0 b0 b1 b1 a0 a1 b1 a0 a1 a0 b0 b1
88	87	lor 70	. . . . . 6 c0 c1 a0 b0 b1 b1 a0 a1 c0 c1 b1 a0 a1 a0 b0 b1
89		or4 84	. . . . . . 7 c0 c1 b1 a0 a1 a0 b0 b1 c0 b1 a0 a1 c1 a0 b0 b1
90		ancom 74	. . . . . . . . . 10 a1 a2 b1 b2 b1 b2 a1 a2
91	43, 90	tr 62	. . . . . . . . 9 c0 b1 b2 a1 a2
92	91	ror 71	. . . . . . . 8 c0 b1 a0 a1 b1 b2 a1 a2 b1 a0 a1
93	44	ror 71	. . . . . . . 8 c1 a0 b0 b1 a0 a2 b0 b2 a0 b0 b1
94	92, 93	2or 72	. . . . . . 7 c0 b1 a0 a1 c1 a0 b0 b1 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1
95	89, 94	tr 62	. . . . . 6 c0 c1 b1 a0 a1 a0 b0 b1 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1
96		leao1 162	. . . . . . . 8 b1 a0 a1 b1 b2
97	96	mli 1124	. . . . . . 7 b1 b2 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 a0 a1
98		leao1 162	. . . . . . . 8 a0 b0 b1 a0 a2
99	98	mli 1124	. . . . . . 7 a0 a2 b0 b2 a0 b0 b1 a0 a2 b0 b2 a0 b0 b1
100	97, 99	2or 72	. . . . . 6 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1
101	88, 95, 100	3tr 65	. . . . 5 c0 c1 a0 b0 b1 b1 a0 a1 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1
102		or32 82	. . . . . . . 8 a1 a2 b1 a0 a1 a1 b1 a0 a1 a2
103		ml3 1128	. . . . . . . . . 10 a1 b1 a0 a1 a1 a0 b1 a1
104		orcom 73	. . . . . . . . . . . 12 b1 a1 a1 b1
105	104	lan 77	. . . . . . . . . . 11 a0 b1 a1 a0 a1 b1
106	105	lor 70	. . . . . . . . . 10 a1 a0 b1 a1 a1 a0 a1 b1
107	103, 106	tr 62	. . . . . . . . 9 a1 b1 a0 a1 a1 a0 a1 b1
108	107	ror 71	. . . . . . . 8 a1 b1 a0 a1 a2 a1 a0 a1 b1 a2
109		or32 82	. . . . . . . 8 a1 a0 a1 b1 a2 a1 a2 a0 a1 b1
110	102, 108, 109	3tr 65	. . . . . . 7 a1 a2 b1 a0 a1 a1 a2 a0 a1 b1
111	110	lan 77	. . . . . 6 b1 b2 a1 a2 b1 a0 a1 b1 b2 a1 a2 a0 a1 b1
112		or32 82	. . . . . . . 8 b0 b2 a0 b0 b1 b0 a0 b0 b1 b2
113		orcom 73	. . . . . . . . . . . 12 b0 b1 b1 b0
114	113	lan 77	. . . . . . . . . . 11 a0 b0 b1 a0 b1 b0
115	114	lor 70	. . . . . . . . . 10 b0 a0 b0 b1 b0 a0 b1 b0
116		ml3 1128	. . . . . . . . . 10 b0 a0 b1 b0 b0 b1 a0 b0
117	115, 116	tr 62	. . . . . . . . 9 b0 a0 b0 b1 b0 b1 a0 b0
118	117	ror 71	. . . . . . . 8 b0 a0 b0 b1 b2 b0 b1 a0 b0 b2
119		or32 82	. . . . . . . 8 b0 b1 a0 b0 b2 b0 b2 b1 a0 b0
120	112, 118, 119	3tr 65	. . . . . . 7 b0 b2 a0 b0 b1 b0 b2 b1 a0 b0
121	120	lan 77	. . . . . 6 a0 a2 b0 b2 a0 b0 b1 a0 a2 b0 b2 b1 a0 b0
122	111, 121	2or 72	. . . . 5 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1 b1 b2 a1 a2 a0 a1 b1 a0 a2 b0 b2 b1 a0 b0
123	101, 122	tr 62	. . . 4 c0 c1 a0 b0 b1 b1 a0 a1 b1 b2 a1 a2 a0 a1 b1 a0 a2 b0 b2 b1 a0 b0
124	86, 123	lbtr 139	. . 3 c2 b1 b2 a1 a2 a0 a1 b1 a0 a2 b0 b2 b1 a0 b0
125		lea 160	. . . . . . 7 a0 a1 b1 a0
126	25	leran 153	. . . . . . . 8 a0 a1 b1 a0 b0 a1 b1
127	126, 37	letr 137	. . . . . . 7 a0 a1 b1 a2 b2
128	125, 127	ler2an 173	. . . . . 6 a0 a1 b1 a0 a2 b2
129	128	lelor 166	. . . . 5 a1 a2 a0 a1 b1 a1 a2 a0 a2 b2
130	129	lelan 167	. . . 4 b1 b2 a1 a2 a0 a1 b1 b1 b2 a1 a2 a0 a2 b2
131		lea 160	. . . . . . 7 b1 a0 b0 b1
132		lear 161	. . . . . . . . 9 b1 a0 b0 a0 b0
133		leao3 164	. . . . . . . . 9 b1 a0 b0 a1 b1
134	132, 133	ler2an 173	. . . . . . . 8 b1 a0 b0 a0 b0 a1 b1
135	134, 37	letr 137	. . . . . . 7 b1 a0 b0 a2 b2
136	131, 135	ler2an 173	. . . . . 6 b1 a0 b0 b1 a2 b2
137	136	lelor 166	. . . . 5 b0 b2 b1 a0 b0 b0 b2 b1 a2 b2
138	137	lelan 167	. . . 4 a0 a2 b0 b2 b1 a0 b0 a0 a2 b0 b2 b1 a2 b2
139	130, 138	le2or 168	. . 3 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
140	124, 139	letr 137	. 2 c2 b1 b2 a1 a2 a0 a2 b2 a0 a2 b0 b2 b1 a2 b2
141		ax-a2 31	. . . . . . . . . 10 a2 b2 b2 a2
142	141	lan 77	. . . . . . . . 9 a0 a2 b2 a0 b2 a2
143	142	lor 70	. . . . . . . 8 a2 a0 a2 b2 a2 a0 b2 a2
144		ml3 1128	. . . . . . . 8 a2 a0 b2 a2 a2 b2 a0 a2
145	143, 144	tr 62	. . . . . . 7 a2 a0 a2 b2 a2 b2 a0 a2
146	145	lor 70	. . . . . 6 a1 a2 a0 a2 b2 a1 a2 b2 a0 a2
147		orass 75	. . . . . 6 a1 a2 a0 a2 b2 a1 a2 a0 a2 b2
148		orass 75	. . . . . 6 a1 a2 b2 a0 a2 a1 a2 b2 a0 a2
149	146, 147, 148	3tr1 63	. . . . 5 a1 a2 a0 a2 b2 a1 a2 b2 a0 a2
150	149	lan 77	. . . 4 b1 b2 a1 a2 a0 a2 b2 b1 b2 a1 a2 b2 a0 a2
151		ml3 1128	. . . . . . 7 b2 b1 a2 b2 b2 a2 b1 b2
152	151	lor 70	. . . . . 6 b0 b2 b1 a2 b2 b0 b2 a2 b1 b2
153		orass 75	. . . . . 6 b0 b2 b1 a2 b2 b0 b2 b1 a2 b2
154		orass 75	. . . . . 6 b0 b2 a2 b1 b2 b0 b2 a2 b1 b2
155	152, 153, 154	3tr1 63	. . . . 5 b0 b2 b1 a2 b2 b0 b2 a2 b1 b2
156	155	lan 77	. . . 4 a0 a2 b0 b2 b1 a2 b2 a0 a2 b0 b2 a2 b1 b2
157	150, 156	2or 72	. . 3 b1 b2 a1 a2 a0 a2 b2 a0 a2 b0 b2 b1 a2 b2 b1 b2 a1 a2 b2 a0 a2 a0 a2 b0 b2 a2 b1 b2
158		leao3 164	. . . . . 6 b2 a0 a2 b1 b2
159	158	mldual2i 1125	. . . . 5 b1 b2 a1 a2 b2 a0 a2 b1 b2 a1 a2 b2 a0 a2
160	91	ror 71	. . . . . 6 c0 b2 a0 a2 b1 b2 a1 a2 b2 a0 a2
161	160	cm 61	. . . . 5 b1 b2 a1 a2 b2 a0 a2 c0 b2 a0 a2
162	159, 161	tr 62	. . . 4 b1 b2 a1 a2 b2 a0 a2 c0 b2 a0 a2
163		leao3 164	. . . . . 6 a2 b1 b2 a0 a2
164	163	mldual2i 1125	. . . . 5 a0 a2 b0 b2 a2 b1 b2 a0 a2 b0 b2 a2 b1 b2
165	44	ror 71	. . . . . 6 c1 a2 b1 b2 a0 a2 b0 b2 a2 b1 b2
166	165	cm 61	. . . . 5 a0 a2 b0 b2 a2 b1 b2 c1 a2 b1 b2
167	164, 166	tr 62	. . . 4 a0 a2 b0 b2 a2 b1 b2 c1 a2 b1 b2
168	162, 167	2or 72	. . 3 b1 b2 a1 a2 b2 a0 a2 a0 a2 b0 b2 a2 b1 b2 c0 b2 a0 a2 c1 a2 b1 b2
169		or4 84	. . . 4 c0 b2 a0 a2 c1 a2 b1 b2 c0 c1 b2 a0 a2 a2 b1 b2
170		orcom 73	. . . 4 c0 c1 b2 a0 a2 a2 b1 b2 b2 a0 a2 a2 b1 b2 c0 c1
171		ancom 74	. . . . . . . 8 b2 a0 a2 a0 a2 b2
172		leor 159	. . . . . . . . 9 b2 b0 b2
173	172	lelan 167	. . . . . . . 8 a0 a2 b2 a0 a2 b0 b2
174	171, 173	bltr 138	. . . . . . 7 b2 a0 a2 a0 a2 b0 b2
175		leor 159	. . . . . . . 8 a2 a1 a2
176	175	leran 153	. . . . . . 7 a2 b1 b2 a1 a2 b1 b2
177	174, 176	le2or 168	. . . . . 6 b2 a0 a2 a2 b1 b2 a0 a2 b0 b2 a1 a2 b1 b2
178	44, 43	2or 72	. . . . . . . 8 c1 c0 a0 a2 b0 b2 a1 a2 b1 b2
179	178	cm 61	. . . . . . 7 a0 a2 b0 b2 a1 a2 b1 b2 c1 c0
180		orcom 73	. . . . . . 7 c1 c0 c0 c1
181	179, 180	tr 62	. . . . . 6 a0 a2 b0 b2 a1 a2 b1 b2 c0 c1
182	177, 181	lbtr 139	. . . . 5 b2 a0 a2 a2 b1 b2 c0 c1
183	182	df-le2 131	. . . 4 b2 a0 a2 a2 b1 b2 c0 c1 c0 c1
184	169, 170, 183	3tr 65	. . 3 c0 b2 a0 a2 c1 a2 b1 b2 c0 c1
185	157, 168, 184	3tr 65	. 2 b1 b2 a1 a2 a0 a2 b2 a0 a2 b0 b2 b1 a2 b2 c0 c1
186	140, 185	lbtr 139	1 c2 c0 c1

Colors of variables: term

Syntax hints:   wb 1   wle 2   wo 6   wa 7

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