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

---

Theorem dp15lema 1152

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

Hypotheses

Ref	Expression
dp15lema.1	a2 a0 a1 b1
dp15lema.2	p0 a1 b1 a2 b2
dp15lema.3	b0 a0 p0

Assertion

Ref	Expression
dp15lema	a0 a1 b1 b2

---

Proof of Theorem dp15lema

Step	Hyp	Ref	Expression
1		dp15lema.3	. . . . 5 b0 a0 p0
2		dp15lema.2	. . . . . . 7 p0 a1 b1 a2 b2
3	2	lor 70	. . . . . 6 a0 p0 a0 a1 b1 a2 b2
4	3	lan 77	. . . . 5 b0 a0 p0 b0 a0 a1 b1 a2 b2
5	1, 4	tr 62	. . . 4 b0 a0 a1 b1 a2 b2
6	5	lor 70	. . 3 a0 a0 b0 a0 a1 b1 a2 b2
7	6	ran 78	. 2 a0 a1 b1 a0 b0 a0 a1 b1 a2 b2 a1 b1
8		le1 146	. . . . . 6 b0
9	8	leran 153	. . . . 5 b0 a0 a1 b1 a2 b2 a0 a1 b1 a2 b2
10	9	lelor 166	. . . 4 a0 b0 a0 a1 b1 a2 b2 a0 a0 a1 b1 a2 b2
11	10	leran 153	. . 3 a0 b0 a0 a1 b1 a2 b2 a1 b1 a0 a0 a1 b1 a2 b2 a1 b1
12		an1r 107	. . . . . . . . 9 a0 a1 b1 a2 b2 a0 a1 b1 a2 b2
13	12	lor 70	. . . . . . . 8 a0 a0 a1 b1 a2 b2 a0 a0 a1 b1 a2 b2
14		orass 75	. . . . . . . . 9 a0 a0 a1 b1 a2 b2 a0 a0 a1 b1 a2 b2
15	14	cm 61	. . . . . . . 8 a0 a0 a1 b1 a2 b2 a0 a0 a1 b1 a2 b2
16		oridm 110	. . . . . . . . . 10 a0 a0 a0
17	16	ror 71	. . . . . . . . 9 a0 a0 a1 b1 a2 b2 a0 a1 b1 a2 b2
18		orcom 73	. . . . . . . . 9 a0 a1 b1 a2 b2 a1 b1 a2 b2 a0
19	17, 18	tr 62	. . . . . . . 8 a0 a0 a1 b1 a2 b2 a1 b1 a2 b2 a0
20	13, 15, 19	3tr 65	. . . . . . 7 a0 a0 a1 b1 a2 b2 a1 b1 a2 b2 a0
21	20	ran 78	. . . . . 6 a0 a0 a1 b1 a2 b2 a1 b1 a1 b1 a2 b2 a0 a1 b1
22		lea 160	. . . . . . 7 a1 b1 a2 b2 a1 b1
23	22	mlduali 1126	. . . . . 6 a1 b1 a2 b2 a0 a1 b1 a1 b1 a2 b2 a0 a1 b1
24	21, 23	tr 62	. . . . 5 a0 a0 a1 b1 a2 b2 a1 b1 a1 b1 a2 b2 a0 a1 b1
25		lear 161	. . . . . 6 a1 b1 a2 b2 a2 b2
26	25	leror 152	. . . . 5 a1 b1 a2 b2 a0 a1 b1 a2 b2 a0 a1 b1
27	24, 26	bltr 138	. . . 4 a0 a0 a1 b1 a2 b2 a1 b1 a2 b2 a0 a1 b1
28		or32 82	. . . . 5 a2 b2 a0 a1 b1 a2 a0 a1 b1 b2
29		dp15lema.1	. . . . . . 7 a2 a0 a1 b1
30	29	ror 71	. . . . . 6 b2 a2 a0 a1 b1 b2
31	30	cm 61	. . . . 5 a2 a0 a1 b1 b2 b2
32	28, 31	tr 62	. . . 4 a2 b2 a0 a1 b1 b2
33	27, 32	lbtr 139	. . 3 a0 a0 a1 b1 a2 b2 a1 b1 b2
34	11, 33	letr 137	. 2 a0 b0 a0 a1 b1 a2 b2 a1 b1 b2
35	7, 34	bltr 138	1 a0 a1 b1 b2

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

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:  dp15lemb  1153

Copyright terms: Public domain

W3C validator