Theorem dandysum2p2e4

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)

	Ref	Expression
Hypotheses	dandysum2p2e4.a	$$⊢\phi \leftrightarrow \left(\theta \wedge \tau \right)$$
	dandysum2p2e4.b	$$⊢\psi \leftrightarrow \left(\eta \wedge \zeta \right)$$
	dandysum2p2e4.c	$$⊢\chi \leftrightarrow \left(\sigma \wedge \rho \right)$$
	dandysum2p2e4.d	$$⊢\theta \leftrightarrow \perp$$
	dandysum2p2e4.e	$$⊢\tau \leftrightarrow \perp$$
	dandysum2p2e4.f	$$⊢\eta \leftrightarrow \top$$
	dandysum2p2e4.g	$$⊢\zeta \leftrightarrow \top$$
	dandysum2p2e4.h	$$⊢\sigma \leftrightarrow \perp$$
	dandysum2p2e4.i	$$⊢\rho \leftrightarrow \perp$$
	dandysum2p2e4.j	$$⊢\mu \leftrightarrow \perp$$
	dandysum2p2e4.k	$$⊢\lambda \leftrightarrow \perp$$
	dandysum2p2e4.l	$$⊢\kappa \leftrightarrow \left(\left(\theta ⊻\tau \right)⊻\left(\theta \wedge \tau \right)\right)$$
	dandysum2p2e4.m	No typesetting found for |- ( jph <-> ( ( et \/_ ze ) \/ ph ) ) with typecode |-
	dandysum2p2e4.n	No typesetting found for |- ( jps <-> ( ( si \/_ rh ) \/ ps ) ) with typecode |-
	dandysum2p2e4.o	No typesetting found for |- ( jch <-> ( ( mu \/_ la ) \/ ch ) ) with typecode |-
Assertion	dandysum2p2e4	Could not format assertion : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph <-> ( th /\ ta ) ) /\ ( ps <-> ( et /\ ze ) ) ) /\ ( ch <-> ( si /\ rh ) ) ) /\ ( th <-> F. ) ) /\ ( ta <-> F. ) ) /\ ( et <-> T. ) ) /\ ( ze <-> T. ) ) /\ ( si <-> F. ) ) /\ ( rh <-> F. ) ) /\ ( mu <-> F. ) ) /\ ( la <-> F. ) ) /\ ( ka <-> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) ) ) /\ ( jph <-> ( ( et \/_ ze ) \/ ph ) ) ) /\ ( jps <-> ( ( si \/_ rh ) \/ ps ) ) ) /\ ( jch <-> ( ( mu \/_ la ) \/ ch ) ) ) -> ( ( ( ( ka <-> F. ) /\ ( jph <-> F. ) ) /\ ( jps <-> T. ) ) /\ ( jch <-> F. ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dandysum2p2e4.a	$$⊢\phi \leftrightarrow \left(\theta \wedge \tau \right)$$
2		dandysum2p2e4.b	$$⊢\psi \leftrightarrow \left(\eta \wedge \zeta \right)$$
3		dandysum2p2e4.c	$$⊢\chi \leftrightarrow \left(\sigma \wedge \rho \right)$$
4		dandysum2p2e4.d	$$⊢\theta \leftrightarrow \perp$$
5		dandysum2p2e4.e	$$⊢\tau \leftrightarrow \perp$$
6		dandysum2p2e4.f	$$⊢\eta \leftrightarrow \top$$
7		dandysum2p2e4.g	$$⊢\zeta \leftrightarrow \top$$
8		dandysum2p2e4.h	$$⊢\sigma \leftrightarrow \perp$$
9		dandysum2p2e4.i	$$⊢\rho \leftrightarrow \perp$$
10		dandysum2p2e4.j	$$⊢\mu \leftrightarrow \perp$$
11		dandysum2p2e4.k	$$⊢\lambda \leftrightarrow \perp$$
12		dandysum2p2e4.l	$$⊢\kappa \leftrightarrow \left(\left(\theta ⊻\tau \right)⊻\left(\theta \wedge \tau \right)\right)$$
13		dandysum2p2e4.m	Could not format ( jph <-> ( ( et \/_ ze ) \/ ph ) ) : No typesetting found for |- ( jph <-> ( ( et \/_ ze ) \/ ph ) ) with typecode |-
14		dandysum2p2e4.n	Could not format ( jps <-> ( ( si \/_ rh ) \/ ps ) ) : No typesetting found for |- ( jps <-> ( ( si \/_ rh ) \/ ps ) ) with typecode |-
15		dandysum2p2e4.o	Could not format ( jch <-> ( ( mu \/_ la ) \/ ch ) ) : No typesetting found for |- ( jch <-> ( ( mu \/_ la ) \/ ch ) ) with typecode |-
16	12	biimpi	$$⊢\kappa \to \left(\left(\theta ⊻\tau \right)⊻\left(\theta \wedge \tau \right)\right)$$
17	4 5	bothfbothsame	$$⊢\theta \leftrightarrow \tau$$
18	17	aisbnaxb	$$⊢\neg \left(\theta ⊻\tau \right)$$
19	4	aisfina	$$⊢\neg \theta$$
20	19	notatnand	$$⊢\neg \left(\theta \wedge \tau \right)$$
21	18 20	2false	$$⊢\left(\theta ⊻\tau \right)\leftrightarrow \left(\theta \wedge \tau \right)$$
22	21	aisbnaxb	$$⊢\neg \left(\left(\theta ⊻\tau \right)⊻\left(\theta \wedge \tau \right)\right)$$
23	16 22	aibnbaif	$$⊢\kappa \leftrightarrow \perp$$
24	13	biimpi	Could not format ( jph -> ( ( et \/_ ze ) \/ ph ) ) : No typesetting found for |- ( jph -> ( ( et \/_ ze ) \/ ph ) ) with typecode |-
25	6 7	bothtbothsame	$$⊢\eta \leftrightarrow \zeta$$
26	25	aisbnaxb	$$⊢\neg \left(\eta ⊻\zeta \right)$$
27	20 1	mtbir	$$⊢\neg \phi$$
28	26 27	pm3.2ni	$$⊢\neg \left(\left(\eta ⊻\zeta \right)\vee \phi \right)$$
29	24 28	aibnbaif	Could not format ( jph <-> F. ) : No typesetting found for |- ( jph <-> F. ) with typecode |-
30	23 29	pm3.2i	Could not format ( ( ka <-> F. ) /\ ( jph <-> F. ) ) : No typesetting found for |- ( ( ka <-> F. ) /\ ( jph <-> F. ) ) with typecode |-
31	6 7	astbstanbst	$$⊢\left(\eta \wedge \zeta \right)\leftrightarrow \top$$
32	2 31	aiffbbtat	$$⊢\psi \leftrightarrow \top$$
33	32	aistia	$$⊢\psi$$
34	33	olci	$$⊢\left(\left(\sigma ⊻\rho \right)\vee \psi \right)$$
35	34	bitru	$$⊢\left(\left(\sigma ⊻\rho \right)\vee \psi \right)\leftrightarrow \top$$
36	14 35	aiffbbtat	Could not format ( jps <-> T. ) : No typesetting found for |- ( jps <-> T. ) with typecode |-
37	30 36	pm3.2i	Could not format ( ( ( ka <-> F. ) /\ ( jph <-> F. ) ) /\ ( jps <-> T. ) ) : No typesetting found for |- ( ( ( ka <-> F. ) /\ ( jph <-> F. ) ) /\ ( jps <-> T. ) ) with typecode |-
38	15	biimpi	Could not format ( jch -> ( ( mu \/_ la ) \/ ch ) ) : No typesetting found for |- ( jch -> ( ( mu \/_ la ) \/ ch ) ) with typecode |-
39	10 11	bothfbothsame	$$⊢\mu \leftrightarrow \lambda$$
40	39	aisbnaxb	$$⊢\neg \left(\mu ⊻\lambda \right)$$
41	8	aisfina	$$⊢\neg \sigma$$
42	41	notatnand	$$⊢\neg \left(\sigma \wedge \rho \right)$$
43	42 3	mtbir	$$⊢\neg \chi$$
44	40 43	pm3.2ni	$$⊢\neg \left(\left(\mu ⊻\lambda \right)\vee \chi \right)$$
45	38 44	aibnbaif	Could not format ( jch <-> F. ) : No typesetting found for |- ( jch <-> F. ) with typecode |-
46	37 45	pm3.2i	Could not format ( ( ( ( ka <-> F. ) /\ ( jph <-> F. ) ) /\ ( jps <-> T. ) ) /\ ( jch <-> F. ) ) : No typesetting found for |- ( ( ( ( ka <-> F. ) /\ ( jph <-> F. ) ) /\ ( jps <-> T. ) ) /\ ( jch <-> F. ) ) with typecode |-
47	46	a1i	Could not format ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph <-> ( th /\ ta ) ) /\ ( ps <-> ( et /\ ze ) ) ) /\ ( ch <-> ( si /\ rh ) ) ) /\ ( th <-> F. ) ) /\ ( ta <-> F. ) ) /\ ( et <-> T. ) ) /\ ( ze <-> T. ) ) /\ ( si <-> F. ) ) /\ ( rh <-> F. ) ) /\ ( mu <-> F. ) ) /\ ( la <-> F. ) ) /\ ( ka <-> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) ) ) /\ ( jph <-> ( ( et \/_ ze ) \/ ph ) ) ) /\ ( jps <-> ( ( si \/_ rh ) \/ ps ) ) ) /\ ( jch <-> ( ( mu \/_ la ) \/ ch ) ) ) -> ( ( ( ( ka <-> F. ) /\ ( jph <-> F. ) ) /\ ( jps <-> T. ) ) /\ ( jch <-> F. ) ) ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph <-> ( th /\ ta ) ) /\ ( ps <-> ( et /\ ze ) ) ) /\ ( ch <-> ( si /\ rh ) ) ) /\ ( th <-> F. ) ) /\ ( ta <-> F. ) ) /\ ( et <-> T. ) ) /\ ( ze <-> T. ) ) /\ ( si <-> F. ) ) /\ ( rh <-> F. ) ) /\ ( mu <-> F. ) ) /\ ( la <-> F. ) ) /\ ( ka <-> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) ) ) /\ ( jph <-> ( ( et \/_ ze ) \/ ph ) ) ) /\ ( jps <-> ( ( si \/_ rh ) \/ ps ) ) ) /\ ( jch <-> ( ( mu \/_ la ) \/ ch ) ) ) -> ( ( ( ( ka <-> F. ) /\ ( jph <-> F. ) ) /\ ( jps <-> T. ) ) /\ ( jch <-> F. ) ) ) with typecode |-