Users' Mathboxes Mathbox for Jarvin Udandy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mdandysum2p2e4 Structured version   Unicode version

Theorem mdandysum2p2e4 27920
Description: CONTRADICTION PROVED AT 1 + 1 = 2 . Luckily Mario Carneiro did a successful version of his own.

See Mario's Relevant Work: 1.3.14 Half-adders and full adders in propositional calculus

Given the right hypotheses we can prove a dandysum of 2+2=4. The qed step is the value '4' in Decimal BEING IMPLIED by the hypotheses.

Note: Values that when added which exceed a 4bit value are not supported.

Note: Digits begin from left (least) to right (greatest). e.g. 1000 would be '1', 0100 would be '2'. 0010 would be '4'.

How to perceive the hypotheses' bits in order: ( th <-> F. ), ( ta <-> F. ) Would be input value X's first bit, and input value Y's first bit.

( et <-> F. ), ( ze <-> F. ) would be input value X's second bit, and input value Y's second bit.

In mdandysum2p2e4, one might imagine what jth or jta could be then do the math with their truths. Also limited to the restriction jth, jta are having opposite truths equivalent to the stated truth constants.

(Contributed by Jarvin Udandy, 6-Sep-2016.)

Hypotheses
Ref Expression
mdandysum2p2e4.1  |-  (jth  <->  F.  )
mdandysum2p2e4.2  |-  (jta  <->  T.  )
mdandysum2p2e4.a  |-  ( ph  <->  ( th  /\  ta )
)
mdandysum2p2e4.b  |-  ( ps  <->  ( et  /\  ze )
)
mdandysum2p2e4.c  |-  ( ch  <->  ( si  /\  rh ) )
mdandysum2p2e4.d  |-  ( th  <-> jth
)
mdandysum2p2e4.e  |-  ( ta  <-> jth
)
mdandysum2p2e4.f  |-  ( et  <-> jta
)
mdandysum2p2e4.g  |-  ( ze  <-> jta
)
mdandysum2p2e4.h  |-  ( si  <-> jth
)
mdandysum2p2e4.i  |-  ( rh  <-> jth
)
mdandysum2p2e4.j  |-  ( mu  <-> jth
)
mdandysum2p2e4.k  |-  ( la  <-> jth
)
mdandysum2p2e4.l  |-  ( ka  <->  ( ( th  \/_  ta )  \/_  ( th  /\  ta ) ) )
mdandysum2p2e4.m  |-  (jph  <->  ( ( et  \/_  ze )  \/  ph ) )
mdandysum2p2e4.n  |-  (jps  <->  ( ( si  \/_  rh )  \/  ps )
)
mdandysum2p2e4.o  |-  (jch  <->  ( ( mu  \/_  la )  \/  ch ) )
Assertion
Ref Expression
mdandysum2p2e4  |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph  <->  ( th  /\  ta ) )  /\  ( ps  <->  ( et  /\  ze ) ) )  /\  ( ch  <->  ( si  /\  rh ) ) )  /\  ( th  <->  F.  ) )  /\  ( ta  <->  F.  )
)  /\  ( et  <->  T.  ) )  /\  ( ze 
<->  T.  ) )  /\  ( si  <->  F.  ) )  /\  ( rh  <->  F.  )
)  /\  ( mu  <->  F.  ) )  /\  ( la 
<->  F.  ) )  /\  ( ka  <->  ( ( th 
\/_  ta )  \/_  ( th  /\  ta ) ) ) )  /\  (jph  <->  ( ( et  \/_  ze )  \/  ph ) ) )  /\  (jps  <->  ( ( si  \/_  rh )  \/  ps )
) )  /\  (jch  <->  ( ( mu  \/_  la )  \/  ch ) ) )  ->  ( ( ( ( ka  <->  F.  )  /\  (jph  <->  F.  )
)  /\  (jps  <->  T.  ) )  /\  (jch  <->  F.  ) ) )

Proof of Theorem mdandysum2p2e4
StepHypRef Expression
1 mdandysum2p2e4.a . 2  |-  ( ph  <->  ( th  /\  ta )
)
2 mdandysum2p2e4.b . 2  |-  ( ps  <->  ( et  /\  ze )
)
3 mdandysum2p2e4.c . 2  |-  ( ch  <->  ( si  /\  rh ) )
4 mdandysum2p2e4.d . . 3  |-  ( th  <-> jth
)
5 mdandysum2p2e4.1 . . 3  |-  (jth  <->  F.  )
64, 5aisbbisfaisf 27846 . 2  |-  ( th  <->  F.  )
7 mdandysum2p2e4.e . . 3  |-  ( ta  <-> jth
)
87, 5aisbbisfaisf 27846 . 2  |-  ( ta  <->  F.  )
9 mdandysum2p2e4.f . . 3  |-  ( et  <-> jta
)
10 mdandysum2p2e4.2 . . 3  |-  (jta  <->  T.  )
119, 10aiffbbtat 27845 . 2  |-  ( et  <->  T.  )
12 mdandysum2p2e4.g . . 3  |-  ( ze  <-> jta
)
1312, 10aiffbbtat 27845 . 2  |-  ( ze  <->  T.  )
14 mdandysum2p2e4.h . . 3  |-  ( si  <-> jth
)
1514, 5aisbbisfaisf 27846 . 2  |-  ( si  <->  F.  )
16 mdandysum2p2e4.i . . 3  |-  ( rh  <-> jth
)
1716, 5aisbbisfaisf 27846 . 2  |-  ( rh  <->  F.  )
18 mdandysum2p2e4.j . . 3  |-  ( mu  <-> jth
)
1918, 5aisbbisfaisf 27846 . 2  |-  ( mu  <->  F.  )
20 mdandysum2p2e4.k . . 3  |-  ( la  <-> jth
)
2120, 5aisbbisfaisf 27846 . 2  |-  ( la  <->  F.  )
22 mdandysum2p2e4.l . 2  |-  ( ka  <->  ( ( th  \/_  ta )  \/_  ( th  /\  ta ) ) )
23 mdandysum2p2e4.m . 2  |-  (jph  <->  ( ( et  \/_  ze )  \/  ph ) )
24 mdandysum2p2e4.n . 2  |-  (jps  <->  ( ( si  \/_  rh )  \/  ps )
)
25 mdandysum2p2e4.o . 2  |-  (jch  <->  ( ( mu  \/_  la )  \/  ch ) )
261, 2, 3, 6, 8, 11, 13, 15, 17, 19, 21, 22, 23, 24, 25dandysum2p2e4 27919 1  |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph  <->  ( th  /\  ta ) )  /\  ( ps  <->  ( et  /\  ze ) ) )  /\  ( ch  <->  ( si  /\  rh ) ) )  /\  ( th  <->  F.  ) )  /\  ( ta  <->  F.  )
)  /\  ( et  <->  T.  ) )  /\  ( ze 
<->  T.  ) )  /\  ( si  <->  F.  ) )  /\  ( rh  <->  F.  )
)  /\  ( mu  <->  F.  ) )  /\  ( la 
<->  F.  ) )  /\  ( ka  <->  ( ( th 
\/_  ta )  \/_  ( th  /\  ta ) ) ) )  /\  (jph  <->  ( ( et  \/_  ze )  \/  ph ) ) )  /\  (jps  <->  ( ( si  \/_  rh )  \/  ps )
) )  /\  (jch  <->  ( ( mu  \/_  la )  \/  ch ) ) )  ->  ( ( ( ( ka  <->  F.  )  /\  (jph  <->  F.  )
)  /\  (jps  <->  T.  ) )  /\  (jch  <->  F.  ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    \/_ wxo 1313    T. wtru 1325    F. wfal 1326
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-xor 1314  df-tru 1328  df-fal 1329
  Copyright terms: Public domain W3C validator