Theorem 2p2e4 12397

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 8575 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 12325	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7440	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12327	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12326	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7439	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12337	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11209	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11267	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2768	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2767	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1540  (class class class)co 7429  1c1 11152   + caddc 11154  2c2 12317  3c3 12318  4c4 12319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11209  ax-addcl 11211  ax-addass 11216

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-br 5142  df-iota 6512  df-fv 6567  df-ov 7432  df-2 12325  df-3 12326  df-4 12327

This theorem is referenced by:  2t2e4  12426  i4  14239  4bc2eq6  14364  bpoly4  16091  fsumcube  16092  ef01bndlem  16216  6gcd4e2  16571  pythagtriplem1  16850  prmlem2  17153  43prm  17155  1259lem4  17167  2503lem1  17170  2503lem2  17171  2503lem3  17172  4001lem1  17174  4001lem4  17177  cphipval2  25265  quart1lem  26888  log2ub  26982  hgt750lem2  34645  3lexlogpow5ineq1  42033  3lexlogpow5ineq5  42039  3cubeslem3l  42675  3cubeslem3r  42676  wallispi2lem1  46059  stirlinglem8  46069  sqwvfourb  46217  fmtnorec4  47509  m11nprm  47561  3exp4mod41  47576  gbowgt5  47722  gbpart7  47727  sbgoldbaltlem1  47739  sbgoldbalt  47741  sgoldbeven3prm  47743  mogoldbb  47745  nnsum3primes4  47748  2t6m3t4e0  48237  ackval1012  48584  2p2ne5  49290