Theorem dandysum2p2e4 44380

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 215	. . . . . 6 ⊢ (𝜅 → ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))
3		dandysum2p2e4.d	. . . . . . . . . 10 ⊢ (𝜃 ↔ ⊥)
4		dandysum2p2e4.e	. . . . . . . . . 10 ⊢ (𝜏 ↔ ⊥)
5	3, 4	bothfbothsame 44282	. . . . . . . . 9 ⊢ (𝜃 ↔ 𝜏)
6	5	aisbnaxb 44293	. . . . . . . 8 ⊢ ¬ (𝜃 ⊻ 𝜏)
7	3	aisfina 44280	. . . . . . . . 9 ⊢ ¬ 𝜃
8	7	notatnand 44278	. . . . . . . 8 ⊢ ¬ (𝜃 ∧ 𝜏)
9	6, 8	2false 375	. . . . . . 7 ⊢ ((𝜃 ⊻ 𝜏) ↔ (𝜃 ∧ 𝜏))
10	9	aisbnaxb 44293	. . . . . 6 ⊢ ¬ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏))
11	2, 10	aibnbaif 44289	. . . . 5 ⊢ (𝜅 ↔ ⊥)
12		dandysum2p2e4.m	. . . . . . 7 ⊢ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))
13	12	biimpi 215	. . . . . 6 ⊢ (jph → ((𝜂 ⊻ 𝜁) ∨ 𝜑))
14		dandysum2p2e4.f	. . . . . . . . 9 ⊢ (𝜂 ↔ ⊤)
15		dandysum2p2e4.g	. . . . . . . . 9 ⊢ (𝜁 ↔ ⊤)
16	14, 15	bothtbothsame 44281	. . . . . . . 8 ⊢ (𝜂 ↔ 𝜁)
17	16	aisbnaxb 44293	. . . . . . 7 ⊢ ¬ (𝜂 ⊻ 𝜁)
18		dandysum2p2e4.a	. . . . . . . 8 ⊢ (𝜑 ↔ (𝜃 ∧ 𝜏))
19	8, 18	mtbir 322	. . . . . . 7 ⊢ ¬ 𝜑
20	17, 19	pm3.2ni 877	. . . . . 6 ⊢ ¬ ((𝜂 ⊻ 𝜁) ∨ 𝜑)
21	13, 20	aibnbaif 44289	. . . . 5 ⊢ (jph ↔ ⊥)
22	11, 21	pm3.2i 470	. . . 4 ⊢ ((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥))
23		dandysum2p2e4.n	. . . . 5 ⊢ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))
24		dandysum2p2e4.b	. . . . . . . . 9 ⊢ (𝜓 ↔ (𝜂 ∧ 𝜁))
25	14, 15	astbstanbst 44291	. . . . . . . . 9 ⊢ ((𝜂 ∧ 𝜁) ↔ ⊤)
26	24, 25	aiffbbtat 44283	. . . . . . . 8 ⊢ (𝜓 ↔ ⊤)
27	26	aistia 44279	. . . . . . 7 ⊢ 𝜓
28	27	olci 862	. . . . . 6 ⊢ ((𝜎 ⊻ 𝜌) ∨ 𝜓)
29	28	bitru 1548	. . . . 5 ⊢ (((𝜎 ⊻ 𝜌) ∨ 𝜓) ↔ ⊤)
30	23, 29	aiffbbtat 44283	. . . 4 ⊢ (jps ↔ ⊤)
31	22, 30	pm3.2i 470	. . 3 ⊢ (((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤))
32		dandysum2p2e4.o	. . . . 5 ⊢ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))
33	32	biimpi 215	. . . 4 ⊢ (jch → ((𝜇 ⊻ 𝜆) ∨ 𝜒))
34		dandysum2p2e4.j	. . . . . . 7 ⊢ (𝜇 ↔ ⊥)
35		dandysum2p2e4.k	. . . . . . 7 ⊢ (𝜆 ↔ ⊥)
36	34, 35	bothfbothsame 44282	. . . . . 6 ⊢ (𝜇 ↔ 𝜆)
37	36	aisbnaxb 44293	. . . . 5 ⊢ ¬ (𝜇 ⊻ 𝜆)
38		dandysum2p2e4.h	. . . . . . . 8 ⊢ (𝜎 ↔ ⊥)
39	38	aisfina 44280	. . . . . . 7 ⊢ ¬ 𝜎
40	39	notatnand 44278	. . . . . 6 ⊢ ¬ (𝜎 ∧ 𝜌)
41		dandysum2p2e4.c	. . . . . 6 ⊢ (𝜒 ↔ (𝜎 ∧ 𝜌))
42	40, 41	mtbir 322	. . . . 5 ⊢ ¬ 𝜒
43	37, 42	pm3.2ni 877	. . . 4 ⊢ ¬ ((𝜇 ⊻ 𝜆) ∨ 𝜒)
44	33, 43	aibnbaif 44289	. . 3 ⊢ (jch ↔ ⊥)
45	31, 44	pm3.2i 470	. 2 ⊢ ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥))
46	45	a1i 11	1 ⊢ ((((((((((((((((𝜑 ↔ (𝜃 ∧ 𝜏)) ∧ (𝜓 ↔ (𝜂 ∧ 𝜁))) ∧ (𝜒 ↔ (𝜎 ∧ 𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))) ∧ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   ⊻ wxo 1503  ⊤wtru 1540  ⊥wfal 1551

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 844  df-xor 1504  df-tru 1542  df-fal 1552

This theorem is referenced by:  mdandysum2p2e4  44381