Theorem 2p2e4 12352

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 8510 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 12280	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7407	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12282	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12281	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7406	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12293	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11131	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11192	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2789	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2788	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1560  (class class class)co 7396  1c1 11074   + caddc 11076  2c2 12272  3c3 12273  4c4 12274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-addcl 11133  ax-addass 11138

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-2 12280  df-3 12281  df-4 12282

This theorem is referenced by:  2t2e4  12381  i4  14217  4bc2eq6  14342  bpoly4  16089  fsumcube  16090  ef01bndlem  16216  6gcd4e2  16572  pythagtriplem1  16852  prmlem2  17156  43prm  17158  1259lem4  17170  2503lem1  17173  2503lem2  17174  2503lem3  17175  4001lem1  17177  4001lem4  17180  cphipval2  25300  quart1lem  26917  log2ub  27011  hgt750lem2  34943  3lexlogpow5ineq1  42668  3lexlogpow5ineq5  42674  3cubeslem3l  43264  3cubeslem3r  43265  wallispi2lem1  46642  stirlinglem8  46652  sqwvfourb  46800  sin3t  47462  cos3t  47463  fmtnorec4  48155  m11nprm  48207  3exp4mod41  48222  gbowgt5  48381  gbpart7  48386  sbgoldbaltlem1  48398  sbgoldbalt  48400  sgoldbeven3prm  48402  mogoldbb  48404  nnsum3primes4  48407  pgnbgreunbgrlem2lem3  48735  2t6m3t4e0  48967  ackval1012  49309  2p2ne5  50416