QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  mlaconjo Unicode version
Theorem mlaconjo 886
Description: OML proof of Mladen's conjecture.
Assertion
Ref Expression
mlaconjo ((a == b) ^ ((a == c) v (b == c))) =< (a == c)
Proof of Theorem mlaconjo
StepHypRef Expression
1 dfb 94 . . . 4 (a == b) = ((a ^ b) v (a' ^ b'))
21bile 142 . . 3 (a == b) =< ((a ^ b) v (a' ^ b'))
3 mlaconjolem 885 . . 3 ((a == c) v (b == c)) =< ((c ^ (a v b)) v (c' ^ (a' v b')))
42, 3le2an 169 . 2 ((a == b) ^ ((a == c) v (b == c))) =< (((a ^ b) v (a' ^ b')) ^ ((c ^ (a v b)) v (c' ^ (a' v b'))))
5 lea 160 . . . . 5 (a ^ b) =< a
6 lea 160 . . . . 5 (c ^ (a v b)) =< c
75, 6le2an 169 . . . 4 ((a ^ b) ^ (c ^ (a v b))) =< (a ^ c)
8 lea 160 . . . . 5 (a' ^ b') =< a'
9 lea 160 . . . . 5 (c' ^ (a' v b')) =< c'
108, 9le2an 169 . . . 4 ((a' ^ b') ^ (c' ^ (a' v b'))) =< (a' ^ c')
117, 10le2or 168 . . 3 (((a ^ b) ^ (c ^ (a v b))) v ((a' ^ b') ^ (c' ^ (a' v b')))) =< ((a ^ c) v (a' ^ c'))
12 leao1 162 . . . . . . . 8 (a ^ b) =< (a v b)
13 oran 87 . . . . . . . 8 (a v b) = (a' ^ b')'
1412, 13lbtr 139 . . . . . . 7 (a ^ b) =< (a' ^ b')'
1514lecom 180 . . . . . 6 (a ^ b) C (a' ^ b')'
1615comcom7 460 . . . . 5 (a ^ b) C (a' ^ b')
17 leor 159 . . . . . . . 8 (a ^ b) =< (c v (a ^ b))
18 df-a 40 . . . . . . . . . 10 (a ^ b) = (a' v b')'
1918lor 70 . . . . . . . . 9 (c v (a ^ b)) = (c v (a' v b')')
20 oran1 91 . . . . . . . . 9 (c v (a' v b')') = (c' ^ (a' v b'))'
2119, 20ax-r2 36 . . . . . . . 8 (c v (a ^ b)) = (c' ^ (a' v b'))'
2217, 21lbtr 139 . . . . . . 7 (a ^ b) =< (c' ^ (a' v b'))'
2322lecom 180 . . . . . 6 (a ^ b) C (c' ^ (a' v b'))'
2423comcom7 460 . . . . 5 (a ^ b) C (c' ^ (a' v b'))
25 lear 161 . . . . . . . 8 (c ^ (a v b)) =< (a v b)
2625, 13lbtr 139 . . . . . . 7 (c ^ (a v b)) =< (a' ^ b')'
2726lecom 180 . . . . . 6 (c ^ (a v b)) C (a' ^ b')'
2827comcom7 460 . . . . 5 (c ^ (a v b)) C (a' ^ b')
29 leao1 162 . . . . . . . 8 (c ^ (a v b)) =< (c v (a' v b')')
3029, 20lbtr 139 . . . . . . 7 (c ^ (a v b)) =< (c' ^ (a' v b'))'
3130lecom 180 . . . . . 6 (c ^ (a v b)) C (c' ^ (a' v b'))'
3231comcom7 460 . . . . 5 (c ^ (a v b)) C (c' ^ (a' v b'))
3316, 24, 28, 32mh 879 . . . 4 (((a ^ b) v (a' ^ b')) ^ ((c ^ (a v b)) v (c' ^ (a' v b')))) = ((((a ^ b) ^ (c ^ (a v b))) v ((a ^ b) ^ (c' ^ (a' v b')))) v (((a' ^ b') ^ (c ^ (a v b))) v ((a' ^ b') ^ (c' ^ (a' v b')))))
34 an12 81 . . . . . . . 8 ((a ^ b) ^ (c' ^ (a' v b'))) = (c' ^ ((a ^ b) ^ (a' v b')))
35 oran3 93 . . . . . . . . . . 11 (a' v b') = (a ^ b)'
3635lan 77 . . . . . . . . . 10 ((a ^ b) ^ (a' v b')) = ((a ^ b) ^ (a ^ b)')
37 dff 101 . . . . . . . . . . 11 0 = ((a ^ b) ^ (a ^ b)')
3837ax-r1 35 . . . . . . . . . 10 ((a ^ b) ^ (a ^ b)') = 0
3936, 38ax-r2 36 . . . . . . . . 9 ((a ^ b) ^ (a' v b')) = 0
4039lan 77 . . . . . . . 8 (c' ^ ((a ^ b) ^ (a' v b'))) = (c' ^ 0)
41 an0 108 . . . . . . . 8 (c' ^ 0) = 0
4234, 40, 413tr 65 . . . . . . 7 ((a ^ b) ^ (c' ^ (a' v b'))) = 0
4342lor 70 . . . . . 6 (((a ^ b) ^ (c ^ (a v b))) v ((a ^ b) ^ (c' ^ (a' v b')))) = (((a ^ b) ^ (c ^ (a v b))) v 0)
44 or0 102 . . . . . 6 (((a ^ b) ^ (c ^ (a v b))) v 0) = ((a ^ b) ^ (c ^ (a v b)))
4543, 44ax-r2 36 . . . . 5 (((a ^ b) ^ (c ^ (a v b))) v ((a ^ b) ^ (c' ^ (a' v b')))) = ((a ^ b) ^ (c ^ (a v b)))
46 an12 81 . . . . . . . 8 ((a' ^ b') ^ (c ^ (a v b))) = (c ^ ((a' ^ b') ^ (a v b)))
4713lan 77 . . . . . . . . . 10 ((a' ^ b') ^ (a v b)) = ((a' ^ b') ^ (a' ^ b')')
48 dff 101 . . . . . . . . . . 11 0 = ((a' ^ b') ^ (a' ^ b')')
4948ax-r1 35 . . . . . . . . . 10 ((a' ^ b') ^ (a' ^ b')') = 0
5047, 49ax-r2 36 . . . . . . . . 9 ((a' ^ b') ^ (a v b)) = 0
5150lan 77 . . . . . . . 8 (c ^ ((a' ^ b') ^ (a v b))) = (c ^ 0)
52 an0 108 . . . . . . . 8 (c ^ 0) = 0
5346, 51, 523tr 65 . . . . . . 7 ((a' ^ b') ^ (c ^ (a v b))) = 0
5453ax-r5 38 . . . . . 6 (((a' ^ b') ^ (c ^ (a v b))) v ((a' ^ b') ^ (c' ^ (a' v b')))) = (0 v ((a' ^ b') ^ (c' ^ (a' v b'))))
55 or0r 103 . . . . . 6 (0 v ((a' ^ b') ^ (c' ^ (a' v b')))) = ((a' ^ b') ^ (c' ^ (a' v b')))
5654, 55ax-r2 36 . . . . 5 (((a' ^ b') ^ (c ^ (a v b))) v ((a' ^ b') ^ (c' ^ (a' v b')))) = ((a' ^ b') ^ (c' ^ (a' v b')))
5745, 562or 72 . . . 4 ((((a ^ b) ^ (c ^ (a v b))) v ((a ^ b) ^ (c' ^ (a' v b')))) v (((a' ^ b') ^ (c ^ (a v b))) v ((a' ^ b') ^ (c' ^ (a' v b'))))) = (((a ^ b) ^ (c ^ (a v b))) v ((a' ^ b') ^ (c' ^ (a' v b'))))
5833, 57ax-r2 36 . . 3 (((a ^ b) v (a' ^ b')) ^ ((c ^ (a v b)) v (c' ^ (a' v b')))) = (((a ^ b) ^ (c ^ (a v b))) v ((a' ^ b') ^ (c' ^ (a' v b'))))
59 dfb 94 . . 3 (a == c) = ((a ^ c) v (a' ^ c'))
6011, 58, 59le3tr1 140 . 2 (((a ^ b) v (a' ^ b')) ^ ((c ^ (a v b)) v (c' ^ (a' v b')))) =< (a == c)
614, 60letr 137 1 ((a == b) ^ ((a == c) v (b == c))) =< (a == c)
Colors of variables: term
Syntax hints:   =< wle 2  'wn 4   == tb 5   v wo 6   ^ wa 7  0wf 9
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-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  distid  887
  Copyright terms: Public domain W3C validator