MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  5t2e10 Structured version   Unicode version

Theorem 5t2e10 10679
Description: 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.)
Assertion
Ref Expression
5t2e10  |-  ( 5  x.  2 )  =  10

Proof of Theorem 5t2e10
StepHypRef Expression
1 5cn 10604 . . 3  |-  5  e.  CC
21times2i 10646 . 2  |-  ( 5  x.  2 )  =  ( 5  +  5 )
3 5p5e10 10665 . 2  |-  ( 5  +  5 )  =  10
42, 3eqtri 2489 1  |-  ( 5  x.  2 )  =  10
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374  (class class class)co 6275    + caddc 9484    x. cmul 9486   2c2 10574   5c5 10577   10c10 10582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rrecex 9553  ax-cnre 9554
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-ov 6278  df-2 10583  df-3 10584  df-4 10585  df-5 10586  df-6 10587  df-7 10588  df-8 10589  df-9 10590  df-10 10591
This theorem is referenced by:  5t3e15  11039  dec2dvds  14397  dec5dvds  14398  dec5nprm  14400  dec2nprm  14401  2exp16  14422  10nprm  14446  1259lem1  14460  1259lem4  14463  2503lem1  14466  2503lem2  14467  2503lem3  14468  4001lem1  14470  4001lem4  14473  4001prm  14474  log2ublem3  23000  log2ub  23001  bclbnd  23276  bpos1  23279  bposlem4  23283  bposlem5  23284  bposlem8  23287
  Copyright terms: Public domain W3C validator