Theorem 2p2e4 12393

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 8573 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 12321	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7437	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12323	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12322	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7436	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12333	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11205	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11263	. . 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 1535  (class class class)co 7426  1c1 11148   + caddc 11150  2c2 12313  3c3 12314  4c4 12315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1963  ax-7 2003  ax-8 2106  ax-9 2114  ax-ext 2704  ax-1cn 11205  ax-addcl 11207  ax-addass 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1087  df-tru 1538  df-fal 1548  df-ex 1775  df-sb 2061  df-clab 2711  df-cleq 2725  df-clel 2812  df-rab 3433  df-v 3479  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4916  df-br 5151  df-iota 6511  df-fv 6567  df-ov 7429  df-2 12321  df-3 12322  df-4 12323

This theorem is referenced by:  2t2e4  12422  i4  14230  4bc2eq6  14355  bpoly4  16082  fsumcube  16083  ef01bndlem  16207  6gcd4e2  16562  pythagtriplem1  16840  prmlem2  17144  43prm  17146  1259lem4  17158  2503lem1  17161  2503lem2  17162  2503lem3  17163  4001lem1  17165  4001lem4  17168  cphipval2  25271  quart1lem  26895  log2ub  26989  hgt750lem2  34607  3lexlogpow5ineq1  41997  3lexlogpow5ineq5  42003  3cubeslem3l  42635  3cubeslem3r  42636  wallispi2lem1  45984  stirlinglem8  45994  sqwvfourb  46142  fmtnorec4  47431  m11nprm  47483  3exp4mod41  47498  gbowgt5  47644  gbpart7  47649  sbgoldbaltlem1  47661  sbgoldbalt  47663  sgoldbeven3prm  47665  mogoldbb  47667  nnsum3primes4  47670  2t6m3t4e0  48118  ackval1012  48468  2p2ne5  48951