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