Metamath Proof Explorer


Theorem 2p2ne5

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
Assertion 2p2ne5 ( 2 + 2 ) ≠ 5

Proof

Step Hyp Ref Expression
1 2p2e4 ( 2 + 2 ) = 4
2 4re 4 ∈ ℝ
3 4lt5 4 < 5
4 2 3 ltneii 4 ≠ 5
5 1 4 eqnetri ( 2 + 2 ) ≠ 5