Theorem 2p2e4 12305

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 8470 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 12238	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7372	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12240	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12239	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7371	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12250	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11090	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11149	. . 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 7361  1c1 11033   + caddc 11035  2c2 12230  3c3 12231  4c4 12232

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 11090  ax-addcl 11092  ax-addass 11097

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238  df-3 12239  df-4 12240

This theorem is referenced by:  2t2e4  12334  i4  14160  4bc2eq6  14285  bpoly4  16018  fsumcube  16019  ef01bndlem  16145  6gcd4e2  16501  pythagtriplem1  16781  prmlem2  17084  43prm  17086  1259lem4  17098  2503lem1  17101  2503lem2  17102  2503lem3  17103  4001lem1  17105  4001lem4  17108  cphipval2  25221  quart1lem  26835  log2ub  26929  hgt750lem2  34815  3lexlogpow5ineq1  42510  3lexlogpow5ineq5  42516  3cubeslem3l  43135  3cubeslem3r  43136  wallispi2lem1  46520  stirlinglem8  46530  sqwvfourb  46678  sin3t  47338  cos3t  47339  fmtnorec4  48027  m11nprm  48079  3exp4mod41  48094  gbowgt5  48253  gbpart7  48258  sbgoldbaltlem1  48270  sbgoldbalt  48272  sgoldbeven3prm  48274  mogoldbb  48276  nnsum3primes4  48279  pgnbgreunbgrlem2lem3  48607  2t6m3t4e0  48839  ackval1012  49181  2p2ne5  50288