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

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

Proof of Theorem 1cnd
StepHypRef Expression
1 ax-1cn 10277 . 2 1 ∈ ℂ
21a1i 11 1 (𝜑 → 1 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  cc 10217  1c1 10220
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 10277
This theorem is referenced by:  adddirp1d  10349  1p1times  10490  addcom  10505  addcomd  10521  muladd11r  10532  pncan1  10737  npcan1  10738  muls1d  10774  mulsubfacd  10775  recrec  11005  rec11  11006  rec11r  11007  rereccl  11026  subrec  11137  nn1m1nn  11323  add1p1  11548  sub1m1  11549  cnm2m1cnm3  11550  xp1d2m1eqxm1d2  11551  div4p1lem1div2  11552  nn0n0n1ge2  11622  zneo  11724  rpnnen1lem5  12035  lincmb01cmp  12536  iccf1o  12537  xov1plusxeqvd  12539  zpnn0elfzo1  12764  ubmelm1fzo  12786  fzosplitpr  12799  fzosplitprm1  12800  fzoshftral  12807  fladdz  12848  2tnp1ge0ge0  12852  ltdifltdiv  12857  dfceil2  12862  negmod  12937  modnegd  12947  addmodlteq  12967  binom2sub1  13203  binom3  13206  zesq  13208  sqoddm1div8  13249  bcm1k  13320  bcp1n  13321  bcp1m1  13325  bcpasc  13326  bcn2m1  13329  hashfz  13429  hashfzo  13431  hashfzp1  13433  hashf1lem2  13455  hashf1  13456  hashdifsnp1  13493  lswccatn0lsw  13586  ccatws1lenp1b  13615  swrdccatwrd  13690  revccat  13737  repswrevw  13755  cshwidxm1  13775  cshwidxn  13777  cshweqrep  13789  cshimadifsn0  13798  swrds2m  13908  swrd2lsw  13918  relexpaddnn  14012  absexpz  14266  reccn2  14548  rlimno1  14605  isercolllem1  14616  isercoll2  14620  iseraltlem2  14634  iseraltlem3  14635  hashiun  14774  hash2iun1dif1  14776  binomlem  14781  bcxmas  14787  incexc  14789  incexc2  14790  climcndslem1  14801  arisum  14812  arisum2  14813  trireciplem  14814  pwm1geoser  14820  geolim2  14822  georeclim  14823  mertenslem1  14835  prodfrec  14846  ntrivcvg  14848  ntrivcvgtail  14851  prodrblem  14878  prodmolem2a  14883  fprodntriv  14891  prod1  14893  fprodser  14898  fprodcl  14901  fprodm1  14916  fprodp1  14918  risefacval2  14959  fallfacval2  14960  risefacp1  14978  fallfacp1  14979  risefacfac  14984  fallfacfwd  14985  binomfallfaclem2  14989  fallfacval4  14992  bpolydiflem  15003  ef0lem  15027  tanaddlem  15114  tanadd  15115  cos01bnd  15134  oddm1even  15285  oddp1even  15286  oexpneg  15287  ltoddhalfle  15303  halfleoddlt  15304  nn0ob  15318  pwp1fsum  15332  flodddiv4  15354  bitsp1o  15372  bitsf1  15385  sadcp1  15394  qredeu  15588  prmdiv  15705  prmdiveq  15706  vfermltlALT  15722  pcexp  15779  pc2dvds  15798  4sqlem11  15874  4sqlem12  15875  vdwapun  15893  vdwlem3  15902  vdwlem6  15905  vdwlem9  15908  ramub1lem2  15946  prmop1  15957  prmdvdsprmo  15961  prmgaplem8  15977  cshwshashnsame  16020  gsumccat  17581  mulgnnass  17777  psgnunilem5  18113  psgnunilem2  18114  sylow1lem1  18212  efgredlemc  18357  odadd2  18451  srgbinomlem3  18742  srgbinomlem4  18743  cncrng  19973  cnfldmulg  19984  gzrngunit  20018  zringunit  20042  prmirredlem  20047  cayhamlem1  20882  expcn  22886  iirevcn  22940  iihalf2cn  22944  icchmeo  22951  icopnfcnv  22952  icopnfhmeo  22953  evth  22969  pjthlem1  23418  ovolunlem1a  23475  ovolunlem1  23476  opnmbllem  23580  mbfi1fseqlem6  23699  bddibl  23818  dvnadd  23904  dvmptid  23932  dvmptdiv  23949  dvcnvlem  23951  dveflem  23954  dvsincos  23956  dvlipcn  23969  dvivthlem1  23983  lhop2  23990  dvcvx  23995  dvfsumle  23996  dvfsumabs  23998  dvfsumlem1  24001  dvfsumlem2  24002  ply1divex  24108  fta1glem1  24137  dgrcolem1  24241  dgrcolem2  24242  aaliou3lem2  24310  aaliou3lem8  24312  dvtaylp  24336  dvntaylp  24337  taylthlem1  24339  taylthlem2  24340  abelthlem1  24397  abelthlem2  24398  abelthlem6  24402  abelthlem7  24404  logdivlti  24578  advlog  24612  advlogexp  24613  logtayl  24618  cxpmul2  24647  dvcxp1  24693  dvcxp2  24694  dvcncxp1  24696  dvcnsqrt  24697  loglesqrt  24711  relogbdiv  24729  ang180lem4  24754  ang180lem5  24755  isosctrlem2  24761  isosctrlem3  24762  affineequiv  24765  affineequiv2  24766  angpieqvdlem  24767  chordthmlem2  24772  chordthmlem3  24773  chordthmlem5  24775  dcubic2  24783  dcubic  24785  quart1lem  24794  quart1  24795  quart  24800  asinlem  24807  asinlem3  24810  atansopn  24871  dvatan  24874  leibpi  24881  birthdaylem2  24891  efrlim  24908  cxplim  24910  divsqrtsumlem  24918  logdifbnd  24932  emcllem2  24935  emcllem3  24936  emcllem5  24938  zetacvg  24953  lgamgulmlem2  24968  lgamgulmlem3  24969  lgamgulmlem4  24970  lgamgulmlem5  24971  lgamgulmlem6  24972  lgamgulm2  24974  lgamcvg2  24993  gamcvg  24994  gamcvg2lem  24997  lgam1  25002  gamfac  25005  wilthimp  25010  ftalem5  25015  basellem3  25021  basellem5  25023  basellem8  25026  basellem9  25027  sqff1o  25120  muinv  25131  logfaclbnd  25159  logfacrlim  25161  logexprlim  25162  perfectlem2  25167  dchr1cl  25188  dchrinvcl  25190  dchrfi  25192  dchr1  25194  dchrsum2  25205  bcmono  25214  bcp1ctr  25216  bclbnd  25217  bposlem1  25221  bposlem9  25229  gausslemma2dlem1a  25302  gausslemma2dlem5  25308  lgseisenlem4  25315  lgsquadlem1  25317  m1lgs  25325  2lgslem3a  25333  2lgslem3b  25334  2lgslem3c  25335  2lgslem3d  25336  2lgslem3d1  25340  2lgsoddprmlem1  25345  2sqlem8  25363  chtppilim  25376  rpvmasumlem  25388  dchrisumlem1  25390  dchrisum0re  25414  dchrisum0lem2a  25418  mudivsum  25431  mulogsumlem  25432  mulogsum  25433  2vmadivsumlem  25441  selberg4lem1  25461  pntrsumo1  25466  selberg34r  25472  pntrlog2bndlem2  25479  pntrlog2bndlem4  25481  pntrlog2bndlem5  25482  pntrlog2bndlem6  25484  pntibndlem2  25492  pntlemg  25499  pntlemr  25503  pntlemf  25506  pntlemk  25507  pntlemo  25508  pntlem3  25510  ostth2lem2  25535  ttgcontlem1  25977  cusgrsize2inds  26575  wlklenvclwlk  26777  pthdadjvtx  26852  crctcshwlkn0lem1  26929  crctcshwlkn0lem4  26932  crctcshwlkn0lem5  26933  wlklnwwlkln2lem  27007  wlknwwlksnbij  27017  wwlksnred  27027  wwlksnextbi  27029  wwlksnredwwlkn  27030  wwlksnextwrd  27032  wwlksnextinj  27034  wwlksnextproplem2  27046  wwlksnextproplem3  27047  clwwlkccatlem  27130  clwlkclwwlklem2a1  27133  clwlkclwwlklem2a4  27138  clwlkclwwlklem2a  27139  clwlkclwwlklem2  27141  clwlkclwwlklem3  27142  clwlkclwwlk  27143  clwwisshclwwslemlem  27154  clwwisshclwws  27156  clwwlkel  27193  clwwlkf  27194  clwwlkwwlksb  27202  clwwlkext2edg  27204  wwlksext2clwwlk  27205  wwlksext2clwwlkOLD  27206  clwwlknonex2lem1  27274  clwwlknonex2lem2  27275  eucrct2eupth  27416  extwwlkfablem1OLD  27515  numclwwlk1lem2foalem  27528  numclwwlk1lem2fo  27535  numclwlk2lem2f  27555  numclwlk2lem2f1o  27557  numclwlk2lem2fOLD  27562  numclwlk2lem2f1oOLD  27564  numclwwlk6  27576  smcnlem  27878  bcm1n  29879  ltesubnnd  29893  omndmul2  30035  archirngz  30066  archiabllem1a  30068  archiabllem2c  30072  psgnfzto1stlem  30173  1smat1  30193  madjusmdetlem2  30217  madjusmdetlem4  30219  dya2icoseg  30662  iwrdsplit  30772  fibp1  30786  ballotlemfp1  30876  ballotlemfc0  30877  ballotlemfcc  30878  ballotlemic  30891  ballotlem1c  30892  ballotlemsgt1  30895  ballotlemsdom  30896  ballotlemsel1i  30897  ballotlemsi  30899  ballotlemsima  30900  ballotlem1ri  30919  sgn0bi  30932  signstfvn  30969  signsvtn0  30970  signstfveq0  30977  signsvfn  30982  signsvtn  30984  signshf  30988  hashreprin  31021  circlemeth  31041  logdivsqrle  31051  subfacp1lem1  31482  subfacp1lem5  31487  cvxpconn  31545  sinccvglem  31886  divcnvlin  31938  bcm1nt  31943  bcprod  31944  bccolsum  31945  iprodgam  31948  faclimlem1  31949  faclimlem2  31950  faclimlem3  31951  faclim  31952  iprodfac  31953  faclim2  31954  fwddifnp1  32591  dnizphlfeqhlf  32781  dnibndlem3  32785  dnibndlem13  32795  unblimceq0  32813  knoppndvlem6  32823  knoppndvlem9  32826  knoppndvlem14  32831  knoppndvlem15  32832  knoppndvlem16  32833  knoppndvlem17  32834  bj-bary1lem1  33476  poimirlem25  33745  poimirlem26  33746  poimirlem32  33752  opnmbllem0  33756  itg2addnclem2  33772  dvasin  33806  dvacos  33807  areacirclem1  33810  areacirclem4  33813  areacirc  33815  bfp  33932  pell1qrge1  37934  rmspecfund  37973  acongeq  38049  jm2.18  38054  jm2.19lem3  38057  jm2.25  38065  jm2.16nn0  38070  jm3.1lem1  38083  jm3.1lem2  38084  itgpowd  38298  areaquad  38300  relexpmulnn  38499  relexpaddss  38508  cvgdvgrat  39010  radcnvrat  39011  hashnzfzclim  39019  ofdivrec  39023  expgrowthi  39030  bccm1k  39039  dvradcnv2  39044  binomcxplemwb  39045  binomcxplemnn0  39046  binomcxplemrat  39047  binomcxplemfrat  39048  binomcxplemdvbinom  39050  binomcxplemnotnn0  39053  refsum2cnlem1  39688  fzisoeu  39993  fperiodmullem  39996  fzdifsuc2  40003  xralrple2  40048  nnsplit  40052  infleinflem2  40065  fmul01lt1lem2  40295  fprodcn  40310  clim1fr1  40311  isumneg  40312  climneg  40320  sumnnodd  40340  reclimc  40363  coseq0  40553  coskpi2  40555  cosknegpi  40558  fprodcncf  40592  fprodsubrecnncnvlem  40599  fprodaddrecnncnvlem  40601  ioodvbdlimc1lem2  40625  ioodvbdlimc2lem  40627  dvnxpaek  40635  dvnmul  40636  dvmptfprod  40638  dvnprodlem3  40641  itgsinexp  40648  itgiccshift  40673  itgperiod  40674  itgsbtaddcnst  40675  stoweidlem1  40695  stoweidlem7  40701  stoweidlem10  40704  stoweidlem11  40705  stoweidlem14  40708  stoweidlem17  40711  stoweidlem34  40728  stoweidlem42  40736  wallispilem3  40761  wallispilem5  40763  wallispi  40764  wallispi2lem1  40765  wallispi2lem2  40766  wallispi2  40767  stirlinglem1  40768  stirlinglem3  40770  stirlinglem4  40771  stirlinglem5  40772  stirlinglem6  40773  stirlinglem7  40774  stirlinglem8  40775  stirlinglem10  40777  stirlinglem11  40778  stirlinglem12  40779  stirlinglem13  40780  stirlinglem15  40782  dirkertrigeqlem2  40793  dirkertrigeqlem3  40794  dirkertrigeq  40795  dirkercncflem1  40797  dirkercncflem2  40798  dirkercncflem4  40800  fourierdlem11  40812  fourierdlem15  40816  fourierdlem26  40827  fourierdlem36  40837  fourierdlem40  40841  fourierdlem41  40842  fourierdlem42  40843  fourierdlem48  40848  fourierdlem49  40849  fourierdlem56  40856  fourierdlem58  40858  fourierdlem59  40859  fourierdlem62  40862  fourierdlem64  40864  fourierdlem65  40865  fourierdlem78  40878  fourierdlem79  40879  sqwvfoura  40922  fourierswlem  40924  fouriersw  40925  etransclem23  40951  etransclem24  40952  etransclem28  40956  etransclem35  40963  etransclem38  40966  nnfoctbdjlem  41149  smfmullem1  41478  sigaradd  41535  deccarry  41894  fargshiftf1  41950  fargshiftfo  41951  fmtnof1  42020  sqrtpwpw2p  42023  fmtnorec2lem  42027  fmtnorec4  42034  fmtnoprmfac1lem  42049  fmtnoprmfac1  42050  fmtnoprmfac2  42052  pwdif  42074  pwm1geoserALT  42075  2pwp1prm  42076  mod42tp1mod8  42092  sfprmdvdsmersenne  42093  lighneallem3  42097  lighneallem4  42100  onego  42132  zofldiv2ALTV  42147  oexpnegALTV  42161  opoeALTV  42167  opeoALTV  42168  epee  42187  perfectALTVlem1  42203  0nodd  42376  2nodd  42378  nnsgrpnmnd  42384  1neven  42498  altgsumbc  42696  pw2m1lepw2m1  42876  m1modmmod  42882  zofldiv2  42891  nnpw2pmod  42943  blen1b  42948  blennn0em1  42951  dignn0flhalflem1  42975  dignn0flhalflem2  42976  nn0sumshdiglemB  42980  nn0sumshdiglem1  42981  nn0sumshdiglem2  42982
  Copyright terms: Public domain W3C validator