Mathbox for Jarvin Udandy |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > mdandysum2p2e4 | Structured version Visualization version GIF version |
Description: CONTRADICTION PROVED AT 1
+ 1 = 2 . Luckily Mario Carneiro did a
successful version of his own.
See Mario's Relevant Work: 1.3.14 Half adder and full adder in propositional calculus. 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. In mdandysum2p2e4, one might imagine what jth or jta could be then do the math with their truths. Also limited to the restriction jth, jta are having opposite truths equivalent to the stated truth constants. (Contributed by Jarvin Udandy, 6-Sep-2016.) |
Ref | Expression |
---|---|
mdandysum2p2e4.1 | ⊢ (jth ↔ ⊥) |
mdandysum2p2e4.2 | ⊢ (jta ↔ ⊤) |
mdandysum2p2e4.a | ⊢ (𝜑 ↔ (𝜃 ∧ 𝜏)) |
mdandysum2p2e4.b | ⊢ (𝜓 ↔ (𝜂 ∧ 𝜁)) |
mdandysum2p2e4.c | ⊢ (𝜒 ↔ (𝜎 ∧ 𝜌)) |
mdandysum2p2e4.d | ⊢ (𝜃 ↔ jth) |
mdandysum2p2e4.e | ⊢ (𝜏 ↔ jth) |
mdandysum2p2e4.f | ⊢ (𝜂 ↔ jta) |
mdandysum2p2e4.g | ⊢ (𝜁 ↔ jta) |
mdandysum2p2e4.h | ⊢ (𝜎 ↔ jth) |
mdandysum2p2e4.i | ⊢ (𝜌 ↔ jth) |
mdandysum2p2e4.j | ⊢ (𝜇 ↔ jth) |
mdandysum2p2e4.k | ⊢ (𝜆 ↔ jth) |
mdandysum2p2e4.l | ⊢ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏))) |
mdandysum2p2e4.m | ⊢ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑)) |
mdandysum2p2e4.n | ⊢ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓)) |
mdandysum2p2e4.o | ⊢ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒)) |
Ref | Expression |
---|---|
mdandysum2p2e4 | ⊢ ((((((((((((((((𝜑 ↔ (𝜃 ∧ 𝜏)) ∧ (𝜓 ↔ (𝜂 ∧ 𝜁))) ∧ (𝜒 ↔ (𝜎 ∧ 𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))) ∧ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mdandysum2p2e4.a | . 2 ⊢ (𝜑 ↔ (𝜃 ∧ 𝜏)) | |
2 | mdandysum2p2e4.b | . 2 ⊢ (𝜓 ↔ (𝜂 ∧ 𝜁)) | |
3 | mdandysum2p2e4.c | . 2 ⊢ (𝜒 ↔ (𝜎 ∧ 𝜌)) | |
4 | mdandysum2p2e4.d | . . 3 ⊢ (𝜃 ↔ jth) | |
5 | mdandysum2p2e4.1 | . . 3 ⊢ (jth ↔ ⊥) | |
6 | 4, 5 | aisbbisfaisf 43137 | . 2 ⊢ (𝜃 ↔ ⊥) |
7 | mdandysum2p2e4.e | . . 3 ⊢ (𝜏 ↔ jth) | |
8 | 7, 5 | aisbbisfaisf 43137 | . 2 ⊢ (𝜏 ↔ ⊥) |
9 | mdandysum2p2e4.f | . . 3 ⊢ (𝜂 ↔ jta) | |
10 | mdandysum2p2e4.2 | . . 3 ⊢ (jta ↔ ⊤) | |
11 | 9, 10 | aiffbbtat 43136 | . 2 ⊢ (𝜂 ↔ ⊤) |
12 | mdandysum2p2e4.g | . . 3 ⊢ (𝜁 ↔ jta) | |
13 | 12, 10 | aiffbbtat 43136 | . 2 ⊢ (𝜁 ↔ ⊤) |
14 | mdandysum2p2e4.h | . . 3 ⊢ (𝜎 ↔ jth) | |
15 | 14, 5 | aisbbisfaisf 43137 | . 2 ⊢ (𝜎 ↔ ⊥) |
16 | mdandysum2p2e4.i | . . 3 ⊢ (𝜌 ↔ jth) | |
17 | 16, 5 | aisbbisfaisf 43137 | . 2 ⊢ (𝜌 ↔ ⊥) |
18 | mdandysum2p2e4.j | . . 3 ⊢ (𝜇 ↔ jth) | |
19 | 18, 5 | aisbbisfaisf 43137 | . 2 ⊢ (𝜇 ↔ ⊥) |
20 | mdandysum2p2e4.k | . . 3 ⊢ (𝜆 ↔ jth) | |
21 | 20, 5 | aisbbisfaisf 43137 | . 2 ⊢ (𝜆 ↔ ⊥) |
22 | mdandysum2p2e4.l | . 2 ⊢ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏))) | |
23 | mdandysum2p2e4.m | . 2 ⊢ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑)) | |
24 | mdandysum2p2e4.n | . 2 ⊢ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓)) | |
25 | mdandysum2p2e4.o | . 2 ⊢ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒)) | |
26 | 1, 2, 3, 6, 8, 11, 13, 15, 17, 19, 21, 22, 23, 24, 25 | dandysum2p2e4 43233 | 1 ⊢ ((((((((((((((((𝜑 ↔ (𝜃 ∧ 𝜏)) ∧ (𝜓 ↔ (𝜂 ∧ 𝜁))) ∧ (𝜒 ↔ (𝜎 ∧ 𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))) ∧ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 ⊻ wxo 1500 ⊤wtru 1534 ⊥wfal 1545 |
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 1501 df-tru 1536 df-fal 1546 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |