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

---

Theorem xxdp53 1201

Description: Part of proof (5)=>(3) 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
xxdp53	a0 b0 b1 c2 c0 c1

---

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

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