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

Theorem dandysum2p2e4 30129
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 194 . . . . . 6  |-  ( ka 
->  ( ( th  \/_  ta )  \/_  ( th 
/\  ta ) ) )
3 dandysum2p2e4.d . . . . . . . . . 10  |-  ( th  <-> F.  )
4 dandysum2p2e4.e . . . . . . . . . 10  |-  ( ta  <-> F.  )
53, 4bothfbothsame 30054 . . . . . . . . 9  |-  ( th  <->  ta )
65aisbnaxb 30065 . . . . . . . 8  |-  -.  ( th  \/_  ta )
73aisfina 30052 . . . . . . . . 9  |-  -.  th
87notatnand 30050 . . . . . . . 8  |-  -.  ( th  /\  ta )
96, 82false 350 . . . . . . 7  |-  ( ( th  \/_  ta )  <->  ( th  /\  ta )
)
109aisbnaxb 30065 . . . . . 6  |-  -.  (
( th  \/_  ta )  \/_  ( th  /\  ta ) )
112, 10aibnbaif 30061 . . . . 5  |-  ( ka  <-> F.  )
12 dandysum2p2e4.m . . . . . . 7  |-  (jph  <->  ( ( et  \/_  ze )  \/  ph ) )
1312biimpi 194 . . . . . 6  |-  (jph 
->  ( ( et  \/_  ze )  \/  ph )
)
14 dandysum2p2e4.f . . . . . . . . 9  |-  ( et  <-> T.  )
15 dandysum2p2e4.g . . . . . . . . 9  |-  ( ze  <-> T.  )
1614, 15bothtbothsame 30053 . . . . . . . 8  |-  ( et  <->  ze )
1716aisbnaxb 30065 . . . . . . 7  |-  -.  ( et  \/_  ze )
18 dandysum2p2e4.a . . . . . . . 8  |-  ( ph  <->  ( th  /\  ta )
)
198, 18mtbir 299 . . . . . . 7  |-  -.  ph
2017, 19pm3.2ni 850 . . . . . 6  |-  -.  (
( et  \/_  ze )  \/  ph )
2113, 20aibnbaif 30061 . . . . 5  |-  (jph  <-> F.  )
2211, 21pm3.2i 455 . . . 4  |-  ( ( ka  <-> F.  )  /\  (jph  <-> F.  )
)
23 dandysum2p2e4.n . . . . 5  |-  (jps  <->  ( ( si  \/_  rh )  \/  ps )
)
24 dandysum2p2e4.b . . . . . . . . 9  |-  ( ps  <->  ( et  /\  ze )
)
2514, 15astbstanbst 30063 . . . . . . . . 9  |-  ( ( et  /\  ze )  <-> T.  )
2624, 25aiffbbtat 30055 . . . . . . . 8  |-  ( ps  <-> T.  )
2726aistia 30051 . . . . . . 7  |-  ps
2827olci 391 . . . . . 6  |-  ( ( si  \/_  rh )  \/  ps )
2928bitru 1382 . . . . 5  |-  ( ( ( si  \/_  rh )  \/  ps )  <-> T.  )
3023, 29aiffbbtat 30055 . . . 4  |-  (jps  <-> T.  )
3122, 30pm3.2i 455 . . 3  |-  ( ( ( ka  <-> F.  )  /\  (jph  <-> F.  )
)  /\  (jps  <-> T.  ) )
32 dandysum2p2e4.o . . . . 5  |-  (jch  <->  ( ( mu  \/_  la )  \/  ch ) )
3332biimpi 194 . . . 4  |-  (jch 
->  ( ( mu  \/_  la )  \/  ch )
)
34 dandysum2p2e4.j . . . . . . 7  |-  ( mu  <-> F.  )
35 dandysum2p2e4.k . . . . . . 7  |-  ( la  <-> F.  )
3634, 35bothfbothsame 30054 . . . . . 6  |-  ( mu  <->  la )
3736aisbnaxb 30065 . . . . 5  |-  -.  ( mu  \/_  la )
38 dandysum2p2e4.h . . . . . . . 8  |-  ( si  <-> F.  )
3938aisfina 30052 . . . . . . 7  |-  -.  si
4039notatnand 30050 . . . . . 6  |-  -.  ( si  /\  rh )
41 dandysum2p2e4.c . . . . . 6  |-  ( ch  <->  ( si  /\  rh ) )
4240, 41mtbir 299 . . . . 5  |-  -.  ch
4337, 42pm3.2ni 850 . . . 4  |-  -.  (
( mu  \/_  la )  \/  ch )
4433, 43aibnbaif 30061 . . 3  |-  (jch  <-> F.  )
4531, 44pm3.2i 455 . 2  |-  ( ( ( ( ka  <-> F.  )  /\  (jph  <-> F.  )
)  /\  (jps  <-> T.  ) )  /\  (jch  <-> F.  ) )
4645a1i 11 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 setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    \/_ wxo 1351   T. wtru 1371   F. wfal 1375
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-xor 1352  df-tru 1373  df-fal 1376
This theorem is referenced by:  mdandysum2p2e4  30130
  Copyright terms: Public domain W3C validator