Theorem dandysum2p2e4 48067

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 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. (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

Step	Hyp	Ref	Expression
1		dandysum2p2e4.l	. . . . . . 7 ⊢ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))
2	1	biimpi 219	. . . . . 6 ⊢ (𝜅 → ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))
3		dandysum2p2e4.d	. . . . . . . . . 10 ⊢ (𝜃 ↔ ⊥)
4		dandysum2p2e4.e	. . . . . . . . . 10 ⊢ (𝜏 ↔ ⊥)
5	3, 4	bothfbothsame 47969	. . . . . . . . 9 ⊢ (𝜃 ↔ 𝜏)
6	5	aisbnaxb 47980	. . . . . . . 8 ⊢ ¬ (𝜃 ⊻ 𝜏)
7	3	aisfina 47967	. . . . . . . . 9 ⊢ ¬ 𝜃
8	7	notatnand 47965	. . . . . . . 8 ⊢ ¬ (𝜃 ∧ 𝜏)
9	6, 8	2false 378	. . . . . . 7 ⊢ ((𝜃 ⊻ 𝜏) ↔ (𝜃 ∧ 𝜏))
10	9	aisbnaxb 47980	. . . . . 6 ⊢ ¬ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏))
11	2, 10	aibnbaif 47976	. . . . 5 ⊢ (𝜅 ↔ ⊥)
12		dandysum2p2e4.m	. . . . . . 7 ⊢ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))
13	12	biimpi 219	. . . . . 6 ⊢ (jph → ((𝜂 ⊻ 𝜁) ∨ 𝜑))
14		dandysum2p2e4.f	. . . . . . . . 9 ⊢ (𝜂 ↔ ⊤)
15		dandysum2p2e4.g	. . . . . . . . 9 ⊢ (𝜁 ↔ ⊤)
16	14, 15	bothtbothsame 47968	. . . . . . . 8 ⊢ (𝜂 ↔ 𝜁)
17	16	aisbnaxb 47980	. . . . . . 7 ⊢ ¬ (𝜂 ⊻ 𝜁)
18		dandysum2p2e4.a	. . . . . . . 8 ⊢ (𝜑 ↔ (𝜃 ∧ 𝜏))
19	8, 18	mtbir 326	. . . . . . 7 ⊢ ¬ 𝜑
20	17, 19	pm3.2ni 894	. . . . . 6 ⊢ ¬ ((𝜂 ⊻ 𝜁) ∨ 𝜑)
21	13, 20	aibnbaif 47976	. . . . 5 ⊢ (jph ↔ ⊥)
22	11, 21	pm3.2i 476	. . . 4 ⊢ ((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥))
23		dandysum2p2e4.n	. . . . 5 ⊢ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))
24		dandysum2p2e4.b	. . . . . . . . 9 ⊢ (𝜓 ↔ (𝜂 ∧ 𝜁))
25	14, 15	astbstanbst 47978	. . . . . . . . 9 ⊢ ((𝜂 ∧ 𝜁) ↔ ⊤)
26	24, 25	aiffbbtat 47970	. . . . . . . 8 ⊢ (𝜓 ↔ ⊤)
27	26	aistia 47966	. . . . . . 7 ⊢ 𝜓
28	27	olci 880	. . . . . 6 ⊢ ((𝜎 ⊻ 𝜌) ∨ 𝜓)
29	28	bitru 1579	. . . . 5 ⊢ (((𝜎 ⊻ 𝜌) ∨ 𝜓) ↔ ⊤)
30	23, 29	aiffbbtat 47970	. . . 4 ⊢ (jps ↔ ⊤)
31	22, 30	pm3.2i 476	. . 3 ⊢ (((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤))
32		dandysum2p2e4.o	. . . . 5 ⊢ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))
33	32	biimpi 219	. . . 4 ⊢ (jch → ((𝜇 ⊻ 𝜆) ∨ 𝜒))
34		dandysum2p2e4.j	. . . . . . 7 ⊢ (𝜇 ↔ ⊥)
35		dandysum2p2e4.k	. . . . . . 7 ⊢ (𝜆 ↔ ⊥)
36	34, 35	bothfbothsame 47969	. . . . . 6 ⊢ (𝜇 ↔ 𝜆)
37	36	aisbnaxb 47980	. . . . 5 ⊢ ¬ (𝜇 ⊻ 𝜆)
38		dandysum2p2e4.h	. . . . . . . 8 ⊢ (𝜎 ↔ ⊥)
39	38	aisfina 47967	. . . . . . 7 ⊢ ¬ 𝜎
40	39	notatnand 47965	. . . . . 6 ⊢ ¬ (𝜎 ∧ 𝜌)
41		dandysum2p2e4.c	. . . . . 6 ⊢ (𝜒 ↔ (𝜎 ∧ 𝜌))
42	40, 41	mtbir 326	. . . . 5 ⊢ ¬ 𝜒
43	37, 42	pm3.2ni 894	. . . 4 ⊢ ¬ ((𝜇 ⊻ 𝜆) ∨ 𝜒)
44	33, 43	aibnbaif 47976	. . 3 ⊢ (jch ↔ ⊥)
45	31, 44	pm3.2i 476	. 2 ⊢ ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥))
46	45	a1i 11	1 ⊢ ((((((((((((((((𝜑 ↔ (𝜃 ∧ 𝜏)) ∧ (𝜓 ↔ (𝜂 ∧ 𝜁))) ∧ (𝜒 ↔ (𝜎 ∧ 𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))) ∧ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ⊻ wxo 1541  ⊤wtru 1571  ⊥wfal 1582

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-xor 1542  df-tru 1573  df-fal 1583

This theorem is used by:  mdandysum2p2e4  48068