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

Theorem dandysum2p2e4 27919
 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 187 . . . . . 6
3 dandysum2p2e4.d . . . . . . . . . 10
4 dandysum2p2e4.e . . . . . . . . . 10
53, 4bothfbothsame 27844 . . . . . . . . 9
65aisbnaxb 27855 . . . . . . . 8
73aisfina 27842 . . . . . . . . 9
87notatnand 27840 . . . . . . . 8
96, 82false 340 . . . . . . 7
109aisbnaxb 27855 . . . . . 6
112, 10aibnbaif 27851 . . . . 5
12 dandysum2p2e4.m . . . . . . 7 jph
1312biimpi 187 . . . . . 6 jph
14 dandysum2p2e4.f . . . . . . . . 9
15 dandysum2p2e4.g . . . . . . . . 9
1614, 15bothtbothsame 27843 . . . . . . . 8
1716aisbnaxb 27855 . . . . . . 7
18 dandysum2p2e4.a . . . . . . . 8
198, 18mtbir 291 . . . . . . 7
2017, 19pm3.2ni 828 . . . . . 6
2113, 20aibnbaif 27851 . . . . 5 jph
2211, 21pm3.2i 442 . . . 4 jph
23 dandysum2p2e4.n . . . . 5 jps
24 dandysum2p2e4.b . . . . . . . . 9
2514, 15astbstanbst 27853 . . . . . . . . 9
2624, 25aiffbbtat 27845 . . . . . . . 8
2726aistia 27841 . . . . . . 7
2827olci 381 . . . . . 6
2928bitru 1335 . . . . 5
3023, 29aiffbbtat 27845 . . . 4 jps
3122, 30pm3.2i 442 . . 3 jph jps
32 dandysum2p2e4.o . . . . 5 jch
3332biimpi 187 . . . 4 jch
34 dandysum2p2e4.j . . . . . . 7
35 dandysum2p2e4.k . . . . . . 7
3634, 35bothfbothsame 27844 . . . . . 6
3736aisbnaxb 27855 . . . . 5
38 dandysum2p2e4.h . . . . . . . 8
3938aisfina 27842 . . . . . . 7
4039notatnand 27840 . . . . . 6
41 dandysum2p2e4.c . . . . . 6
4240, 41mtbir 291 . . . . 5
4337, 42pm3.2ni 828 . . . 4
4433, 43aibnbaif 27851 . . 3 jch
4531, 44pm3.2i 442 . 2 jph jps jch
4645a1i 11 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 is referenced by:  mdandysum2p2e4  27920 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