Theorem 2p2e4 12383

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 8566 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 12311	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7435	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12313	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12312	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7434	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12323	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11202	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11260	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2759	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2758	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1533  (class class class)co 7424  1c1 11145   + caddc 11147  2c2 12303  3c3 12304  4c4 12305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698  ax-1cn 11202  ax-addcl 11204  ax-addass 11209

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3429  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-br 5151  df-iota 6503  df-fv 6559  df-ov 7427  df-2 12311  df-3 12312  df-4 12313

This theorem is referenced by:  2t2e4  12412  i4  14205  4bc2eq6  14326  bpoly4  16041  fsumcube  16042  ef01bndlem  16166  6gcd4e2  16519  pythagtriplem1  16790  prmlem2  17094  43prm  17096  1259lem4  17108  2503lem1  17111  2503lem2  17112  2503lem3  17113  4001lem1  17115  4001lem4  17118  cphipval2  25187  quart1lem  26805  log2ub  26899  hgt750lem2  34289  3lexlogpow5ineq1  41529  3lexlogpow5ineq5  41535  3cubeslem3l  42109  3cubeslem3r  42110  wallispi2lem1  45461  stirlinglem8  45471  sqwvfourb  45619  fmtnorec4  46891  m11nprm  46943  3exp4mod41  46958  gbowgt5  47104  gbpart7  47109  sbgoldbaltlem1  47121  sbgoldbalt  47123  sgoldbeven3prm  47125  mogoldbb  47127  nnsum3primes4  47130  2t6m3t4e0  47463  ackval1012  47814  2p2ne5  48282