Theorem 2p2e4 12292

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 8482 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 12225	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7380	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 12227	. . 3 ⊢ 4 = (3 + 1)
4		df-3 12226	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7379	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 12237	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 11102	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 11160	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2756	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2755	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1540  (class class class)co 7369  1c1 11045   + caddc 11047  2c2 12217  3c3 12218  4c4 12219

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 2701  ax-1cn 11102  ax-addcl 11104  ax-addass 11109

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 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-2 12225  df-3 12226  df-4 12227

This theorem is referenced by:  2t2e4  12321  i4  14145  4bc2eq6  14270  bpoly4  16001  fsumcube  16002  ef01bndlem  16128  6gcd4e2  16484  pythagtriplem1  16763  prmlem2  17066  43prm  17068  1259lem4  17080  2503lem1  17083  2503lem2  17084  2503lem3  17085  4001lem1  17087  4001lem4  17090  cphipval2  25117  quart1lem  26741  log2ub  26835  hgt750lem2  34616  3lexlogpow5ineq1  42015  3lexlogpow5ineq5  42021  3cubeslem3l  42647  3cubeslem3r  42648  wallispi2lem1  46042  stirlinglem8  46052  sqwvfourb  46200  fmtnorec4  47523  m11nprm  47575  3exp4mod41  47590  gbowgt5  47736  gbpart7  47741  sbgoldbaltlem1  47753  sbgoldbalt  47755  sgoldbeven3prm  47757  mogoldbb  47759  nnsum3primes4  47762  pgnbgreunbgrlem2lem3  48079  2t6m3t4e0  48309  ackval1012  48652  2p2ne5  49760