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
mdandysum2p2e4.2 jta
mdandysum2p2e4.a
mdandysum2p2e4.b
mdandysum2p2e4.c
mdandysum2p2e4.d jth
mdandysum2p2e4.e jth
mdandysum2p2e4.f jta
mdandysum2p2e4.g jta
mdandysum2p2e4.h jth
mdandysum2p2e4.i jth
mdandysum2p2e4.j jth
mdandysum2p2e4.k jth
mdandysum2p2e4.l
mdandysum2p2e4.m jph
mdandysum2p2e4.n jps
mdandysum2p2e4.o jch
Assertion
Ref Expression
mdandysum2p2e4 jph jps jch jph jps jch

Proof of Theorem mdandysum2p2e4
StepHypRef Expression
1 mdandysum2p2e4.a . 2
2 mdandysum2p2e4.b . 2
3 mdandysum2p2e4.c . 2
4 mdandysum2p2e4.d . . 3 jth
5 mdandysum2p2e4.1 . . 3 jth
64, 5aisbbisfaisf 27846 . 2
7 mdandysum2p2e4.e . . 3 jth
87, 5aisbbisfaisf 27846 . 2
9 mdandysum2p2e4.f . . 3 jta
10 mdandysum2p2e4.2 . . 3 jta
119, 10aiffbbtat 27845 . 2
12 mdandysum2p2e4.g . . 3 jta
1312, 10aiffbbtat 27845 . 2
14 mdandysum2p2e4.h . . 3 jth
1514, 5aisbbisfaisf 27846 . 2
16 mdandysum2p2e4.i . . 3 jth
1716, 5aisbbisfaisf 27846 . 2
18 mdandysum2p2e4.j . . 3 jth
1918, 5aisbbisfaisf 27846 . 2
20 mdandysum2p2e4.k . . 3 jth
2120, 5aisbbisfaisf 27846 . 2
22 mdandysum2p2e4.l . 2
23 mdandysum2p2e4.m . 2 jph
24 mdandysum2p2e4.n . 2 jps
25 mdandysum2p2e4.o . 2 jch
261, 2, 3, 6, 8, 11, 13, 15, 17, 19, 21, 22, 23, 24, 25dandysum2p2e4 27919 1 jph jps jch jph jps jch
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wo 358   wa 359   wxo 1313   wtru 1325   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