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

Theorem dandysum2p2e4 37986
 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
dandysum2p2e4.b
dandysum2p2e4.c
dandysum2p2e4.d
dandysum2p2e4.e
dandysum2p2e4.f
dandysum2p2e4.g
dandysum2p2e4.h
dandysum2p2e4.i
dandysum2p2e4.j
dandysum2p2e4.k
dandysum2p2e4.l
dandysum2p2e4.m jph
dandysum2p2e4.n jps
dandysum2p2e4.o jch
Assertion
Ref Expression
dandysum2p2e4 jph jps jch jph jps jch

Proof of Theorem dandysum2p2e4
StepHypRef Expression
1 dandysum2p2e4.l . . . . . . 7
21biimpi 197 . . . . . 6
3 dandysum2p2e4.d . . . . . . . . . 10
4 dandysum2p2e4.e . . . . . . . . . 10
53, 4bothfbothsame 37887 . . . . . . . . 9
65aisbnaxb 37898 . . . . . . . 8
73aisfina 37885 . . . . . . . . 9
87notatnand 37883 . . . . . . . 8
96, 82false 351 . . . . . . 7
109aisbnaxb 37898 . . . . . 6
112, 10aibnbaif 37894 . . . . 5
12 dandysum2p2e4.m . . . . . . 7 jph
1312biimpi 197 . . . . . 6 jph
14 dandysum2p2e4.f . . . . . . . . 9
15 dandysum2p2e4.g . . . . . . . . 9
1614, 15bothtbothsame 37886 . . . . . . . 8
1716aisbnaxb 37898 . . . . . . 7
18 dandysum2p2e4.a . . . . . . . 8
198, 18mtbir 300 . . . . . . 7
2017, 19pm3.2ni 862 . . . . . 6
2113, 20aibnbaif 37894 . . . . 5 jph
2211, 21pm3.2i 456 . . . 4 jph
23 dandysum2p2e4.n . . . . 5 jps
24 dandysum2p2e4.b . . . . . . . . 9
2514, 15astbstanbst 37896 . . . . . . . . 9
2624, 25aiffbbtat 37888 . . . . . . . 8
2726aistia 37884 . . . . . . 7
2827olci 392 . . . . . 6
2928bitru 1449 . . . . 5
3023, 29aiffbbtat 37888 . . . 4 jps
3122, 30pm3.2i 456 . . 3 jph jps
32 dandysum2p2e4.o . . . . 5 jch
3332biimpi 197 . . . 4 jch
34 dandysum2p2e4.j . . . . . . 7
35 dandysum2p2e4.k . . . . . . 7
3634, 35bothfbothsame 37887 . . . . . 6
3736aisbnaxb 37898 . . . . 5
38 dandysum2p2e4.h . . . . . . . 8
3938aisfina 37885 . . . . . . 7
4039notatnand 37883 . . . . . 6
41 dandysum2p2e4.c . . . . . 6
4240, 41mtbir 300 . . . . 5
4337, 42pm3.2ni 862 . . . 4
4433, 43aibnbaif 37894 . . 3 jch
4531, 44pm3.2i 456 . 2 jph jps jch
4645a1i 11 1 jph jps jch jph jps jch
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wo 369   wa 370   wxo 1400   wtru 1438   wfal 1442 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 188  df-or 371  df-an 372  df-xor 1401  df-tru 1440  df-fal 1443 This theorem is referenced by:  mdandysum2p2e4  37987
 Copyright terms: Public domain W3C validator