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

Theorem 5t2e10 10731
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 10656 . . 3  |-  5  e.  CC
21times2i 10698 . 2  |-  ( 5  x.  2 )  =  ( 5  +  5 )
3 5p5e10 10717 . 2  |-  ( 5  +  5 )  =  10
42, 3eqtri 2431 1  |-  ( 5  x.  2 )  =  10
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405  (class class class)co 6278    + caddc 9525    x. cmul 9527   2c2 10626   5c5 10629   10c10 10634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-mulcom 9586  ax-addass 9587  ax-mulass 9588  ax-distr 9589  ax-i2m1 9590  ax-1ne0 9591  ax-1rid 9592  ax-rrecex 9594  ax-cnre 9595
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-iota 5533  df-fv 5577  df-ov 6281  df-2 10635  df-3 10636  df-4 10637  df-5 10638  df-6 10639  df-7 10640  df-8 10641  df-9 10642  df-10 10643
This theorem is referenced by:  5t3e15  11093  dec2dvds  14758  dec5dvds  14759  dec5nprm  14761  dec2nprm  14762  2exp16  14784  10nprm  14808  1259lem1  14822  1259lem4  14825  2503lem1  14828  2503lem2  14829  2503lem3  14830  4001lem1  14832  4001lem4  14835  4001prm  14836  log2ublem3  23604  log2ub  23605  bclbnd  23936  bpos1  23939  bposlem4  23943  bposlem5  23944  bposlem8  23947  41prothprm  37865
  Copyright terms: Public domain W3C validator