Theorem 2p2e4 12013

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 8310 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 11941	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7263	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 11943	. . 3 ⊢ 4 = (3 + 1)
4		df-3 11942	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7262	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 11953	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 10835	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 10891	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2771	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2770	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1543  (class class class)co 7252  1c1 10778   + caddc 10780  2c2 11933  3c3 11934  4c4 11935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710  ax-1cn 10835  ax-addcl 10837  ax-addass 10842

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-rab 3073  df-v 3425  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4255  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6373  df-fv 6423  df-ov 7255  df-2 11941  df-3 11942  df-4 11943

This theorem is referenced by:  2t2e4  12042  i4  13824  4bc2eq6  13946  bpoly4  15672  fsumcube  15673  ef01bndlem  15796  6gcd4e2  16149  pythagtriplem1  16420  prmlem2  16724  43prm  16726  1259lem4  16738  2503lem1  16741  2503lem2  16742  2503lem3  16743  4001lem1  16745  4001lem4  16748  cphipval2  24285  quart1lem  25885  log2ub  25979  hgt750lem2  32507  3lexlogpow5ineq1  39969  3lexlogpow5ineq5  39975  3cubeslem3l  40396  3cubeslem3r  40397  wallispi2lem1  43475  stirlinglem8  43485  sqwvfourb  43633  fmtnorec4  44862  m11nprm  44914  3exp4mod41  44929  gbowgt5  45075  gbpart7  45080  sbgoldbaltlem1  45092  sbgoldbalt  45094  sgoldbeven3prm  45096  mogoldbb  45098  nnsum3primes4  45101  2t6m3t4e0  45545  ackval1012  45897  2p2ne5  46361