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$$