Mathbox for Jarvin Udandy |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > dandysum2p2e4 | Structured version Visualization version GIF version |
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 |
---|---|
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 ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒)) |
Ref | Expression |
---|---|
dandysum2p2e4 | ⊢ ((((((((((((((((𝜑 ↔ (𝜃 ∧ 𝜏)) ∧ (𝜓 ↔ (𝜂 ∧ 𝜁))) ∧ (𝜒 ↔ (𝜎 ∧ 𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))) ∧ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dandysum2p2e4.l | . . . . . . 7 ⊢ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏))) | |
2 | 1 | biimpi 218 | . . . . . 6 ⊢ (𝜅 → ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏))) |
3 | dandysum2p2e4.d | . . . . . . . . . 10 ⊢ (𝜃 ↔ ⊥) | |
4 | dandysum2p2e4.e | . . . . . . . . . 10 ⊢ (𝜏 ↔ ⊥) | |
5 | 3, 4 | bothfbothsame 43156 | . . . . . . . . 9 ⊢ (𝜃 ↔ 𝜏) |
6 | 5 | aisbnaxb 43167 | . . . . . . . 8 ⊢ ¬ (𝜃 ⊻ 𝜏) |
7 | 3 | aisfina 43154 | . . . . . . . . 9 ⊢ ¬ 𝜃 |
8 | 7 | notatnand 43152 | . . . . . . . 8 ⊢ ¬ (𝜃 ∧ 𝜏) |
9 | 6, 8 | 2false 378 | . . . . . . 7 ⊢ ((𝜃 ⊻ 𝜏) ↔ (𝜃 ∧ 𝜏)) |
10 | 9 | aisbnaxb 43167 | . . . . . 6 ⊢ ¬ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)) |
11 | 2, 10 | aibnbaif 43163 | . . . . 5 ⊢ (𝜅 ↔ ⊥) |
12 | dandysum2p2e4.m | . . . . . . 7 ⊢ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑)) | |
13 | 12 | biimpi 218 | . . . . . 6 ⊢ (jph → ((𝜂 ⊻ 𝜁) ∨ 𝜑)) |
14 | dandysum2p2e4.f | . . . . . . . . 9 ⊢ (𝜂 ↔ ⊤) | |
15 | dandysum2p2e4.g | . . . . . . . . 9 ⊢ (𝜁 ↔ ⊤) | |
16 | 14, 15 | bothtbothsame 43155 | . . . . . . . 8 ⊢ (𝜂 ↔ 𝜁) |
17 | 16 | aisbnaxb 43167 | . . . . . . 7 ⊢ ¬ (𝜂 ⊻ 𝜁) |
18 | dandysum2p2e4.a | . . . . . . . 8 ⊢ (𝜑 ↔ (𝜃 ∧ 𝜏)) | |
19 | 8, 18 | mtbir 325 | . . . . . . 7 ⊢ ¬ 𝜑 |
20 | 17, 19 | pm3.2ni 877 | . . . . . 6 ⊢ ¬ ((𝜂 ⊻ 𝜁) ∨ 𝜑) |
21 | 13, 20 | aibnbaif 43163 | . . . . 5 ⊢ (jph ↔ ⊥) |
22 | 11, 21 | pm3.2i 473 | . . . 4 ⊢ ((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) |
23 | dandysum2p2e4.n | . . . . 5 ⊢ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓)) | |
24 | dandysum2p2e4.b | . . . . . . . . 9 ⊢ (𝜓 ↔ (𝜂 ∧ 𝜁)) | |
25 | 14, 15 | astbstanbst 43165 | . . . . . . . . 9 ⊢ ((𝜂 ∧ 𝜁) ↔ ⊤) |
26 | 24, 25 | aiffbbtat 43157 | . . . . . . . 8 ⊢ (𝜓 ↔ ⊤) |
27 | 26 | aistia 43153 | . . . . . . 7 ⊢ 𝜓 |
28 | 27 | olci 862 | . . . . . 6 ⊢ ((𝜎 ⊻ 𝜌) ∨ 𝜓) |
29 | 28 | bitru 1546 | . . . . 5 ⊢ (((𝜎 ⊻ 𝜌) ∨ 𝜓) ↔ ⊤) |
30 | 23, 29 | aiffbbtat 43157 | . . . 4 ⊢ (jps ↔ ⊤) |
31 | 22, 30 | pm3.2i 473 | . . 3 ⊢ (((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) |
32 | dandysum2p2e4.o | . . . . 5 ⊢ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒)) | |
33 | 32 | biimpi 218 | . . . 4 ⊢ (jch → ((𝜇 ⊻ 𝜆) ∨ 𝜒)) |
34 | dandysum2p2e4.j | . . . . . . 7 ⊢ (𝜇 ↔ ⊥) | |
35 | dandysum2p2e4.k | . . . . . . 7 ⊢ (𝜆 ↔ ⊥) | |
36 | 34, 35 | bothfbothsame 43156 | . . . . . 6 ⊢ (𝜇 ↔ 𝜆) |
37 | 36 | aisbnaxb 43167 | . . . . 5 ⊢ ¬ (𝜇 ⊻ 𝜆) |
38 | dandysum2p2e4.h | . . . . . . . 8 ⊢ (𝜎 ↔ ⊥) | |
39 | 38 | aisfina 43154 | . . . . . . 7 ⊢ ¬ 𝜎 |
40 | 39 | notatnand 43152 | . . . . . 6 ⊢ ¬ (𝜎 ∧ 𝜌) |
41 | dandysum2p2e4.c | . . . . . 6 ⊢ (𝜒 ↔ (𝜎 ∧ 𝜌)) | |
42 | 40, 41 | mtbir 325 | . . . . 5 ⊢ ¬ 𝜒 |
43 | 37, 42 | pm3.2ni 877 | . . . 4 ⊢ ¬ ((𝜇 ⊻ 𝜆) ∨ 𝜒) |
44 | 33, 43 | aibnbaif 43163 | . . 3 ⊢ (jch ↔ ⊥) |
45 | 31, 44 | pm3.2i 473 | . 2 ⊢ ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥)) |
46 | 45 | a1i 11 | 1 ⊢ ((((((((((((((((𝜑 ↔ (𝜃 ∧ 𝜏)) ∧ (𝜓 ↔ (𝜂 ∧ 𝜁))) ∧ (𝜒 ↔ (𝜎 ∧ 𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))) ∧ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 ⊻ wxo 1501 ⊤wtru 1538 ⊥wfal 1549 |
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 209 df-an 399 df-or 844 df-xor 1502 df-tru 1540 df-fal 1550 |
This theorem is referenced by: mdandysum2p2e4 43255 |
Copyright terms: Public domain | W3C validator |