Theorem 2p2e4 12374

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 8525 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 12302	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7422	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12304	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12303	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7421	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12315	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11157	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11218	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2796	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2795	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1567  (class class class)co 7411  1c1 11100   + caddc 11102  2c2 12294  3c3 12295  4c4 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11157  ax-addcl 11159  ax-addass 11164

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12302  df-3 12303  df-4 12304

This theorem is referenced by:  2t2e4  12403  i4  14239  4bc2eq6  14364  bpoly4  16112  fsumcube  16113  ef01bndlem  16239  6gcd4e2  16595  pythagtriplem1  16875  prmlem2  17179  43prm  17181  1259lem4  17193  2503lem1  17196  2503lem2  17197  2503lem3  17198  4001lem1  17200  4001lem4  17203  cphipval2  25368  quart1lem  26985  log2ub  27079  hgt750lem2  34983  3lexlogpow5ineq1  42710  3lexlogpow5ineq5  42716  3cubeslem3l  43308  3cubeslem3r  43309  wallispi2lem1  46676  stirlinglem8  46686  sqwvfourb  46834  sin3t  47496  cos3t  47497  fmtnorec4  48189  m11nprm  48241  3exp4mod41  48256  gbowgt5  48415  gbpart7  48420  sbgoldbaltlem1  48432  sbgoldbalt  48434  sgoldbeven3prm  48436  mogoldbb  48438  nnsum3primes4  48441  pgnbgreunbgrlem2lem3  48769  2t6m3t4e0  49012  ackval1012  49354  2p2ne5  50471