Theorem 2p2e4 12373

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 8551 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 12301	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7414	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12303	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12302	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7413	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12313	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11185	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11243	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2762	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2761	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1540  (class class class)co 7403  1c1 11128   + caddc 11130  2c2 12293  3c3 12294  4c4 12295

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-addcl 11187  ax-addass 11192

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-2 12301  df-3 12302  df-4 12303

This theorem is referenced by:  2t2e4  12402  i4  14220  4bc2eq6  14345  bpoly4  16073  fsumcube  16074  ef01bndlem  16200  6gcd4e2  16555  pythagtriplem1  16834  prmlem2  17137  43prm  17139  1259lem4  17151  2503lem1  17154  2503lem2  17155  2503lem3  17156  4001lem1  17158  4001lem4  17161  cphipval2  25191  quart1lem  26815  log2ub  26909  hgt750lem2  34630  3lexlogpow5ineq1  42013  3lexlogpow5ineq5  42019  3cubeslem3l  42656  3cubeslem3r  42657  wallispi2lem1  46048  stirlinglem8  46058  sqwvfourb  46206  fmtnorec4  47511  m11nprm  47563  3exp4mod41  47578  gbowgt5  47724  gbpart7  47729  sbgoldbaltlem1  47741  sbgoldbalt  47743  sgoldbeven3prm  47745  mogoldbb  47747  nnsum3primes4  47750  2t6m3t4e0  48271  ackval1012  48618  2p2ne5  49610