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

---

Theorem dp41lemh 1188

Description: Part of proof (4)=>(1) in Day/Pickering 1982. "By CP(a,b)".

Hypotheses

Ref	Expression
dp41lem.1	c0 a1 a2 b1 b2
dp41lem.2	c1 a0 a2 b0 b2
dp41lem.3	c2 a0 a1 b0 b1
dp41lem.4	a0 b0 a1 b1 a2 b2
dp41lem.5	p2 a0 b0 a1 b1
dp41lem.6	p2 a2 b2

Assertion

Ref	Expression
dp41lemh	b1 b2 a1 a2 a0 a1 b1 a0 a2 b0 b2 b1 a0 b0 b1 b2 a1 a2 a0 a2 b2 a0 a2 b0 b2 b1 a2 b2

---

Proof of Theorem dp41lemh

Step	Hyp	Ref	Expression
1		lea 160	. . . . 5 a0 a1 b1 a0
2		leo 158	. . . . . . 7 a0 a0 b0
3	2	leran 153	. . . . . 6 a0 a1 b1 a0 b0 a1 b1
4		dp41lem.5	. . . . . . . 8 p2 a0 b0 a1 b1
5	4	cm 61	. . . . . . 7 a0 b0 a1 b1 p2
6		dp41lem.6	. . . . . . 7 p2 a2 b2
7	5, 6	bltr 138	. . . . . 6 a0 b0 a1 b1 a2 b2
8	3, 7	letr 137	. . . . 5 a0 a1 b1 a2 b2
9	1, 8	ler2an 173	. . . 4 a0 a1 b1 a0 a2 b2
10	9	lelor 166	. . 3 a1 a2 a0 a1 b1 a1 a2 a0 a2 b2
11	10	lelan 167	. 2 b1 b2 a1 a2 a0 a1 b1 b1 b2 a1 a2 a0 a2 b2
12		lea 160	. . . . 5 b1 a0 b0 b1
13		lear 161	. . . . . . 7 b1 a0 b0 a0 b0
14		leao3 164	. . . . . . 7 b1 a0 b0 a1 b1
15	13, 14	ler2an 173	. . . . . 6 b1 a0 b0 a0 b0 a1 b1
16	15, 7	letr 137	. . . . 5 b1 a0 b0 a2 b2
17	12, 16	ler2an 173	. . . 4 b1 a0 b0 b1 a2 b2
18	17	lelor 166	. . 3 b0 b2 b1 a0 b0 b0 b2 b1 a2 b2
19	18	lelan 167	. 2 a0 a2 b0 b2 b1 a0 b0 a0 a2 b0 b2 b1 a2 b2
20	11, 19	le2or 168	1 b1 b2 a1 a2 a0 a1 b1 a0 a2 b0 b2 b1 a0 b0 b1 b2 a1 a2 a0 a2 b2 a0 a2 b0 b2 b1 a2 b2

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

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:  dp41lemm  1192

Copyright terms: Public domain

W3C validator