Theorem 2p2e4 12343

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 8536 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 12271	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7415	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12273	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12272	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7414	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12283	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11164	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11220	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2765	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2764	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1542  (class class class)co 7404  1c1 11107   + caddc 11109  2c2 12263  3c3 12264  4c4 12265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11164  ax-addcl 11166  ax-addass 11171

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7407  df-2 12271  df-3 12272  df-4 12273

This theorem is referenced by:  2t2e4  12372  i4  14164  4bc2eq6  14285  bpoly4  15999  fsumcube  16000  ef01bndlem  16123  6gcd4e2  16476  pythagtriplem1  16745  prmlem2  17049  43prm  17051  1259lem4  17063  2503lem1  17066  2503lem2  17067  2503lem3  17068  4001lem1  17070  4001lem4  17073  cphipval2  24740  quart1lem  26340  log2ub  26434  hgt750lem2  33602  3lexlogpow5ineq1  40857  3lexlogpow5ineq5  40863  3cubeslem3l  41357  3cubeslem3r  41358  wallispi2lem1  44722  stirlinglem8  44732  sqwvfourb  44880  fmtnorec4  46152  m11nprm  46204  3exp4mod41  46219  gbowgt5  46365  gbpart7  46370  sbgoldbaltlem1  46382  sbgoldbalt  46384  sgoldbeven3prm  46386  mogoldbb  46388  nnsum3primes4  46391  2t6m3t4e0  46926  ackval1012  47278  2p2ne5  47747