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 \in ℂ$
7		ax-1cn	$⊢ 1 \in ℂ$
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$