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 | ⊢ ( 𝜑 ↔ ( 𝜃 ∧ 𝜏 ) ) | |
| 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 ↔ ⊥ ) ) ) |