Theorem dandysum2p2e4 41165

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 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. (Contributed by Jarvin Udandy, 6-Sep-2016.)

Hypotheses

Ref	Expression
dandysum2p2e4.a	|- ( ph <-> ( th /\ ta ) )
dandysum2p2e4.b	|- ( ps <-> ( et /\ ze ) )
dandysum2p2e4.c	|- ( ch <-> ( si /\ rh ) )
dandysum2p2e4.d	|- ( th <-> F. )
dandysum2p2e4.e	|- ( ta <-> F. )
dandysum2p2e4.f	|- ( et <-> T. )
dandysum2p2e4.g	|- ( ze <-> T. )
dandysum2p2e4.h	|- ( si <-> F. )
dandysum2p2e4.i	|- ( rh <-> F. )
dandysum2p2e4.j	|- ( mu <-> F. )
dandysum2p2e4.k	|- ( la <-> F. )
dandysum2p2e4.l	|- ( ka <-> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) )
dandysum2p2e4.m	|- (jph <-> ( ( et \/_ ze ) \/ ph ) )
dandysum2p2e4.n	|- (jps <-> ( ( si \/_ rh ) \/ ps ) )
dandysum2p2e4.o	|- (jch <-> ( ( mu \/_ la ) \/ ch ) )

Assertion

Ref

Expression

dandysum2p2e4

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

Proof of Theorem dandysum2p2e4

Step	Hyp	Ref	Expression
1		dandysum2p2e4.l	. . . . . . 7 |- ( ka <-> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) )
2	1	biimpi 206	. . . . . 6 |- ( ka -> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) )
3		dandysum2p2e4.d	. . . . . . . . . 10 |- ( th <-> F. )
4		dandysum2p2e4.e	. . . . . . . . . 10 |- ( ta <-> F. )
5	3, 4	bothfbothsame 41067	. . . . . . . . 9 |- ( th <-> ta )
6	5	aisbnaxb 41078	. . . . . . . 8 |- -. ( th \/_ ta )
7	3	aisfina 41065	. . . . . . . . 9 |- -. th
8	7	notatnand 41063	. . . . . . . 8 |- -. ( th /\ ta )
9	6, 8	2false 365	. . . . . . 7 |- ( ( th \/_ ta ) <-> ( th /\ ta ) )
10	9	aisbnaxb 41078	. . . . . 6 |- -. ( ( th \/_ ta ) \/_ ( th /\ ta ) )
11	2, 10	aibnbaif 41074	. . . . 5 |- ( ka <-> F. )
12		dandysum2p2e4.m	. . . . . . 7 |- (jph <-> ( ( et \/_ ze ) \/ ph ) )
13	12	biimpi 206	. . . . . 6 |- (jph -> ( ( et \/_ ze ) \/ ph ) )
14		dandysum2p2e4.f	. . . . . . . . 9 |- ( et <-> T. )
15		dandysum2p2e4.g	. . . . . . . . 9 |- ( ze <-> T. )
16	14, 15	bothtbothsame 41066	. . . . . . . 8 |- ( et <-> ze )
17	16	aisbnaxb 41078	. . . . . . 7 |- -. ( et \/_ ze )
18		dandysum2p2e4.a	. . . . . . . 8 |- ( ph <-> ( th /\ ta ) )
19	8, 18	mtbir 313	. . . . . . 7 |- -. ph
20	17, 19	pm3.2ni 899	. . . . . 6 |- -. ( ( et \/_ ze ) \/ ph )
21	13, 20	aibnbaif 41074	. . . . 5 |- (jph <-> F. )
22	11, 21	pm3.2i 471	. . . 4 |- ( ( ka <-> F. ) /\ (jph <-> F. ) )
23		dandysum2p2e4.n	. . . . 5 |- (jps <-> ( ( si \/_ rh ) \/ ps ) )
24		dandysum2p2e4.b	. . . . . . . . 9 |- ( ps <-> ( et /\ ze ) )
25	14, 15	astbstanbst 41076	. . . . . . . . 9 |- ( ( et /\ ze ) <-> T. )
26	24, 25	aiffbbtat 41068	. . . . . . . 8 |- ( ps <-> T. )
27	26	aistia 41064	. . . . . . 7 |- ps
28	27	olci 406	. . . . . 6 |- ( ( si \/_ rh ) \/ ps )
29	28	bitru 1496	. . . . 5 |- ( ( ( si \/_ rh ) \/ ps ) <-> T. )
30	23, 29	aiffbbtat 41068	. . . 4 |- (jps <-> T. )
31	22, 30	pm3.2i 471	. . 3 |- ( ( ( ka <-> F. ) /\ (jph <-> F. ) ) /\ (jps <-> T. ) )
32		dandysum2p2e4.o	. . . . 5 |- (jch <-> ( ( mu \/_ la ) \/ ch ) )
33	32	biimpi 206	. . . 4 |- (jch -> ( ( mu \/_ la ) \/ ch ) )
34		dandysum2p2e4.j	. . . . . . 7 |- ( mu <-> F. )
35		dandysum2p2e4.k	. . . . . . 7 |- ( la <-> F. )
36	34, 35	bothfbothsame 41067	. . . . . 6 |- ( mu <-> la )
37	36	aisbnaxb 41078	. . . . 5 |- -. ( mu \/_ la )
38		dandysum2p2e4.h	. . . . . . . 8 |- ( si <-> F. )
39	38	aisfina 41065	. . . . . . 7 |- -. si
40	39	notatnand 41063	. . . . . 6 |- -. ( si /\ rh )
41		dandysum2p2e4.c	. . . . . 6 |- ( ch <-> ( si /\ rh ) )
42	40, 41	mtbir 313	. . . . 5 |- -. ch
43	37, 42	pm3.2ni 899	. . . 4 |- -. ( ( mu \/_ la ) \/ ch )
44	33, 43	aibnbaif 41074	. . 3 |- (jch <-> F. )
45	31, 44	pm3.2i 471	. 2 |- ( ( ( ( ka <-> F. ) /\ (jph <-> F. ) ) /\ (jps <-> T. ) ) /\ (jch <-> F. ) )
46	45	a1i 11	1 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 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. ) ) )

Syntax hints:   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   \/_ wxo 1464   T. wtru 1484   F. wfal 1488

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 385  df-an 386  df-xor 1465  df-tru 1486  df-fal 1489

This theorem is referenced by:  mdandysum2p2e4  41166