Theorem 2p2e4 12322

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 8507 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 12250	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7400	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12252	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12251	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7399	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12262	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11132	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11190	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2757	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2756	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1540  (class class class)co 7389  1c1 11075   + caddc 11077  2c2 12242  3c3 12243  4c4 12244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11132  ax-addcl 11134  ax-addass 11139

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-iota 6466  df-fv 6521  df-ov 7392  df-2 12250  df-3 12251  df-4 12252

This theorem is referenced by:  2t2e4  12351  i4  14175  4bc2eq6  14300  bpoly4  16031  fsumcube  16032  ef01bndlem  16158  6gcd4e2  16514  pythagtriplem1  16793  prmlem2  17096  43prm  17098  1259lem4  17110  2503lem1  17113  2503lem2  17114  2503lem3  17115  4001lem1  17117  4001lem4  17120  cphipval2  25147  quart1lem  26771  log2ub  26865  hgt750lem2  34649  3lexlogpow5ineq1  42037  3lexlogpow5ineq5  42043  3cubeslem3l  42667  3cubeslem3r  42668  wallispi2lem1  46062  stirlinglem8  46072  sqwvfourb  46220  fmtnorec4  47540  m11nprm  47592  3exp4mod41  47607  gbowgt5  47753  gbpart7  47758  sbgoldbaltlem1  47770  sbgoldbalt  47772  sgoldbeven3prm  47774  mogoldbb  47776  nnsum3primes4  47779  pgnbgreunbgrlem2lem3  48096  2t6m3t4e0  48326  ackval1012  48669  2p2ne5  49777