Theorem 2p2e4 12484

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 8557 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 12412	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7435	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12414	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12413	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7434	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12425	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11265	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11326	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2787	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2786	1 ⊢ (2 + 2) = 4

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7424  1c1 11208   + caddc 11210  2c2 12404  3c3 12405  4c4 12406

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11265  ax-addcl 11267  ax-addass 11272

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-2 12412  df-3 12413  df-4 12414

This theorem is used by:  2t2e4  12513  i4  14355  4bc2eq6  14480  bpoly4  16234  fsumcube  16235  ef01bndlem  16361  6gcd4e2  16720  pythagtriplem1  17003  prmlem2  17307  43prm  17309  1259lem4  17321  2503lem1  17324  2503lem2  17325  2503lem3  17326  4001lem1  17328  4001lem4  17331  cphipval2  25571  quart1lem  27192  log2ub  27286  hgt750lem2  35331  3lexlogpow5ineq1  43241  3lexlogpow5ineq5  43247  4p4e8ALT  43446  2p4e6  43454  2p6e8  43456  3p4e7  43458  3cubeslem3l  43833  3cubeslem3r  43834  wallispi2lem1  47217  stirlinglem8  47227  sqwvfourb  47375  sin3t  48053  cos3t  48054  goldpolyfactor  48063  fmtnorec4  48770  m11nprm  48822  3exp4mod41  48837  gbowgt5  48996  gbpart7  49001  sbgoldbaltlem1  49013  sbgoldbalt  49015  sgoldbeven3prm  49017  mogoldbb  49019  nnsum3primes4  49022  pgnbgreunbgrlem2lem3  49350  2t6m3t4e0  49596  ackval1012  49938  2p2ne5  51147