Theorem 2p2e4 12287

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 8478 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 12220	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7379	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12222	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12221	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7378	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12232	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11096	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11154	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2764	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2763	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1542  (class class class)co 7368  1c1 11039   + caddc 11041  2c2 12212  3c3 12213  4c4 12214

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 2709  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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-2 12220  df-3 12221  df-4 12222

This theorem is referenced by:  2t2e4  12316  i4  14139  4bc2eq6  14264  bpoly4  15994  fsumcube  15995  ef01bndlem  16121  6gcd4e2  16477  pythagtriplem1  16756  prmlem2  17059  43prm  17061  1259lem4  17073  2503lem1  17076  2503lem2  17077  2503lem3  17078  4001lem1  17080  4001lem4  17083  cphipval2  25209  quart1lem  26833  log2ub  26927  hgt750lem2  34830  3lexlogpow5ineq1  42424  3lexlogpow5ineq5  42430  3cubeslem3l  43043  3cubeslem3r  43044  wallispi2lem1  46429  stirlinglem8  46439  sqwvfourb  46587  fmtnorec4  47909  m11nprm  47961  3exp4mod41  47976  gbowgt5  48122  gbpart7  48127  sbgoldbaltlem1  48139  sbgoldbalt  48141  sgoldbeven3prm  48143  mogoldbb  48145  nnsum3primes4  48148  pgnbgreunbgrlem2lem3  48476  2t6m3t4e0  48708  ackval1012  49050  2p2ne5  50157