MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2p2e4 Structured version   Visualization version   GIF version

Theorem 2p2e4 11766
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 8162 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
StepHypRef Expression
1 df-2 11694 . . 3 2 = (1 + 1)
21oveq2i 7161 . 2 (2 + 2) = (2 + (1 + 1))
3 df-4 11696 . . 3 4 = (3 + 1)
4 df-3 11695 . . . 4 3 = (2 + 1)
54oveq1i 7160 . . 3 (3 + 1) = ((2 + 1) + 1)
6 2cn 11706 . . . 4 2 ∈ ℂ
7 ax-1cn 10589 . . . 4 1 ∈ ℂ
86, 7, 7addassi 10645 . . 3 ((2 + 1) + 1) = (2 + (1 + 1))
93, 5, 83eqtri 2853 . 2 4 = (2 + (1 + 1))
102, 9eqtr4i 2852 1 (2 + 2) = 4
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  (class class class)co 7150  1c1 10532   + caddc 10534  2c2 11686  3c3 11687  4c4 11688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-1cn 10589  ax-addcl 10591  ax-addass 10596
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-iota 6313  df-fv 6362  df-ov 7153  df-2 11694  df-3 11695  df-4 11696
This theorem is referenced by:  2t2e4  11795  i4  13562  4bc2eq6  13684  bpoly4  15408  fsumcube  15409  ef01bndlem  15532  6gcd4e2  15881  pythagtriplem1  16148  prmlem2  16448  43prm  16450  1259lem4  16462  2503lem1  16465  2503lem2  16466  2503lem3  16467  4001lem1  16469  4001lem4  16472  cphipval2  23778  quart1lem  25365  log2ub  25460  hgt750lem2  31828  3cubeslem3l  39167  3cubeslem3r  39168  wallispi2lem1  42241  stirlinglem8  42251  sqwvfourb  42399  fmtnorec4  43562  m11nprm  43617  3exp4mod41  43632  gbowgt5  43778  gbpart7  43783  sbgoldbaltlem1  43795  sbgoldbalt  43797  sgoldbeven3prm  43799  mogoldbb  43801  nnsum3primes4  43804  2t6m3t4e0  44298  2p2ne5  44801
  Copyright terms: Public domain W3C validator