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

---

Theorem dp15lemf 1157

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
dp15lemf	a0 a2 b0 a0 p0 b2 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1

---

Proof of Theorem dp15lemf

Step	Hyp	Ref	Expression
1		lea 160	. . . . 5 b0 a0 p0 b0
2	1	leror 152	. . . 4 b0 a0 p0 b2 b0 b2
3	2	lelan 167	. . 3 a0 a2 b0 a0 p0 b2 a0 a2 b0 b2
4		leao1 162	. . . . . 6 b1 a0 a1 b1 b2
5	4	mldual2i 1125	. . . . 5 b1 b2 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 a0 a1
6		ancom 74	. . . . 5 b1 b2 a1 a2 b1 a0 a1 a1 a2 b1 a0 a1 b1 b2
7		ancom 74	. . . . . 6 b1 b2 a1 a2 a1 a2 b1 b2
8	7	ror 71	. . . . 5 b1 b2 a1 a2 b1 a0 a1 a1 a2 b1 b2 b1 a0 a1
9	5, 6, 8	3tr2 64	. . . 4 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 b2 b1 a0 a1
10	9	bile 142	. . 3 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 b2 b1 a0 a1
11	3, 10	le2or 168	. 2 a0 a2 b0 a0 p0 b2 a1 a2 b1 a0 a1 b1 b2 a0 a2 b0 b2 a1 a2 b1 b2 b1 a0 a1
12		or12 80	. 2 a0 a2 b0 b2 a1 a2 b1 b2 b1 a0 a1 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1
13	11, 12	lbtr 139	1 a0 a2 b0 a0 p0 b2 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1

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-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:  dp15lemh  1159

Copyright terms: Public domain

W3C validator