Theorem 2p2e4 12289

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 8480 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 12222	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7381	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12224	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12223	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7380	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12234	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11098	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11156	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2764	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2763	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1542  (class class class)co 7370  1c1 11041   + caddc 11043  2c2 12214  3c3 12215  4c4 12216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11098  ax-addcl 11100  ax-addass 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6458  df-fv 6510  df-ov 7373  df-2 12222  df-3 12223  df-4 12224

This theorem is referenced by:  2t2e4  12318  i4  14141  4bc2eq6  14266  bpoly4  15996  fsumcube  15997  ef01bndlem  16123  6gcd4e2  16479  pythagtriplem1  16758  prmlem2  17061  43prm  17063  1259lem4  17075  2503lem1  17078  2503lem2  17079  2503lem3  17080  4001lem1  17082  4001lem4  17085  cphipval2  25214  quart1lem  26838  log2ub  26932  hgt750lem2  34836  3lexlogpow5ineq1  42453  3lexlogpow5ineq5  42459  3cubeslem3l  43072  3cubeslem3r  43073  wallispi2lem1  46458  stirlinglem8  46468  sqwvfourb  46616  fmtnorec4  47938  m11nprm  47990  3exp4mod41  48005  gbowgt5  48151  gbpart7  48156  sbgoldbaltlem1  48168  sbgoldbalt  48170  sgoldbeven3prm  48172  mogoldbb  48174  nnsum3primes4  48177  pgnbgreunbgrlem2lem3  48505  2t6m3t4e0  48737  ackval1012  49079  2p2ne5  50186