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

Theorem dandysum2p2e4 40466
 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 206 . . . . . 6 (𝜅 → ((𝜃𝜏) ⊻ (𝜃𝜏)))
3 dandysum2p2e4.d . . . . . . . . . 10 (𝜃 ↔ ⊥)
4 dandysum2p2e4.e . . . . . . . . . 10 (𝜏 ↔ ⊥)
53, 4bothfbothsame 40368 . . . . . . . . 9 (𝜃𝜏)
65aisbnaxb 40379 . . . . . . . 8 ¬ (𝜃𝜏)
73aisfina 40366 . . . . . . . . 9 ¬ 𝜃
87notatnand 40364 . . . . . . . 8 ¬ (𝜃𝜏)
96, 82false 365 . . . . . . 7 ((𝜃𝜏) ↔ (𝜃𝜏))
109aisbnaxb 40379 . . . . . 6 ¬ ((𝜃𝜏) ⊻ (𝜃𝜏))
112, 10aibnbaif 40375 . . . . 5 (𝜅 ↔ ⊥)
12 dandysum2p2e4.m . . . . . . 7 (jph ↔ ((𝜂𝜁) ∨ 𝜑))
1312biimpi 206 . . . . . 6 (jph → ((𝜂𝜁) ∨ 𝜑))
14 dandysum2p2e4.f . . . . . . . . 9 (𝜂 ↔ ⊤)
15 dandysum2p2e4.g . . . . . . . . 9 (𝜁 ↔ ⊤)
1614, 15bothtbothsame 40367 . . . . . . . 8 (𝜂𝜁)
1716aisbnaxb 40379 . . . . . . 7 ¬ (𝜂𝜁)
18 dandysum2p2e4.a . . . . . . . 8 (𝜑 ↔ (𝜃𝜏))
198, 18mtbir 313 . . . . . . 7 ¬ 𝜑
2017, 19pm3.2ni 898 . . . . . 6 ¬ ((𝜂𝜁) ∨ 𝜑)
2113, 20aibnbaif 40375 . . . . 5 (jph ↔ ⊥)
2211, 21pm3.2i 471 . . . 4 ((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥))
23 dandysum2p2e4.n . . . . 5 (jps ↔ ((𝜎𝜌) ∨ 𝜓))
24 dandysum2p2e4.b . . . . . . . . 9 (𝜓 ↔ (𝜂𝜁))
2514, 15astbstanbst 40377 . . . . . . . . 9 ((𝜂𝜁) ↔ ⊤)
2624, 25aiffbbtat 40369 . . . . . . . 8 (𝜓 ↔ ⊤)
2726aistia 40365 . . . . . . 7 𝜓
2827olci 406 . . . . . 6 ((𝜎𝜌) ∨ 𝜓)
2928bitru 1493 . . . . 5 (((𝜎𝜌) ∨ 𝜓) ↔ ⊤)
3023, 29aiffbbtat 40369 . . . 4 (jps ↔ ⊤)
3122, 30pm3.2i 471 . . 3 (((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤))
32 dandysum2p2e4.o . . . . 5 (jch ↔ ((𝜇𝜆) ∨ 𝜒))
3332biimpi 206 . . . 4 (jch → ((𝜇𝜆) ∨ 𝜒))
34 dandysum2p2e4.j . . . . . . 7 (𝜇 ↔ ⊥)
35 dandysum2p2e4.k . . . . . . 7 (𝜆 ↔ ⊥)
3634, 35bothfbothsame 40368 . . . . . 6 (𝜇𝜆)
3736aisbnaxb 40379 . . . . 5 ¬ (𝜇𝜆)
38 dandysum2p2e4.h . . . . . . . 8 (𝜎 ↔ ⊥)
3938aisfina 40366 . . . . . . 7 ¬ 𝜎
4039notatnand 40364 . . . . . 6 ¬ (𝜎𝜌)
41 dandysum2p2e4.c . . . . . 6 (𝜒 ↔ (𝜎𝜌))
4240, 41mtbir 313 . . . . 5 ¬ 𝜒
4337, 42pm3.2ni 898 . . . 4 ¬ ((𝜇𝜆) ∨ 𝜒)
4433, 43aibnbaif 40375 . . 3 (jch ↔ ⊥)
4531, 44pm3.2i 471 . 2 ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥))
4645a1i 11 1 ((((((((((((((((𝜑 ↔ (𝜃𝜏)) ∧ (𝜓 ↔ (𝜂𝜁))) ∧ (𝜒 ↔ (𝜎𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃𝜏) ⊻ (𝜃𝜏)))) ∧ (jph ↔ ((𝜂𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ⊻ wxo 1461  ⊤wtru 1481  ⊥wfal 1485 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 197  df-or 385  df-an 386  df-xor 1462  df-tru 1483  df-fal 1486 This theorem is referenced by:  mdandysum2p2e4  40467
 Copyright terms: Public domain W3C validator