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

Theorem 1t1e1 10468
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 9339 . 2  |-  1  e.  CC
21mulid1i 9387 1  |-  ( 1  x.  1 )  =  1
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369  (class class class)co 6090   1c1 9282    x. cmul 9286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-resscn 9338  ax-1cn 9339  ax-icn 9340  ax-addcl 9341  ax-mulcl 9343  ax-mulcom 9345  ax-mulass 9347  ax-distr 9348  ax-1rid 9351  ax-cnre 9354
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ral 2719  df-rex 2720  df-rab 2723  df-v 2973  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-sn 3877  df-pr 3879  df-op 3883  df-uni 4091  df-br 4292  df-iota 5380  df-fv 5425  df-ov 6093
This theorem is referenced by:  neg1mulneg1e1  10538  addltmul  10559  1exp  11892  expge1  11900  mulexp  11902  mulexpz  11903  expaddz  11907  sqrecii  11947  i4  11967  facp1  12055  hashf1  12209  binom  13292  rpmul  13808  2503lem2  14161  4001lem4  14167  abvtrivd  16924  evpmodpmf1o  18025  iimulcl  20508  dvexp  21426  dvef  21451  mulcxplem  22128  cxpmul2  22133  dvsqr  22181  abscxpbnd  22190  1cubr  22236  dchrmulcl  22587  dchr1cl  22589  dchrinvcl  22591  lgslem3  22636  lgsval2lem  22644  lgsneg  22657  lgsdilem  22660  lgsdir  22668  lgsdi  22670  lgsquad2lem1  22696  lgsquad2lem2  22697  dchrisum0flblem2  22757  rpvmasum2  22760  mudivsum  22778  pntibndlem2  22839  axlowdimlem6  23192  hisubcomi  24505  lnophmlem2  25420  sgnmul  26924  subfacval2  27074  m1expevenALT  27106  prodf1  27405  prodfrec  27409  fprodmul  27470  fallfac0  27530  binomfallfac  27543  faclim2  27553  dvcnsqr  28476  pell1234qrmulcl  29194  pellqrex  29218  stoweidlem13  29806  stoweidlem16  29809  wallispi  29863  wallispi2lem2  29865
  Copyright terms: Public domain W3C validator