Metamath Proof Explorer


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

Ref Expression
Hypotheses 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 dandysum2p2e4 ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ↔ ( 𝜃𝜏 ) ) ∧ ( 𝜓 ↔ ( 𝜂𝜁 ) ) ) ∧ ( 𝜒 ↔ ( 𝜎𝜌 ) ) ) ∧ ( 𝜃 ↔ ⊥ ) ) ∧ ( 𝜏 ↔ ⊥ ) ) ∧ ( 𝜂 ↔ ⊤ ) ) ∧ ( 𝜁 ↔ ⊤ ) ) ∧ ( 𝜎 ↔ ⊥ ) ) ∧ ( 𝜌 ↔ ⊥ ) ) ∧ ( 𝜇 ↔ ⊥ ) ) ∧ ( 𝜆 ↔ ⊥ ) ) ∧ ( 𝜅 ↔ ( ( 𝜃𝜏 ) ⊻ ( 𝜃𝜏 ) ) ) ) ∧ ( jph ↔ ( ( 𝜂𝜁 ) ∨ 𝜑 ) ) ) ∧ ( jps ↔ ( ( 𝜎𝜌 ) ∨ 𝜓 ) ) ) ∧ ( jch ↔ ( ( 𝜇𝜆 ) ∨ 𝜒 ) ) ) → ( ( ( ( 𝜅 ↔ ⊥ ) ∧ ( jph ↔ ⊥ ) ) ∧ ( jps ↔ ⊤ ) ) ∧ ( jch ↔ ⊥ ) ) )

Proof

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