Theorem 2p2e4 12311

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 8476 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.)

Assertion

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

Proof of Theorem 2p2e4

Step	Hyp	Ref	Expression
1		df-2 12244	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7378	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12246	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12245	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7377	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12256	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11096	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11155	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2763	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2762	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1542  (class class class)co 7367  1c1 11039   + caddc 11041  2c2 12236  3c3 12237  4c4 12238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-addcl 11098  ax-addass 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244  df-3 12245  df-4 12246

This theorem is referenced by:  2t2e4  12340  i4  14166  4bc2eq6  14291  bpoly4  16024  fsumcube  16025  ef01bndlem  16151  6gcd4e2  16507  pythagtriplem1  16787  prmlem2  17090  43prm  17092  1259lem4  17104  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem1  17111  4001lem4  17114  cphipval2  25208  quart1lem  26819  log2ub  26913  hgt750lem2  34796  3lexlogpow5ineq1  42493  3lexlogpow5ineq5  42499  3cubeslem3l  43118  3cubeslem3r  43119  wallispi2lem1  46499  stirlinglem8  46509  sqwvfourb  46657  sin3t  47319  cos3t  47320  fmtnorec4  48012  m11nprm  48064  3exp4mod41  48079  gbowgt5  48238  gbpart7  48243  sbgoldbaltlem1  48255  sbgoldbalt  48257  sgoldbeven3prm  48259  mogoldbb  48261  nnsum3primes4  48264  pgnbgreunbgrlem2lem3  48592  2t6m3t4e0  48824  ackval1012  49166  2p2ne5  50273