Theorem mdandysum2p2e4 46008

Description: CONTRADICTION PROVED AT 1 + 1 = 2 . Luckily Mario Carneiro did a successful version of his own.

See Mario's Relevant Work: 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 would 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

Step	Hyp	Ref	Expression
1		mdandysum2p2e4.a	. 2 ⊢ (𝜑 ↔ (𝜃 ∧ 𝜏))
2		mdandysum2p2e4.b	. 2 ⊢ (𝜓 ↔ (𝜂 ∧ 𝜁))
3		mdandysum2p2e4.c	. 2 ⊢ (𝜒 ↔ (𝜎 ∧ 𝜌))
4		mdandysum2p2e4.d	. . 3 ⊢ (𝜃 ↔ jth)
5		mdandysum2p2e4.1	. . 3 ⊢ (jth ↔ ⊥)
6	4, 5	aisbbisfaisf 45911	. 2 ⊢ (𝜃 ↔ ⊥)
7		mdandysum2p2e4.e	. . 3 ⊢ (𝜏 ↔ jth)
8	7, 5	aisbbisfaisf 45911	. 2 ⊢ (𝜏 ↔ ⊥)
9		mdandysum2p2e4.f	. . 3 ⊢ (𝜂 ↔ jta)
10		mdandysum2p2e4.2	. . 3 ⊢ (jta ↔ ⊤)
11	9, 10	aiffbbtat 45910	. 2 ⊢ (𝜂 ↔ ⊤)
12		mdandysum2p2e4.g	. . 3 ⊢ (𝜁 ↔ jta)
13	12, 10	aiffbbtat 45910	. 2 ⊢ (𝜁 ↔ ⊤)
14		mdandysum2p2e4.h	. . 3 ⊢ (𝜎 ↔ jth)
15	14, 5	aisbbisfaisf 45911	. 2 ⊢ (𝜎 ↔ ⊥)
16		mdandysum2p2e4.i	. . 3 ⊢ (𝜌 ↔ jth)
17	16, 5	aisbbisfaisf 45911	. 2 ⊢ (𝜌 ↔ ⊥)
18		mdandysum2p2e4.j	. . 3 ⊢ (𝜇 ↔ jth)
19	18, 5	aisbbisfaisf 45911	. 2 ⊢ (𝜇 ↔ ⊥)
20		mdandysum2p2e4.k	. . 3 ⊢ (𝜆 ↔ jth)
21	20, 5	aisbbisfaisf 45911	. 2 ⊢ (𝜆 ↔ ⊥)
22		mdandysum2p2e4.l	. 2 ⊢ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))
23		mdandysum2p2e4.m	. 2 ⊢ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))
24		mdandysum2p2e4.n	. 2 ⊢ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))
25		mdandysum2p2e4.o	. 2 ⊢ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))
26	1, 2, 3, 6, 8, 11, 13, 15, 17, 19, 21, 22, 23, 24, 25	dandysum2p2e4 46007	1 ⊢ ((((((((((((((((𝜑 ↔ (𝜃 ∧ 𝜏)) ∧ (𝜓 ↔ (𝜂 ∧ 𝜁))) ∧ (𝜒 ↔ (𝜎 ∧ 𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))) ∧ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   ⊻ wxo 1508  ⊤wtru 1541  ⊥wfal 1552

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 206  df-an 396  df-or 845  df-xor 1509  df-tru 1543  df-fal 1553

This theorem is referenced by: (None)