Theorem 2p2e4 12470

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 8542 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 12398	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7429	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12400	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12399	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7428	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12411	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11251	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11312	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2788	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2787	1 ⊢ (2 + 2) = 4

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7418  1c1 11194   + caddc 11196  2c2 12390  3c3 12391  4c4 12392

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11251  ax-addcl 11253  ax-addass 11258

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-ov 7421  df-2 12398  df-3 12399  df-4 12400

This theorem is used by:  2t2e4  12499  i4  14341  4bc2eq6  14466  bpoly4  16218  fsumcube  16219  ef01bndlem  16345  6gcd4e2  16704  pythagtriplem1  16987  prmlem2  17291  43prm  17293  1259lem4  17305  2503lem1  17308  2503lem2  17309  2503lem3  17310  4001lem1  17312  4001lem4  17315  cphipval2  25555  quart1lem  27176  log2ub  27270  hgt750lem2  35274  3lexlogpow5ineq1  43084  3lexlogpow5ineq5  43090  4p4e8ALT  43289  2p4e6  43297  2p6e8  43299  3p4e7  43301  3cubeslem3l  43676  3cubeslem3r  43677  wallispi2lem1  47050  stirlinglem8  47060  sqwvfourb  47208  sin3t  47886  cos3t  47887  goldpolyfactor  47896  fmtnorec4  48603  m11nprm  48655  3exp4mod41  48670  gbowgt5  48829  gbpart7  48834  sbgoldbaltlem1  48846  sbgoldbalt  48848  sgoldbeven3prm  48850  mogoldbb  48852  nnsum3primes4  48855  pgnbgreunbgrlem2lem3  49183  2t6m3t4e0  49429  ackval1012  49771  2p2ne5  50905