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

Theorem id5leid0 351
Description: Quantum identity is less than classical identity. (Contributed by NM, 4-Mar-2006.)
Assertion
Ref Expression
id5leid0 (ab) ≤ (a0 b)

Proof of Theorem id5leid0
StepHypRef Expression
1 ax-a2 31 . . 3 ((ab) ∪ (ab )) = ((ab ) ∪ (ab))
2 lea 160 . . . . 5 (ab ) ≤ a
3 lear 161 . . . . 5 (ab) ≤ b
42, 3le2or 168 . . . 4 ((ab ) ∪ (ab)) ≤ (ab)
5 lear 161 . . . . 5 (ab ) ≤ b
6 lea 160 . . . . 5 (ab) ≤ a
75, 6le2or 168 . . . 4 ((ab ) ∪ (ab)) ≤ (ba)
84, 7ler2an 173 . . 3 ((ab ) ∪ (ab)) ≤ ((ab) ∩ (ba))
91, 8bltr 138 . 2 ((ab) ∪ (ab )) ≤ ((ab) ∩ (ba))
10 dfb 94 . 2 (ab) = ((ab) ∪ (ab ))
11 df-id0 49 . 2 (a0 b) = ((ab) ∩ (ba))
129, 10, 11le3tr1 140 1 (ab) ≤ (a0 b)
Colors of variables: term
Syntax hints:  wle 2   wn 4  tb 5  wo 6  wa 7  0 wid0 17
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-b 39  df-a 40  df-t 41  df-f 42  df-id0 49  df-le1 130  df-le2 131
This theorem is referenced by:  id5id0  352
  Copyright terms: Public domain W3C validator