This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2p2e4

Description: Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: mmset.html#trivia . This proof is simple, but it depends on many other proof steps because 2 and 4 are complex numbers and thus it depends on our construction of complex numbers. The proof o2p2e4 is similar but proves 2 + 2 = 4 using ordinal natural numbers (finite integers starting at 0), so that proof depends on fewer intermediate steps. (Contributed by NM, 27-May-1999)

		Ref	Expression
	Assertion	2p2e4	⊢ ( 2 + 2 ) = 4

Proof

Step	Hyp	Ref	Expression
1		df-2	⊢ 2 = ( 1 + 1 )
2	1	oveq2i	⊢ ( 2 + 2 ) = ( 2 + ( 1 + 1 ) )
3		df-4	⊢ 4 = ( 3 + 1 )
4		df-3	⊢ 3 = ( 2 + 1 )
5	4	oveq1i	⊢ ( 3 + 1 ) = ( ( 2 + 1 ) + 1 )
6		2cn	⊢ 2 ∈ ℂ
7		ax-1cn	⊢ 1 ∈ ℂ
8	6 7 7	addassi	⊢ ( ( 2 + 1 ) + 1 ) = ( 2 + ( 1 + 1 ) )
9	3 5 8	3eqtri	⊢ 4 = ( 2 + ( 1 + 1 ) )
10	2 9	eqtr4i	⊢ ( 2 + 2 ) = 4