Theorem 2p2e4 12316

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 8505 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 12249	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7398	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12251	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12250	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7397	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12261	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11126	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11184	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2756	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2755	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1540  (class class class)co 7387  1c1 11069   + caddc 11071  2c2 12241  3c3 12242  4c4 12243

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-addcl 11128  ax-addass 11133

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249  df-3 12250  df-4 12251

This theorem is referenced by:  2t2e4  12345  i4  14169  4bc2eq6  14294  bpoly4  16025  fsumcube  16026  ef01bndlem  16152  6gcd4e2  16508  pythagtriplem1  16787  prmlem2  17090  43prm  17092  1259lem4  17104  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem1  17111  4001lem4  17114  cphipval2  25141  quart1lem  26765  log2ub  26859  hgt750lem2  34643  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  3cubeslem3l  42674  3cubeslem3r  42675  wallispi2lem1  46069  stirlinglem8  46079  sqwvfourb  46227  fmtnorec4  47550  m11nprm  47602  3exp4mod41  47617  gbowgt5  47763  gbpart7  47768  sbgoldbaltlem1  47780  sbgoldbalt  47782  sgoldbeven3prm  47784  mogoldbb  47786  nnsum3primes4  47789  pgnbgreunbgrlem2lem3  48106  2t6m3t4e0  48336  ackval1012  48679  2p2ne5  49787