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

Theorem 1cnd 10094
Description: 1 is a complex number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
1cnd (𝜑 → 1 ∈ ℂ)

Proof of Theorem 1cnd
StepHypRef Expression
1 ax-1cn 10032 . 2 1 ∈ ℂ
21a1i 11 1 (𝜑 → 1 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cc 9972  1c1 9975
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 10032
This theorem is referenced by:  adddirp1d  10104  1p1times  10245  addcom  10260  addcomd  10276  muladd11r  10287  pncan1  10492  npcan1  10493  muls1d  10529  mulsubfacd  10530  recrec  10760  rec11  10761  rec11r  10762  rereccl  10781  subrec  10892  nn1m1nn  11078  add1p1  11321  sub1m1  11322  cnm2m1cnm3  11323  xp1d2m1eqxm1d2  11324  div4p1lem1div2  11325  nn0n0n1ge2  11396  zneo  11498  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  lincmb01cmp  12353  iccf1o  12354  xov1plusxeqvd  12356  zpnn0elfzo1  12581  ubmelm1fzo  12604  fzosplitpr  12617  fzosplitprm1  12618  fzoshftral  12625  fladdz  12666  2tnp1ge0ge0  12670  ltdifltdiv  12675  dfceil2  12680  negmod  12755  modnegd  12765  addmodlteq  12785  binom2sub1  13022  binom3  13025  zesq  13027  sqoddm1div8  13068  bcm1k  13142  bcp1n  13143  bcp1m1  13147  bcpasc  13148  bcn2m1  13151  hashfz  13252  hashfzo  13254  hashfzp1  13256  hashf1lem2  13278  hashf1  13279  brfi1indlem  13316  lswccatn0lsw  13409  ccatws1lenp1b  13439  swrdccatwrd  13514  revccat  13561  repswrevw  13579  cshwidxm1  13599  cshwidxn  13601  cshweqrep  13613  cshimadifsn0  13622  swrd2lsw  13741  relexpaddnn  13835  absexpz  14089  reccn2  14371  rlimno1  14428  isercolllem1  14439  isercoll2  14443  iseraltlem2  14457  iseraltlem3  14458  hashiun  14598  hash2iun1dif1  14600  binomlem  14605  bcxmas  14611  incexc  14613  incexc2  14614  climcndslem1  14625  arisum  14636  arisum2  14637  trireciplem  14638  pwm1geoser  14644  geolim2  14646  georeclim  14647  mertenslem1  14660  prodfrec  14671  ntrivcvg  14673  ntrivcvgtail  14676  prodrblem  14703  prodmolem2a  14708  fprodntriv  14716  prod1  14718  fprodser  14723  fprodcl  14726  fprodm1  14741  fprodp1  14743  risefacval2  14785  fallfacval2  14786  risefacp1  14804  fallfacp1  14805  risefacfac  14810  fallfacfwd  14811  binomfallfaclem2  14815  fallfacval4  14818  bpolydiflem  14829  ef0lem  14853  tanaddlem  14940  tanadd  14941  cos01bnd  14960  oddm1even  15114  oddp1even  15115  oexpneg  15116  ltoddhalfle  15132  halfleoddlt  15133  nn0ob  15147  pwp1fsum  15161  flodddiv4  15184  bitsp1o  15202  bitsf1  15215  sadcp1  15224  qredeu  15419  prmdiv  15537  prmdiveq  15538  vfermltlALT  15554  pcexp  15611  pc2dvds  15630  4sqlem11  15706  4sqlem12  15707  vdwapun  15725  vdwlem3  15734  vdwlem6  15737  vdwlem9  15740  ramub1lem2  15778  prmop1  15789  prmdvdsprmo  15793  prmgaplem8  15809  cshwshashnsame  15857  gsumccat  17425  mulgnnass  17623  mulgnnassOLD  17624  psgnunilem5  17960  psgnunilem2  17961  sylow1lem1  18059  efgredlemc  18204  odadd2  18298  srgbinomlem3  18588  srgbinomlem4  18589  cncrng  19815  cnfldmulg  19826  gzrngunit  19860  zringunit  19884  prmirredlem  19889  cayhamlem1  20719  expcn  22722  iirevcn  22776  iihalf2cn  22780  icchmeo  22787  icopnfcnv  22788  icopnfhmeo  22789  evth  22805  pjthlem1  23254  ovolunlem1a  23310  ovolunlem1  23311  opnmbllem  23415  mbfi1fseqlem6  23532  bddibl  23651  dvnadd  23737  dvmptid  23765  dvmptdiv  23782  dvcnvlem  23784  dveflem  23787  dvsincos  23789  dvlipcn  23802  dvivthlem1  23816  lhop2  23823  dvcvx  23828  dvfsumle  23829  dvfsumabs  23831  dvfsumlem1  23834  dvfsumlem2  23835  ply1divex  23941  fta1glem1  23970  dgrcolem1  24074  dgrcolem2  24075  aaliou3lem2  24143  aaliou3lem8  24145  dvtaylp  24169  dvntaylp  24170  taylthlem1  24172  taylthlem2  24173  abelthlem1  24230  abelthlem2  24231  abelthlem6  24235  abelthlem7  24237  logdivlti  24411  advlog  24445  advlogexp  24446  logtayl  24451  cxpmul2  24480  dvcxp1  24526  dvcxp2  24527  dvcncxp1  24529  dvcnsqrt  24530  loglesqrt  24544  relogbdiv  24562  ang180lem4  24587  ang180lem5  24588  isosctrlem2  24594  isosctrlem3  24595  affineequiv  24598  affineequiv2  24599  angpieqvdlem  24600  chordthmlem2  24605  chordthmlem3  24606  chordthmlem5  24608  dcubic2  24616  dcubic  24618  quart1lem  24627  quart1  24628  quart  24633  asinlem  24640  asinlem3  24643  atansopn  24704  dvatan  24707  leibpi  24714  birthdaylem2  24724  efrlim  24741  cxplim  24743  divsqrtsumlem  24751  logdifbnd  24765  emcllem2  24768  emcllem3  24769  emcllem5  24771  zetacvg  24786  lgamgulmlem2  24801  lgamgulmlem3  24802  lgamgulmlem4  24803  lgamgulmlem5  24804  lgamgulmlem6  24805  lgamgulm2  24807  lgamcvg2  24826  gamcvg  24827  gamcvg2lem  24830  lgam1  24835  gamfac  24838  wilthimp  24843  ftalem5  24848  basellem3  24854  basellem5  24856  basellem8  24859  basellem9  24860  sqff1o  24953  muinv  24964  logfaclbnd  24992  logfacrlim  24994  logexprlim  24995  perfectlem2  25000  dchr1cl  25021  dchrinvcl  25023  dchrfi  25025  dchr1  25027  dchrsum2  25038  bcmono  25047  bcp1ctr  25049  bclbnd  25050  bposlem1  25054  bposlem9  25062  gausslemma2dlem1a  25135  gausslemma2dlem5  25141  lgseisenlem4  25148  lgsquadlem1  25150  m1lgs  25158  2lgslem3a  25166  2lgslem3b  25167  2lgslem3c  25168  2lgslem3d  25169  2lgslem3d1  25173  2lgsoddprmlem1  25178  2sqlem8  25196  chtppilim  25209  rpvmasumlem  25221  dchrisumlem1  25223  dchrisum0re  25247  dchrisum0lem2a  25251  mudivsum  25264  mulogsumlem  25265  mulogsum  25266  2vmadivsumlem  25274  selberg4lem1  25294  pntrsumo1  25299  selberg34r  25305  pntrlog2bndlem2  25312  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntrlog2bndlem6  25317  pntibndlem2  25325  pntlemg  25332  pntlemr  25336  pntlemf  25339  pntlemk  25340  pntlemo  25341  pntlem3  25343  ostth2lem2  25368  ttgcontlem1  25810  cusgrsize2inds  26405  wlklenvclwlk  26607  pthdadjvtx  26682  crctcshwlkn0lem1  26758  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  wlklnwwlkln2lem  26836  wwlksnred  26855  wwlksnextbi  26857  wwlksnredwwlkn  26858  wwlksnextwrd  26860  wwlksnextinj  26862  wwlksnextproplem2  26873  wwlksnextproplem3  26874  clwlkclwwlklem2a1  26958  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwlkclwwlklem2  26966  clwlkclwwlklem3  26967  clwlkclwwlk  26968  clwwisshclwwslemlem  26970  clwwisshclwws  26972  clwwlkel  27009  clwwlkf  27010  clwwlkwwlksb  27018  clwwlkext2edg  27020  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  clwwlknonex2lem1  27082  clwwlknonex2lem2  27083  eucrct2eupth  27223  extwwlkfablem1OLD  27323  2clwwlk2clwwlklem2lem2  27329  clwwlkccatlem  27331  numclwlk1lem2foalem  27341  numclwlk1lem2fo  27348  numclwlk2lem2f  27357  numclwlk2lem2f1o  27359  numclwlk2lem2fOLD  27364  numclwlk2lem2f1oOLD  27366  numclwwlk6  27377  smcnlem  27680  bcm1n  29682  ltesubnnd  29696  omndmul2  29840  archirngz  29871  archiabllem1a  29873  archiabllem2c  29877  psgnfzto1stlem  29978  1smat1  29998  madjusmdetlem2  30022  madjusmdetlem4  30024  dya2icoseg  30467  iwrdsplit  30577  fibp1  30591  ballotlemfp1  30681  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemic  30696  ballotlem1c  30697  ballotlemsgt1  30700  ballotlemsdom  30701  ballotlemsel1i  30702  ballotlemsi  30704  ballotlemsima  30705  ballotlem1ri  30724  sgn0bi  30737  signstfvn  30774  signsvtn0  30775  signstfveq0  30782  signsvfn  30787  signsvtn  30789  signshf  30793  hashreprin  30826  circlemeth  30846  logdivsqrle  30856  subfacp1lem1  31287  subfacp1lem5  31292  cvxpconn  31350  sinccvglem  31692  divcnvlin  31744  bcm1nt  31749  bcprod  31750  bccolsum  31751  iprodgam  31754  faclimlem1  31755  faclimlem2  31756  faclimlem3  31757  faclim  31758  iprodfac  31759  faclim2  31760  fwddifnp1  32397  dnizphlfeqhlf  32591  dnibndlem3  32595  dnibndlem13  32605  unblimceq0  32623  knoppndvlem6  32633  knoppndvlem9  32636  knoppndvlem14  32641  knoppndvlem15  32642  knoppndvlem16  32643  knoppndvlem17  32644  bj-bary1lem1  33291  poimirlem25  33564  poimirlem26  33565  poimirlem32  33571  opnmbllem0  33575  itg2addnclem2  33592  dvasin  33626  dvacos  33627  areacirclem1  33630  areacirclem4  33633  areacirc  33635  bfp  33753  pell1qrge1  37751  rmspecfund  37791  acongeq  37867  jm2.18  37872  jm2.19lem3  37875  jm2.25  37883  jm2.16nn0  37888  jm3.1lem1  37901  jm3.1lem2  37902  itgpowd  38117  areaquad  38119  relexpmulnn  38318  relexpaddss  38327  cvgdvgrat  38829  radcnvrat  38830  hashnzfzclim  38838  ofdivrec  38842  expgrowthi  38849  bccm1k  38858  dvradcnv2  38863  binomcxplemwb  38864  binomcxplemnn0  38865  binomcxplemrat  38866  binomcxplemfrat  38867  binomcxplemdvbinom  38869  binomcxplemnotnn0  38872  refsum2cnlem1  39510  fzisoeu  39828  fperiodmullem  39831  fzdifsuc2  39838  xralrple2  39883  nnsplit  39887  infleinflem2  39900  fmul01lt1lem2  40135  fprodcn  40150  clim1fr1  40151  isumneg  40152  climneg  40160  sumnnodd  40180  reclimc  40203  coseq0  40393  coskpi2  40395  cosknegpi  40398  fprodcncf  40432  fprodsubrecnncnvlem  40439  fprodaddrecnncnvlem  40441  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnxpaek  40475  dvnmul  40476  dvmptfprod  40478  dvnprodlem3  40481  itgsinexp  40488  itgiccshift  40514  itgperiod  40515  itgsbtaddcnst  40516  stoweidlem1  40536  stoweidlem7  40542  stoweidlem10  40545  stoweidlem11  40546  stoweidlem14  40549  stoweidlem17  40552  stoweidlem34  40569  stoweidlem42  40577  wallispilem3  40602  wallispilem5  40604  wallispi  40605  wallispi2lem1  40606  wallispi2lem2  40607  wallispi2  40608  stirlinglem1  40609  stirlinglem3  40611  stirlinglem4  40612  stirlinglem5  40613  stirlinglem6  40614  stirlinglem7  40615  stirlinglem8  40616  stirlinglem10  40618  stirlinglem11  40619  stirlinglem12  40620  stirlinglem13  40621  stirlinglem15  40623  dirkertrigeqlem2  40634  dirkertrigeqlem3  40635  dirkertrigeq  40636  dirkercncflem1  40638  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem11  40653  fourierdlem15  40657  fourierdlem26  40668  fourierdlem36  40678  fourierdlem40  40682  fourierdlem41  40683  fourierdlem42  40684  fourierdlem48  40689  fourierdlem49  40690  fourierdlem56  40697  fourierdlem58  40699  fourierdlem59  40700  fourierdlem62  40703  fourierdlem64  40705  fourierdlem65  40706  fourierdlem78  40719  fourierdlem79  40720  sqwvfoura  40763  fourierswlem  40765  fouriersw  40766  etransclem23  40792  etransclem24  40793  etransclem28  40797  etransclem35  40804  etransclem38  40807  nnfoctbdjlem  40990  smfmullem1  41319  sigaradd  41376  deccarry  41646  fargshiftf1  41702  fargshiftfo  41703  fmtnof1  41772  sqrtpwpw2p  41775  fmtnorec2lem  41779  fmtnorec4  41786  fmtnoprmfac1lem  41801  fmtnoprmfac1  41802  fmtnoprmfac2  41804  pwdif  41826  pwm1geoserALT  41827  2pwp1prm  41828  mod42tp1mod8  41844  sfprmdvdsmersenne  41845  lighneallem3  41849  lighneallem4  41852  onego  41884  zofldiv2ALTV  41899  oexpnegALTV  41913  opoeALTV  41919  opeoALTV  41920  epee  41939  perfectALTVlem1  41955  0nodd  42135  2nodd  42137  nnsgrpnmnd  42143  1neven  42257  altgsumbc  42455  pw2m1lepw2m1  42635  m1modmmod  42641  zofldiv2  42650  nnpw2pmod  42702  blen1b  42707  blennn0em1  42710  dignn0flhalflem1  42734  dignn0flhalflem2  42735  nn0sumshdiglemB  42739  nn0sumshdiglem1  42740  nn0sumshdiglem2  42741
  Copyright terms: Public domain W3C validator