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

Theorem 1t1e1 10704
Description: 1 times 1 equals 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
1t1e1  |-  ( 1  x.  1 )  =  1

Proof of Theorem 1t1e1
StepHypRef Expression
1 ax-1cn 9567 . 2  |-  1  e.  CC
21mulid1i 9615 1  |-  ( 1  x.  1 )  =  1
Colors of variables: wff setvar class
Syntax hints:    = wceq 1395  (class class class)co 6296   1c1 9510    x. cmul 9514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-mulcl 9571  ax-mulcom 9573  ax-mulass 9575  ax-distr 9576  ax-1rid 9579  ax-cnre 9582
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-iota 5557  df-fv 5602  df-ov 6299
This theorem is referenced by:  neg1mulneg1e1  10774  addltmul  10795  1exp  12198  expge1  12206  mulexp  12208  mulexpz  12209  expaddz  12213  sqrecii  12253  i4  12273  facp1  12361  hashf1  12510  binom  13654  prodf1  13712  prodfrec  13716  fprodmul  13777  rpmul  14276  2503lem2  14632  4001lem4  14638  abvtrivd  17616  iimulcl  21563  dvexp  22482  dvef  22507  mulcxplem  23191  cxpmul2  23196  dvsqrt  23244  abscxpbnd  23253  1cubr  23299  dchrmulcl  23650  dchr1cl  23652  dchrinvcl  23654  lgslem3  23699  lgsval2lem  23707  lgsneg  23720  lgsdilem  23723  lgsdir  23731  lgsdi  23733  lgsquad2lem1  23759  lgsquad2lem2  23760  dchrisum0flblem2  23820  rpvmasum2  23823  mudivsum  23841  pntibndlem2  23902  axlowdimlem6  24377  hisubcomi  26148  lnophmlem2  27063  sgnmul  28678  subfacval2  28828  m1expevenALT  28860  fallfac0  29368  binomfallfac  29381  faclim2  29391  dvcnsqrt  30306  pell1234qrmulcl  30995  pellqrex  31019  binomcxplemnotnn0  31465  fprodge1  31801  dvnprodlem3  31948  stoweidlem13  31998  stoweidlem16  32001  wallispi  32055  wallispi2lem2  32057
  Copyright terms: Public domain W3C validator