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

Theorem neg3antlem2 865
Description: Lemma for negated antecedent identity. (Contributed by NM, 7-Aug-2001.)
Hypothesis
Ref Expression
neg3ant.1 (a3 c) = (b3 c)
Assertion
Ref Expression
neg3antlem2 a ≤ (b1 c)

Proof of Theorem neg3antlem2
StepHypRef Expression
1 leor 159 . . . . 5 (ac) ≤ ((ac) ∪ (ac))
2 neg3ant.1 . . . . . . 7 (a3 c) = (b3 c)
32ran 78 . . . . . 6 ((a3 c) ∩ c) = ((b3 c) ∩ c)
4 u3lemab 612 . . . . . 6 ((a3 c) ∩ c) = ((ac) ∪ (ac))
5 u3lemab 612 . . . . . 6 ((b3 c) ∩ c) = ((bc) ∪ (bc))
63, 4, 53tr2 64 . . . . 5 ((ac) ∪ (ac)) = ((bc) ∪ (bc))
71, 6lbtr 139 . . . 4 (ac) ≤ ((bc) ∪ (bc))
8 leor 159 . . . . 5 (bc) ≤ (b ∪ (bc))
9 leao1 162 . . . . 5 (bc) ≤ (b ∪ (bc))
108, 9lel2or 170 . . . 4 ((bc) ∪ (bc)) ≤ (b ∪ (bc))
117, 10letr 137 . . 3 (ac) ≤ (b ∪ (bc))
12 leor 159 . . . . . . . . . . . 12 (b ∩ (bc)) ≤ (((bc) ∪ (bc )) ∪ (b ∩ (bc)))
13 df-i3 46 . . . . . . . . . . . . . 14 (b3 c) = (((bc) ∪ (bc )) ∪ (b ∩ (bc)))
142, 13ax-r2 36 . . . . . . . . . . . . 13 (a3 c) = (((bc) ∪ (bc )) ∪ (b ∩ (bc)))
1514ax-r1 35 . . . . . . . . . . . 12 (((bc) ∪ (bc )) ∪ (b ∩ (bc))) = (a3 c)
1612, 15lbtr 139 . . . . . . . . . . 11 (b ∩ (bc)) ≤ (a3 c)
17 leao1 162 . . . . . . . . . . . 12 (b ∩ (bc)) ≤ (bc)
182ran 78 . . . . . . . . . . . . . . . 16 ((a3 c) ∩ c ) = ((b3 c) ∩ c )
19 u3lemanb 617 . . . . . . . . . . . . . . . 16 ((a3 c) ∩ c ) = (ac )
20 u3lemanb 617 . . . . . . . . . . . . . . . 16 ((b3 c) ∩ c ) = (bc )
2118, 19, 203tr2 64 . . . . . . . . . . . . . . 15 (ac ) = (bc )
22 anor3 90 . . . . . . . . . . . . . . 15 (ac ) = (ac)
23 anor3 90 . . . . . . . . . . . . . . 15 (bc ) = (bc)
2421, 22, 233tr2 64 . . . . . . . . . . . . . 14 (ac) = (bc)
2524con1 66 . . . . . . . . . . . . 13 (ac) = (bc)
2625ax-r1 35 . . . . . . . . . . . 12 (bc) = (ac)
2717, 26lbtr 139 . . . . . . . . . . 11 (b ∩ (bc)) ≤ (ac)
2816, 27ler2an 173 . . . . . . . . . 10 (b ∩ (bc)) ≤ ((a3 c) ∩ (ac))
29 u3lem15 795 . . . . . . . . . 10 ((a3 c) ∩ (ac)) = ((ac) ∩ (a ∪ (ac)))
3028, 29lbtr 139 . . . . . . . . 9 (b ∩ (bc)) ≤ ((ac) ∩ (a ∪ (ac)))
31 lear 161 . . . . . . . . 9 ((ac) ∩ (a ∪ (ac))) ≤ (a ∪ (ac))
3230, 31letr 137 . . . . . . . 8 (b ∩ (bc)) ≤ (a ∪ (ac))
33 oran2 92 . . . . . . . . . 10 (bc) = (bc )
3433lan 77 . . . . . . . . 9 (b ∩ (bc)) = (b ∩ (bc ) )
35 anor1 88 . . . . . . . . 9 (b ∩ (bc ) ) = (b ∪ (bc ))
3634, 35ax-r2 36 . . . . . . . 8 (b ∩ (bc)) = (b ∪ (bc ))
37 anor2 89 . . . . . . . . . 10 (ac) = (ac )
3837lor 70 . . . . . . . . 9 (a ∪ (ac)) = (a ∪ (ac ) )
39 oran1 91 . . . . . . . . 9 (a ∪ (ac ) ) = (a ∩ (ac ))
4038, 39ax-r2 36 . . . . . . . 8 (a ∪ (ac)) = (a ∩ (ac ))
4132, 36, 40le3tr2 141 . . . . . . 7 (b ∪ (bc )) ≤ (a ∩ (ac ))
4241lecon1 155 . . . . . 6 (a ∩ (ac )) ≤ (b ∪ (bc ))
43 leo 158 . . . . . . . 8 a ≤ (ac)
442ax-r5 38 . . . . . . . . 9 ((a3 c) ∪ c) = ((b3 c) ∪ c)
45 u3lemob 632 . . . . . . . . 9 ((a3 c) ∪ c) = (ac)
46 u3lemob 632 . . . . . . . . 9 ((b3 c) ∪ c) = (bc)
4744, 45, 463tr2 64 . . . . . . . 8 (ac) = (bc)
4843, 47lbtr 139 . . . . . . 7 a ≤ (bc)
4948lel 151 . . . . . 6 (a ∩ (ac )) ≤ (bc)
5042, 49ler2an 173 . . . . 5 (a ∩ (ac )) ≤ ((b ∪ (bc )) ∩ (bc))
51 comor1 461 . . . . . . 7 (bc) C b
5251comcom7 460 . . . . . . . 8 (bc) C b
53 comor2 462 . . . . . . . . 9 (bc) C c
5453comcom2 183 . . . . . . . 8 (bc) C c
5552, 54com2an 484 . . . . . . 7 (bc) C (bc )
5651, 55fh1r 473 . . . . . 6 ((b ∪ (bc )) ∩ (bc)) = ((b ∩ (bc)) ∪ ((bc ) ∩ (bc)))
57 anabs 121 . . . . . . 7 (b ∩ (bc)) = b
5833lan 77 . . . . . . . 8 ((bc ) ∩ (bc)) = ((bc ) ∩ (bc ) )
59 dff 101 . . . . . . . . 9 0 = ((bc ) ∩ (bc ) )
6059ax-r1 35 . . . . . . . 8 ((bc ) ∩ (bc ) ) = 0
6158, 60ax-r2 36 . . . . . . 7 ((bc ) ∩ (bc)) = 0
6257, 612or 72 . . . . . 6 ((b ∩ (bc)) ∪ ((bc ) ∩ (bc))) = (b ∪ 0)
63 or0 102 . . . . . 6 (b ∪ 0) = b
6456, 62, 633tr 65 . . . . 5 ((b ∪ (bc )) ∩ (bc)) = b
6550, 64lbtr 139 . . . 4 (a ∩ (ac )) ≤ b
6665ler 149 . . 3 (a ∩ (ac )) ≤ (b ∪ (bc))
6711, 66lel2or 170 . 2 ((ac) ∪ (a ∩ (ac ))) ≤ (b ∪ (bc))
68 id 59 . . . . 5 a = a
69 ax-a2 31 . . . . . 6 ((ac) ∪ a ) = (a ∪ (ac))
70 orabs 120 . . . . . 6 (a ∪ (ac)) = a
7169, 70ax-r2 36 . . . . 5 ((ac) ∪ a ) = a
7268, 68, 713tr1 63 . . . 4 a = ((ac) ∪ a )
73 df-t 41 . . . . 5 1 = ((ac) ∪ (ac) )
74 oran1 91 . . . . . . 7 (ac ) = (ac)
7574lor 70 . . . . . 6 ((ac) ∪ (ac )) = ((ac) ∪ (ac) )
7675ax-r1 35 . . . . 5 ((ac) ∪ (ac) ) = ((ac) ∪ (ac ))
7773, 76ax-r2 36 . . . 4 1 = ((ac) ∪ (ac ))
7872, 772an 79 . . 3 (a ∩ 1) = (((ac) ∪ a ) ∩ ((ac) ∪ (ac )))
79 an1 106 . . . 4 (a ∩ 1) = a
8079ax-r1 35 . . 3 a = (a ∩ 1)
81 coman1 185 . . . 4 (ac) C a
8281comcom7 460 . . . . 5 (ac) C a
83 coman2 186 . . . . . 6 (ac) C c
8483comcom2 183 . . . . 5 (ac) C c
8582, 84com2or 483 . . . 4 (ac) C (ac )
8681, 85fh3 471 . . 3 ((ac) ∪ (a ∩ (ac ))) = (((ac) ∪ a ) ∩ ((ac) ∪ (ac )))
8778, 80, 863tr1 63 . 2 a = ((ac) ∪ (a ∩ (ac )))
88 df-i1 44 . 2 (b1 c) = (b ∪ (bc))
8967, 87, 88le3tr1 140 1 a ≤ (b1 c)
Colors of variables: term
Syntax hints:   = wb 1  wle 2   wn 4  wo 6  wa 7  1wt 8  0wf 9  1 wi1 12  3 wi3 14
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-r3 439
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  neg3ant1  866
  Copyright terms: Public domain W3C validator