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

Theorem dandysum2p2e4 28046
Description:

CONTRADICTION PROVED AT 1 + 1 = 2 .

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. (Contributed by Jarvin Udandy, 6-Sep-2016.)

Hypotheses
Ref Expression
dandysum2p2e4.a  |-  ( ph  <->  ( th  /\  ta )
)
dandysum2p2e4.b  |-  ( ps  <->  ( et  /\  ze )
)
dandysum2p2e4.c  |-  ( ch  <->  ( si  /\  rh ) )
dandysum2p2e4.d  |-  ( th  <->  F.  )
dandysum2p2e4.e  |-  ( ta  <->  F.  )
dandysum2p2e4.f  |-  ( et  <->  T.  )
dandysum2p2e4.g  |-  ( ze  <->  T.  )
dandysum2p2e4.h  |-  ( si  <->  F.  )
dandysum2p2e4.i  |-  ( rh  <->  F.  )
dandysum2p2e4.j  |-  ( mu  <->  F.  )
dandysum2p2e4.k  |-  ( la  <->  F.  )
dandysum2p2e4.l  |-  ( ka  <->  ( ( th  \/_  ta )  \/_  ( th  /\  ta ) ) )
dandysum2p2e4.m  |-  (jph  <->  ( ( et  \/_  ze )  \/  ph ) )
dandysum2p2e4.n  |-  (jps  <->  ( ( si  \/_  rh )  \/  ps )
)
dandysum2p2e4.o  |-  (jch  <->  ( ( mu  \/_  la )  \/  ch ) )
Assertion
Ref Expression
dandysum2p2e4  |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 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 dandysum2p2e4
StepHypRef Expression
1 dandysum2p2e4.l . . . . . . 7  |-  ( ka  <->  ( ( th  \/_  ta )  \/_  ( th  /\  ta ) ) )
21biimpi 186 . . . . . 6  |-  ( ka 
->  ( ( th  \/_  ta )  \/_  ( th 
/\  ta ) ) )
3 dandysum2p2e4.d . . . . . . . . . 10  |-  ( th  <->  F.  )
4 dandysum2p2e4.e . . . . . . . . . 10  |-  ( ta  <->  F.  )
53, 4bothfbothsame 27971 . . . . . . . . 9  |-  ( th  <->  ta )
65aisbnaxb 27982 . . . . . . . 8  |-  -.  ( th  \/_  ta )
73aisfina 27969 . . . . . . . . 9  |-  -.  th
87notatnand 27967 . . . . . . . 8  |-  -.  ( th  /\  ta )
96, 82false 339 . . . . . . 7  |-  ( ( th  \/_  ta )  <->  ( th  /\  ta )
)
109aisbnaxb 27982 . . . . . 6  |-  -.  (
( th  \/_  ta )  \/_  ( th  /\  ta ) )
112, 10aibnbaif 27978 . . . . 5  |-  ( ka  <->  F.  )
12 dandysum2p2e4.m . . . . . . 7  |-  (jph  <->  ( ( et  \/_  ze )  \/  ph ) )
1312biimpi 186 . . . . . 6  |-  (jph 
->  ( ( et  \/_  ze )  \/  ph )
)
14 dandysum2p2e4.f . . . . . . . . 9  |-  ( et  <->  T.  )
15 dandysum2p2e4.g . . . . . . . . 9  |-  ( ze  <->  T.  )
1614, 15bothtbothsame 27970 . . . . . . . 8  |-  ( et  <->  ze )
1716aisbnaxb 27982 . . . . . . 7  |-  -.  ( et  \/_  ze )
18 dandysum2p2e4.a . . . . . . . 8  |-  ( ph  <->  ( th  /\  ta )
)
198, 18mtbir 290 . . . . . . 7  |-  -.  ph
2017, 19pm3.2ni 827 . . . . . 6  |-  -.  (
( et  \/_  ze )  \/  ph )
2113, 20aibnbaif 27978 . . . . 5  |-  (jph  <->  F.  )
2211, 21pm3.2i 441 . . . 4  |-  ( ( ka  <->  F.  )  /\  (jph  <->  F.  )
)
23 dandysum2p2e4.n . . . . 5  |-  (jps  <->  ( ( si  \/_  rh )  \/  ps )
)
24 dandysum2p2e4.b . . . . . . . . 9  |-  ( ps  <->  ( et  /\  ze )
)
2514, 15astbstanbst 27980 . . . . . . . . 9  |-  ( ( et  /\  ze )  <->  T.  )
2624, 25aiffbbtat 27972 . . . . . . . 8  |-  ( ps  <->  T.  )
2726aistia 27968 . . . . . . 7  |-  ps
2827olci 380 . . . . . 6  |-  ( ( si  \/_  rh )  \/  ps )
2928bitru 1317 . . . . 5  |-  ( ( ( si  \/_  rh )  \/  ps )  <->  T.  )
3023, 29aiffbbtat 27972 . . . 4  |-  (jps  <->  T.  )
3122, 30pm3.2i 441 . . 3  |-  ( ( ( ka  <->  F.  )  /\  (jph  <->  F.  )
)  /\  (jps  <->  T.  ) )
32 dandysum2p2e4.o . . . . 5  |-  (jch  <->  ( ( mu  \/_  la )  \/  ch ) )
3332biimpi 186 . . . 4  |-  (jch 
->  ( ( mu  \/_  la )  \/  ch )
)
34 dandysum2p2e4.j . . . . . . 7  |-  ( mu  <->  F.  )
35 dandysum2p2e4.k . . . . . . 7  |-  ( la  <->  F.  )
3634, 35bothfbothsame 27971 . . . . . 6  |-  ( mu  <->  la )
3736aisbnaxb 27982 . . . . 5  |-  -.  ( mu  \/_  la )
38 dandysum2p2e4.h . . . . . . . 8  |-  ( si  <->  F.  )
3938aisfina 27969 . . . . . . 7  |-  -.  si
4039notatnand 27967 . . . . . 6  |-  -.  ( si  /\  rh )
41 dandysum2p2e4.c . . . . . 6  |-  ( ch  <->  ( si  /\  rh ) )
4240, 41mtbir 290 . . . . 5  |-  -.  ch
4337, 42pm3.2ni 827 . . . 4  |-  -.  (
( mu  \/_  la )  \/  ch )
4433, 43aibnbaif 27978 . . 3  |-  (jch  <->  F.  )
4531, 44pm3.2i 441 . 2  |-  ( ( ( ( ka  <->  F.  )  /\  (jph  <->  F.  )
)  /\  (jps  <->  T.  ) )  /\  (jch  <->  F.  ) )
4645a1i 10 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 176    \/ wo 357    /\ wa 358    \/_ wxo 1295    T. wtru 1307    F. wfal 1308
This theorem is referenced by:  mdandysum2p2e4  28047
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 177  df-or 359  df-an 360  df-xor 1296  df-tru 1310  df-fal 1311
  Copyright terms: Public domain W3C validator