![]() |
Mathbox for David A. Wheeler |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > 2p2ne5 | Structured version Visualization version GIF version |
Description: Prove that 2 + 2 ≠ 5. In George Orwell's "1984", Part One, Chapter Seven, the protagonist Winston notes that, "In the end the Party would announce that two and two made five, and you would have to believe it." http://www.sparknotes.com/lit/1984/section4.rhtml. More generally, the phrase 2 + 2 = 5 has come to represent an obviously false dogma one may be required to believe. See the Wikipedia article for more about this: https://en.wikipedia.org/wiki/2_%2B_2_%3D_5. Unsurprisingly, we can easily prove that this claim is false. (Contributed by David A. Wheeler, 31-Jan-2017.) |
Ref | Expression |
---|---|
2p2ne5 | ⊢ (2 + 2) ≠ 5 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2p2e4 12393 | . 2 ⊢ (2 + 2) = 4 | |
2 | 4re 12342 | . . 3 ⊢ 4 ∈ ℝ | |
3 | 4lt5 12435 | . . 3 ⊢ 4 < 5 | |
4 | 2, 3 | ltneii 11366 | . 2 ⊢ 4 ≠ 5 |
5 | 1, 4 | eqnetri 3007 | 1 ⊢ (2 + 2) ≠ 5 |
Colors of variables: wff setvar class |
Syntax hints: ≠ wne 2936 (class class class)co 7426 + caddc 11150 2c2 12313 4c4 12315 5c5 12316 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1963 ax-7 2003 ax-8 2106 ax-9 2114 ax-10 2137 ax-11 2153 ax-12 2173 ax-ext 2704 ax-sep 5301 ax-nul 5308 ax-pow 5367 ax-pr 5431 ax-un 7748 ax-resscn 11204 ax-1cn 11205 ax-icn 11206 ax-addcl 11207 ax-addrcl 11208 ax-mulcl 11209 ax-mulrcl 11210 ax-mulcom 11211 ax-addass 11212 ax-mulass 11213 ax-distr 11214 ax-i2m1 11215 ax-1ne0 11216 ax-1rid 11217 ax-rnegex 11218 ax-rrecex 11219 ax-cnre 11220 ax-pre-lttri 11221 ax-pre-lttrn 11222 ax-pre-ltadd 11223 ax-pre-mulgt0 11224 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1538 df-fal 1548 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2536 df-eu 2565 df-clab 2711 df-cleq 2725 df-clel 2812 df-nfc 2888 df-ne 2937 df-nel 3043 df-ral 3058 df-rex 3067 df-reu 3377 df-rab 3433 df-v 3479 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4916 df-br 5151 df-opab 5213 df-mpt 5234 df-id 5577 df-po 5591 df-so 5592 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-iota 6511 df-fun 6561 df-fn 6562 df-f 6563 df-f1 6564 df-fo 6565 df-f1o 6566 df-fv 6567 df-riota 7382 df-ov 7429 df-oprab 7430 df-mpo 7431 df-er 8739 df-en 8980 df-dom 8981 df-sdom 8982 df-pnf 11289 df-mnf 11290 df-xr 11291 df-ltxr 11292 df-le 11293 df-sub 11486 df-neg 11487 df-2 12321 df-3 12322 df-4 12323 df-5 12324 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |