Theorem 2p2e4 12517

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 8587 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 12445	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7462	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12447	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12446	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7461	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12458	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11297	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11358	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2790	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2789	1 ⊢ (2 + 2) = 4

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7451  1c1 11240   + caddc 11242  2c2 12437  3c3 12438  4c4 12439

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-addcl 11299  ax-addass 11304

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-2 12445  df-3 12446  df-4 12447

This theorem is used by:  2t2e4  12546  i4  14388  4bc2eq6  14514  bpoly4  16269  fsumcube  16270  ef01bndlem  16396  6gcd4e2  16755  pythagtriplem1  17038  prmlem2  17342  43prm  17344  1259lem4  17356  2503lem1  17359  2503lem2  17360  2503lem3  17361  4001lem1  17363  4001lem4  17366  cphipval2  25617  quart1lem  27240  log2ub  27334  hgt750lem2  35392  3lexlogpow5ineq1  43370  3lexlogpow5ineq5  43376  4p4e8ALT  43575  2p4e6  43583  2p6e8  43585  3p4e7  43587  3cubeslem3l  43962  3cubeslem3r  43963  wallispi2lem1  47354  stirlinglem8  47364  sqwvfourb  47512  sin3t  48190  cos3t  48191  goldpolyfactor  48200  fmtnorec4  48907  m11nprm  48959  3exp4mod41  48974  gbowgt5  49133  gbpart7  49138  sbgoldbaltlem1  49150  sbgoldbalt  49152  sgoldbeven3prm  49154  mogoldbb  49156  nnsum3primes4  49159  pgnbgreunbgrlem2lem3  49487  2t6m3t4e0  49791  ackval1012  50133  2p2ne5  51364