Theorem 2p2e4 12367

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 8547 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 12295	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7410	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12297	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12296	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7409	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12307	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11179	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11237	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2761	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2760	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1539  (class class class)co 7399  1c1 11122   + caddc 11124  2c2 12287  3c3 12288  4c4 12289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-1cn 11179  ax-addcl 11181  ax-addass 11186

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-iota 6480  df-fv 6535  df-ov 7402  df-2 12295  df-3 12296  df-4 12297

This theorem is referenced by:  2t2e4  12396  i4  14210  4bc2eq6  14335  bpoly4  16062  fsumcube  16063  ef01bndlem  16187  6gcd4e2  16542  pythagtriplem1  16821  prmlem2  17124  43prm  17126  1259lem4  17138  2503lem1  17141  2503lem2  17142  2503lem3  17143  4001lem1  17145  4001lem4  17148  cphipval2  25178  quart1lem  26801  log2ub  26895  hgt750lem2  34605  3lexlogpow5ineq1  41989  3lexlogpow5ineq5  41995  3cubeslem3l  42634  3cubeslem3r  42635  wallispi2lem1  46030  stirlinglem8  46040  sqwvfourb  46188  fmtnorec4  47481  m11nprm  47533  3exp4mod41  47548  gbowgt5  47694  gbpart7  47699  sbgoldbaltlem1  47711  sbgoldbalt  47713  sgoldbeven3prm  47715  mogoldbb  47717  nnsum3primes4  47720  2t6m3t4e0  48209  ackval1012  48556  2p2ne5  49382