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

---

Theorem xxdp15 1200

Description: Part of proof (1)=>(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
xxdp15	a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1

---

Proof of Theorem xxdp15

Step	Hyp	Ref	Expression
1		xxdp.e	. . . . . . . . . . 11 b0 a0 p0
2		xxdp.p0	. . . . . . . . . . . . 13 p0 a1 b1 a2 b2
3	2	lor 70	. . . . . . . . . . . 12 a0 p0 a0 a1 b1 a2 b2
4	3	lan 77	. . . . . . . . . . 11 b0 a0 p0 b0 a0 a1 b1 a2 b2
5	1, 4	tr 62	. . . . . . . . . 10 b0 a0 a1 b1 a2 b2
6	5	lor 70	. . . . . . . . 9 a0 a0 b0 a0 a1 b1 a2 b2
7	6	ran 78	. . . . . . . 8 a0 a1 b1 a0 b0 a0 a1 b1 a2 b2 a1 b1
8		le1 146	. . . . . . . . . . . 12 b0
9	8	leran 153	. . . . . . . . . . 11 b0 a0 a1 b1 a2 b2 a0 a1 b1 a2 b2
10	9	lelor 166	. . . . . . . . . 10 a0 b0 a0 a1 b1 a2 b2 a0 a0 a1 b1 a2 b2
11	10	leran 153	. . . . . . . . 9 a0 b0 a0 a1 b1 a2 b2 a1 b1 a0 a0 a1 b1 a2 b2 a1 b1
12		an1r 107	. . . . . . . . . . . . . . 15 a0 a1 b1 a2 b2 a0 a1 b1 a2 b2
13	12	lor 70	. . . . . . . . . . . . . 14 a0 a0 a1 b1 a2 b2 a0 a0 a1 b1 a2 b2
14		orass 75	. . . . . . . . . . . . . . 15 a0 a0 a1 b1 a2 b2 a0 a0 a1 b1 a2 b2
15	14	cm 61	. . . . . . . . . . . . . 14 a0 a0 a1 b1 a2 b2 a0 a0 a1 b1 a2 b2
16		oridm 110	. . . . . . . . . . . . . . . 16 a0 a0 a0
17	16	ror 71	. . . . . . . . . . . . . . 15 a0 a0 a1 b1 a2 b2 a0 a1 b1 a2 b2
18		orcom 73	. . . . . . . . . . . . . . 15 a0 a1 b1 a2 b2 a1 b1 a2 b2 a0
19	17, 18	tr 62	. . . . . . . . . . . . . 14 a0 a0 a1 b1 a2 b2 a1 b1 a2 b2 a0
20	13, 15, 19	3tr 65	. . . . . . . . . . . . 13 a0 a0 a1 b1 a2 b2 a1 b1 a2 b2 a0
21	20	ran 78	. . . . . . . . . . . 12 a0 a0 a1 b1 a2 b2 a1 b1 a1 b1 a2 b2 a0 a1 b1
22		lea 160	. . . . . . . . . . . . 13 a1 b1 a2 b2 a1 b1
23	22	mlduali 1126	. . . . . . . . . . . 12 a1 b1 a2 b2 a0 a1 b1 a1 b1 a2 b2 a0 a1 b1
24	21, 23	tr 62	. . . . . . . . . . 11 a0 a0 a1 b1 a2 b2 a1 b1 a1 b1 a2 b2 a0 a1 b1
25		lear 161	. . . . . . . . . . . 12 a1 b1 a2 b2 a2 b2
26	25	leror 152	. . . . . . . . . . 11 a1 b1 a2 b2 a0 a1 b1 a2 b2 a0 a1 b1
27	24, 26	bltr 138	. . . . . . . . . 10 a0 a0 a1 b1 a2 b2 a1 b1 a2 b2 a0 a1 b1
28		or32 82	. . . . . . . . . . 11 a2 b2 a0 a1 b1 a2 a0 a1 b1 b2
29		xxdp.d	. . . . . . . . . . . . 13 a2 a0 a1 b1
30	29	ror 71	. . . . . . . . . . . 12 b2 a2 a0 a1 b1 b2
31	30	cm 61	. . . . . . . . . . 11 a2 a0 a1 b1 b2 b2
32	28, 31	tr 62	. . . . . . . . . 10 a2 b2 a0 a1 b1 b2
33	27, 32	lbtr 139	. . . . . . . . 9 a0 a0 a1 b1 a2 b2 a1 b1 b2
34	11, 33	letr 137	. . . . . . . 8 a0 b0 a0 a1 b1 a2 b2 a1 b1 b2
35	7, 34	bltr 138	. . . . . . 7 a0 a1 b1 b2
36	35	ax-arg 1151	. . . . . 6 a0 a1 b1 a0 b2 a1 b1 b2
37	1	ror 71	. . . . . . 7 b1 b0 a0 p0 b1
38	37	lan 77	. . . . . 6 a0 a1 b1 a0 a1 b0 a0 p0 b1
39	29	lor 70	. . . . . . . 8 a0 a0 a2 a0 a1 b1
40	1	ror 71	. . . . . . . 8 b2 b0 a0 p0 b2
41	39, 40	2an 79	. . . . . . 7 a0 b2 a0 a2 a0 a1 b1 b0 a0 p0 b2
42	29	lor 70	. . . . . . . 8 a1 a1 a2 a0 a1 b1
43	42	ran 78	. . . . . . 7 a1 b1 b2 a1 a2 a0 a1 b1 b1 b2
44	41, 43	2or 72	. . . . . 6 a0 b2 a1 b1 b2 a0 a2 a0 a1 b1 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2
45	36, 38, 44	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
46		or12 80	. . . . . . . 8 a0 a2 a0 a1 b1 a2 a0 a0 a1 b1
47		orabs 120	. . . . . . . . 9 a0 a0 a1 b1 a0
48	47	lor 70	. . . . . . . 8 a2 a0 a0 a1 b1 a2 a0
49		orcom 73	. . . . . . . 8 a2 a0 a0 a2
50	46, 48, 49	3tr 65	. . . . . . 7 a0 a2 a0 a1 b1 a0 a2
51	50	ran 78	. . . . . 6 a0 a2 a0 a1 b1 b0 a0 p0 b2 a0 a2 b0 a0 p0 b2
52		orass 75	. . . . . . . 8 a1 a2 a0 a1 b1 a1 a2 a0 a1 b1
53	52	ran 78	. . . . . . 7 a1 a2 a0 a1 b1 b1 b2 a1 a2 a0 a1 b1 b1 b2
54	53	cm 61	. . . . . 6 a1 a2 a0 a1 b1 b1 b2 a1 a2 a0 a1 b1 b1 b2
55	51, 54	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
56	45, 55	lbtr 139	. . . 4 a0 a1 b0 a0 p0 b1 a0 a2 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2
57		ax-a2 31	. . . . . . . . . 10 a1 a2 a2 a1
58		ax-a2 31	. . . . . . . . . . 11 a1 b1 b1 a1
59	58	lan 77	. . . . . . . . . 10 a0 a1 b1 a0 b1 a1
60	57, 59	2or 72	. . . . . . . . 9 a1 a2 a0 a1 b1 a2 a1 a0 b1 a1
61		orass 75	. . . . . . . . 9 a2 a1 a0 b1 a1 a2 a1 a0 b1 a1
62	60, 61	tr 62	. . . . . . . 8 a1 a2 a0 a1 b1 a2 a1 a0 b1 a1
63		ml3le 1127	. . . . . . . . 9 a1 a0 b1 a1 a1 b1 a0 a1
64	63	lelor 166	. . . . . . . 8 a2 a1 a0 b1 a1 a2 a1 b1 a0 a1
65	62, 64	bltr 138	. . . . . . 7 a1 a2 a0 a1 b1 a2 a1 b1 a0 a1
66		orass 75	. . . . . . . . 9 a2 a1 b1 a0 a1 a2 a1 b1 a0 a1
67	66	cm 61	. . . . . . . 8 a2 a1 b1 a0 a1 a2 a1 b1 a0 a1
68		ax-a2 31	. . . . . . . . 9 a2 a1 a1 a2
69	68	ror 71	. . . . . . . 8 a2 a1 b1 a0 a1 a1 a2 b1 a0 a1
70	67, 69	tr 62	. . . . . . 7 a2 a1 b1 a0 a1 a1 a2 b1 a0 a1
71	65, 70	lbtr 139	. . . . . 6 a1 a2 a0 a1 b1 a1 a2 b1 a0 a1
72	71	leran 153	. . . . 5 a1 a2 a0 a1 b1 b1 b2 a1 a2 b1 a0 a1 b1 b2
73	72	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
74	56, 73	letr 137	. . 3 a0 a1 b0 a0 p0 b1 a0 a2 b0 a0 p0 b2 a1 a2 b1 a0 a1 b1 b2
75		lea 160	. . . . . . 7 b0 a0 p0 b0
76	75	leror 152	. . . . . 6 b0 a0 p0 b2 b0 b2
77	76	lelan 167	. . . . 5 a0 a2 b0 a0 p0 b2 a0 a2 b0 b2
78		leao1 162	. . . . . . . 8 b1 a0 a1 b1 b2
79	78	mldual2i 1125	. . . . . . 7 b1 b2 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 a0 a1
80		ancom 74	. . . . . . 7 b1 b2 a1 a2 b1 a0 a1 a1 a2 b1 a0 a1 b1 b2
81		ancom 74	. . . . . . . 8 b1 b2 a1 a2 a1 a2 b1 b2
82	81	ror 71	. . . . . . 7 b1 b2 a1 a2 b1 a0 a1 a1 a2 b1 b2 b1 a0 a1
83	79, 80, 82	3tr2 64	. . . . . 6 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 b2 b1 a0 a1
84	83	bile 142	. . . . 5 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 b2 b1 a0 a1
85	77, 84	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
86		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
87	85, 86	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
88	74, 87	letr 137	. 2 a0 a1 b0 a0 p0 b1 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1
89		xxdp.c0	. . . . 5 c0 a1 a2 b1 b2
90		xxdp.c1	. . . . . 6 c1 a0 a2 b0 b2
91	90	ror 71	. . . . 5 c1 b1 a0 a1 a0 a2 b0 b2 b1 a0 a1
92	89, 91	2or 72	. . . 4 c0 c1 b1 a0 a1 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1
93	92	cm 61	. . 3 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1 c0 c1 b1 a0 a1
94		orass 75	. . . 4 c0 c1 b1 a0 a1 c0 c1 b1 a0 a1
95	94	cm 61	. . 3 c0 c1 b1 a0 a1 c0 c1 b1 a0 a1
96	93, 95	tr 62	. 2 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1 c0 c1 b1 a0 a1
97	88, 96	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