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

---

Theorem dp53lema 1161

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

Hypotheses

Ref	Expression
dp53lem.1	c0 a1 a2 b1 b2
dp53lem.2	c1 a0 a2 b0 b2
dp53lem.3	c2 a0 a1 b0 b1
dp53lem.4	p0 a1 b1 a2 b2
dp53lem.5	a0 b0 a1 b1 a2 b2

Assertion

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

---

Proof of Theorem dp53lema

Step	Hyp	Ref	Expression
1		leo 158	. 2 b1 b1 a0 a1 c0 c1
2		leo 158	. . . . . 6 b0 a0 p0 b0 a0 p0 b1
3		dp53lem.4	. . . . . . . . 9 p0 a1 b1 a2 b2
4	3	lor 70	. . . . . . . 8 a0 p0 a0 a1 b1 a2 b2
5	4	lan 77	. . . . . . 7 b0 a0 p0 b0 a0 a1 b1 a2 b2
6		lear 161	. . . . . . . 8 b0 a0 a1 b1 a2 b2 a0 a1 b1 a2 b2
7		lea 160	. . . . . . . . . 10 a1 b1 a2 b2 a1 b1
8	7	lelor 166	. . . . . . . . 9 a0 a1 b1 a2 b2 a0 a1 b1
9		ax-a3 32	. . . . . . . . . 10 a0 a1 b1 a0 a1 b1
10	9	cm 61	. . . . . . . . 9 a0 a1 b1 a0 a1 b1
11	8, 10	lbtr 139	. . . . . . . 8 a0 a1 b1 a2 b2 a0 a1 b1
12	6, 11	letr 137	. . . . . . 7 b0 a0 a1 b1 a2 b2 a0 a1 b1
13	5, 12	bltr 138	. . . . . 6 b0 a0 p0 a0 a1 b1
14	2, 13	ler2an 173	. . . . 5 b0 a0 p0 b0 a0 p0 b1 a0 a1 b1
15		leor 159	. . . . . . 7 b1 b0 a0 p0 b1
16	15	mldual2i 1125	. . . . . 6 b0 a0 p0 b1 a0 a1 b1 b0 a0 p0 b1 a0 a1 b1
17		ancom 74	. . . . . . 7 b0 a0 p0 b1 a0 a1 a0 a1 b0 a0 p0 b1
18	17	ror 71	. . . . . 6 b0 a0 p0 b1 a0 a1 b1 a0 a1 b0 a0 p0 b1 b1
19	16, 18	tr 62	. . . . 5 b0 a0 p0 b1 a0 a1 b1 a0 a1 b0 a0 p0 b1 b1
20	14, 19	lbtr 139	. . . 4 b0 a0 p0 a0 a1 b0 a0 p0 b1 b1
21	1	lelor 166	. . . 4 a0 a1 b0 a0 p0 b1 b1 a0 a1 b0 a0 p0 b1 b1 a0 a1 c0 c1
22	20, 21	letr 137	. . 3 b0 a0 p0 a0 a1 b0 a0 p0 b1 b1 a0 a1 c0 c1
23		lea 160	. . . . . . . 8 a0 a1 b0 a0 p0 b1 a0 a1
24		dp53lem.1	. . . . . . . . 9 c0 a1 a2 b1 b2
25		dp53lem.2	. . . . . . . . 9 c1 a0 a2 b0 b2
26	24, 25, 3	dp15 1160	. . . . . . . 8 a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1
27	23, 26	ler2an 173	. . . . . . 7 a0 a1 b0 a0 p0 b1 a0 a1 c0 c1 b1 a0 a1
28		lear 161	. . . . . . . 8 b1 a0 a1 a0 a1
29	28	mldual2i 1125	. . . . . . 7 a0 a1 c0 c1 b1 a0 a1 a0 a1 c0 c1 b1 a0 a1
30	27, 29	lbtr 139	. . . . . 6 a0 a1 b0 a0 p0 b1 a0 a1 c0 c1 b1 a0 a1
31		lea 160	. . . . . . 7 b1 a0 a1 b1
32	31	lelor 166	. . . . . 6 a0 a1 c0 c1 b1 a0 a1 a0 a1 c0 c1 b1
33	30, 32	letr 137	. . . . 5 a0 a1 b0 a0 p0 b1 a0 a1 c0 c1 b1
34		orcom 73	. . . . 5 a0 a1 c0 c1 b1 b1 a0 a1 c0 c1
35	33, 34	lbtr 139	. . . 4 a0 a1 b0 a0 p0 b1 b1 a0 a1 c0 c1
36		leid 148	. . . 4 b1 a0 a1 c0 c1 b1 a0 a1 c0 c1
37	35, 36	lel2or 170	. . 3 a0 a1 b0 a0 p0 b1 b1 a0 a1 c0 c1 b1 a0 a1 c0 c1
38	22, 37	letr 137	. 2 b0 a0 p0 b1 a0 a1 c0 c1
39	1, 38	lel2or 170	1 b1 b0 a0 p0 b1 a0 a1 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:  dp53lemd  1164

Copyright terms: Public domain

W3C validator