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