lem3.3.5lem - Quantum Logic Explorer

	Quantum Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > QLE Home > Th. List > lem3.3.5lem		GIF version

Theorem lem3.3.5lem 1054

Description: A fundamental property in quantum logic. Lemma for lem3.3.5 1055.

**Hypothesis**
Ref	Expression
lem3.3.5lem.1	1 ≤ a

**Assertion**
Ref	Expression
lem3.3.5lem	a = 1

**Proof of Theorem lem3.3.5lem**
Step	Hyp	Ref	Expression
1		le1 146	. 2 a ≤ 1
2		lem3.3.5lem.1	. 2 1 ≤ a
3	1, 2	lebi 145	1 a = 1

Colors of variables: term

Syntax hints: = wb 1 ≤ wle 2 1wt 8

This theorem was proved from axioms: ax-a2 31 ax-a4 33 ax-r1 35 ax-r2 36 ax-r5 38

This theorem depends on definitions: df-t 41 df-le1 130 df-le2 131

This theorem is referenced by: lem3.3.5 1055 lem3.4.3 1076 lem4.6.6i1j3 1092