Theorem 2p2e4 12354

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 8547 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 12282	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7423	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12284	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12283	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7422	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12294	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11174	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11231	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2763	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2762	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1540  (class class class)co 7412  1c1 11117   + caddc 11119  2c2 12274  3c3 12275  4c4 12276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-1cn 11174  ax-addcl 11176  ax-addass 11181

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7415  df-2 12282  df-3 12283  df-4 12284

This theorem is referenced by:  2t2e4  12383  i4  14175  4bc2eq6  14296  bpoly4  16010  fsumcube  16011  ef01bndlem  16134  6gcd4e2  16487  pythagtriplem1  16756  prmlem2  17060  43prm  17062  1259lem4  17074  2503lem1  17077  2503lem2  17078  2503lem3  17079  4001lem1  17081  4001lem4  17084  cphipval2  25089  quart1lem  26701  log2ub  26795  hgt750lem2  34128  3lexlogpow5ineq1  41386  3lexlogpow5ineq5  41392  3cubeslem3l  41887  3cubeslem3r  41888  wallispi2lem1  45246  stirlinglem8  45256  sqwvfourb  45404  fmtnorec4  46676  m11nprm  46728  3exp4mod41  46743  gbowgt5  46889  gbpart7  46894  sbgoldbaltlem1  46906  sbgoldbalt  46908  sgoldbeven3prm  46910  mogoldbb  46912  nnsum3primes4  46915  2t6m3t4e0  47187  ackval1012  47538  2p2ne5  48007