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

Theorem mdandysum2p2e4 41589
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 adder and full adder 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 41492 . 2 (𝜃 ↔ ⊥)
7 mdandysum2p2e4.e . . 3 (𝜏jth)
87, 5aisbbisfaisf 41492 . 2 (𝜏 ↔ ⊥)
9 mdandysum2p2e4.f . . 3 (𝜂jta)
10 mdandysum2p2e4.2 . . 3 (jta ↔ ⊤)
119, 10aiffbbtat 41491 . 2 (𝜂 ↔ ⊤)
12 mdandysum2p2e4.g . . 3 (𝜁jta)
1312, 10aiffbbtat 41491 . 2 (𝜁 ↔ ⊤)
14 mdandysum2p2e4.h . . 3 (𝜎jth)
1514, 5aisbbisfaisf 41492 . 2 (𝜎 ↔ ⊥)
16 mdandysum2p2e4.i . . 3 (𝜌jth)
1716, 5aisbbisfaisf 41492 . 2 (𝜌 ↔ ⊥)
18 mdandysum2p2e4.j . . 3 (𝜇jth)
1918, 5aisbbisfaisf 41492 . 2 (𝜇 ↔ ⊥)
20 mdandysum2p2e4.k . . 3 (𝜆jth)
2120, 5aisbbisfaisf 41492 . 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 41588 1 ((((((((((((((((𝜑 ↔ (𝜃𝜏)) ∧ (𝜓 ↔ (𝜂𝜁))) ∧ (𝜒 ↔ (𝜎𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃𝜏) ⊻ (𝜃𝜏)))) ∧ (jph ↔ ((𝜂𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382  wa 383  wxo 1577  wtru 1597  wfal 1601
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 384  df-an 385  df-xor 1578  df-tru 1599  df-fal 1602
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator