Theorem 2p2e4 11773

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 8166 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 11701	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7167	. 2 ⊢ (2 + 2) = (2 + (1 + 1))
3		df-4 11703	. . 3 ⊢ 4 = (3 + 1)
4		df-3 11702	. . . 4 ⊢ 3 = (2 + 1)
5	4	oveq1i 7166	. . 3 ⊢ (3 + 1) = ((2 + 1) + 1)
6		2cn 11713	. . . 4 ⊢ 2 ∈ ℂ
7		ax-1cn 10595	. . . 4 ⊢ 1 ∈ ℂ
8	6, 7, 7	addassi 10651	. . 3 ⊢ ((2 + 1) + 1) = (2 + (1 + 1))
9	3, 5, 8	3eqtri 2848	. 2 ⊢ 4 = (2 + (1 + 1))
10	2, 9	eqtr4i 2847	1 ⊢ (2 + 2) = 4

Syntax hints:   = wceq 1537  (class class class)co 7156  1c1 10538   + caddc 10540  2c2 11693  3c3 11694  4c4 11695

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-1cn 10595  ax-addcl 10597  ax-addass 10602

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-2 11701  df-3 11702  df-4 11703

This theorem is referenced by:  2t2e4  11802  i4  13568  4bc2eq6  13690  bpoly4  15413  fsumcube  15414  ef01bndlem  15537  6gcd4e2  15886  pythagtriplem1  16153  prmlem2  16453  43prm  16455  1259lem4  16467  2503lem1  16470  2503lem2  16471  2503lem3  16472  4001lem1  16474  4001lem4  16477  cphipval2  23844  quart1lem  25433  log2ub  25527  hgt750lem2  31923  3cubeslem3l  39332  3cubeslem3r  39333  wallispi2lem1  42405  stirlinglem8  42415  sqwvfourb  42563  fmtnorec4  43760  m11nprm  43815  3exp4mod41  43830  gbowgt5  43976  gbpart7  43981  sbgoldbaltlem1  43993  sbgoldbalt  43995  sgoldbeven3prm  43997  mogoldbb  43999  nnsum3primes4  44002  2t6m3t4e0  44445  2p2ne5  44948