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

Theorem 2p2e4 10991
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 7485 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 10926 . . 3 2 = (1 + 1)
21oveq2i 6538 . 2 (2 + 2) = (2 + (1 + 1))
3 df-4 10928 . . 3 4 = (3 + 1)
4 df-3 10927 . . . 4 3 = (2 + 1)
54oveq1i 6537 . . 3 (3 + 1) = ((2 + 1) + 1)
6 2cn 10938 . . . 4 2 ∈ ℂ
7 ax-1cn 9850 . . . 4 1 ∈ ℂ
86, 7, 7addassi 9904 . . 3 ((2 + 1) + 1) = (2 + (1 + 1))
93, 5, 83eqtri 2635 . 2 4 = (2 + (1 + 1))
102, 9eqtr4i 2634 1 (2 + 2) = 4
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  (class class class)co 6527  1c1 9793   + caddc 9795  2c2 10917  3c3 10918  4c4 10919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-addass 9857  ax-i2m1 9860  ax-1ne0 9861  ax-rrecex 9864  ax-cnre 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-2 10926  df-3 10927  df-4 10928
This theorem is referenced by:  2t2e4  11024  i4  12784  4bc2eq6  12933  bpoly4  14575  fsumcube  14576  ef01bndlem  14699  6gcd4e2  15039  pythagtriplem1  15305  prmlem2  15611  43prm  15613  1259lem4  15625  2503lem1  15628  2503lem2  15629  2503lem3  15630  4001lem1  15632  4001lem4  15635  quart1lem  24299  log2ub  24393  wallispi2lem1  38761  stirlinglem8  38771  sqwvfourb  38919  fmtnorec4  39797  m11nprm  39854  3exp4mod41  39869  gbogt5  39982  gbpart7  39987  sgoldbaltlem1  39999  sgoldbalt  40001  nnsum3primes4  40002  2t6m3t4e0  41914  2p2ne5  42309
  Copyright terms: Public domain W3C validator