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

Theorem 1cnd 10625
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 10584 . 2 1 ∈ ℂ
21a1i 11 1 (𝜑 → 1 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cc 10524  1c1 10527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 10584
This theorem is referenced by:  adddirp1d  10656  1p1times  10800  addcom  10815  addcomd  10831  muladd11r  10842  pncan1  11053  npcan1  11054  muls1d  11089  mulsubfacd  11090  recrec  11326  rec11  11327  rec11r  11328  rereccl  11347  subrec  11458  nn1m1nn  11647  add1p1  11877  sub1m1  11878  cnm2m1cnm3  11879  xp1d2m1eqxm1d2  11880  div4p1lem1div2  11881  nn0n0n1ge2  11951  zneo  12054  rpnnen1lem5  12370  lincmb01cmp  12871  iccf1o  12872  xov1plusxeqvd  12874  zpnn0elfzo1  13101  ubmelm1fzo  13123  fzosplitpr  13136  fzosplitprm1  13137  fzoshftral  13144  fladdz  13185  2tnp1ge0ge0  13189  ltdifltdiv  13194  dfceil2  13199  negmod  13274  modnegd  13284  addmodlteq  13304  binom2sub1  13572  binom3  13575  zesq  13577  sqoddm1div8  13594  bcm1k  13665  bcp1n  13666  bcp1m1  13670  bcpasc  13671  bcn2m1  13674  hashfz  13778  hashfzo  13780  hashfzp1  13782  hashf1lem2  13804  hashf1  13805  hashdifsnp1  13844  lswccatn0lsw  13935  ccatws1lenp1b  13965  revccat  14118  repswrevw  14139  cshwidxm1  14159  cshwidxn  14161  cshweqrep  14173  cshimadifsn0  14182  swrds2m  14293  swrd2lsw  14304  relexpaddnn  14400  absexpz  14655  reccn2  14943  rlimno1  15000  isercolllem1  15011  isercoll2  15015  iseraltlem2  15029  iseraltlem3  15030  hashiun  15167  hash2iun1dif1  15169  binomlem  15174  bcxmas  15180  incexc  15182  incexc2  15183  climcndslem1  15194  arisum  15205  arisum2  15206  trireciplem  15207  pwdif  15213  pwm1geoser  15214  pwm1geoserOLD  15215  geolim2  15217  georeclim  15218  mertenslem1  15230  prodfrec  15241  ntrivcvg  15243  ntrivcvgtail  15246  prodrblem  15273  prodmolem2a  15278  fprodntriv  15286  prod1  15288  fprodser  15293  fprodcl  15296  fprodm1  15311  fprodp1  15313  fprodclf  15336  risefacval2  15354  fallfacval2  15355  risefacp1  15373  fallfacp1  15374  risefacfac  15379  fallfacfwd  15380  binomfallfaclem2  15384  fallfacval4  15387  bpolydiflem  15398  ef0lem  15422  tanaddlem  15509  tanadd  15510  cos01bnd  15529  oddm1even  15682  oddp1even  15683  oexpneg  15684  ltoddhalfle  15700  halfleoddlt  15701  nn0ob  15725  pwp1fsum  15732  flodddiv4  15754  bitsp1o  15772  bitsf1  15785  sadcp1  15794  qredeu  15992  prmdiv  16112  prmdiveq  16113  vfermltlALT  16129  pc2dvds  16205  4sqlem11  16281  4sqlem12  16282  vdwapun  16300  vdwlem3  16309  vdwlem6  16312  vdwlem9  16315  ramub1lem2  16353  prmop1  16364  prmdvdsprmo  16368  prmgaplem8  16384  cshwshashnsame  16427  gsumsgrpccat  17994  gsumccatOLD  17995  psgnunilem5  18553  psgnunilem2  18554  sylow1lem1  18654  efgredlemc  18802  odadd2  18900  ablsimpgfindlem1  19160  srgbinomlem3  19223  srgbinomlem4  19224  cncrng  20496  gzrngunit  20541  zringunit  20565  prmirredlem  20570  cayhamlem1  21404  expcn  23409  iirevcn  23463  iihalf2cn  23467  icchmeo  23474  icopnfcnv  23475  icopnfhmeo  23476  evth  23492  pcoass  23557  pjthlem1  23969  ovolunlem1a  24026  ovolunlem1  24027  opnmbllem  24131  mbfi1fseqlem6  24250  bddibl  24369  dvnadd  24455  dvmptid  24483  dvmptdiv  24500  dvcnvlem  24502  dveflem  24505  dvef  24506  dvsincos  24507  dvlipcn  24520  dvivthlem1  24534  lhop2  24541  dvcvx  24546  dvfsumle  24547  dvfsumabs  24549  dvfsumlem1  24552  dvfsumlem2  24553  ply1divex  24659  fta1glem1  24688  dgrcolem1  24792  dgrcolem2  24793  vieta1lem1  24828  aaliou3lem2  24861  aaliou3lem8  24863  dvtaylp  24887  dvntaylp  24888  taylthlem1  24890  taylthlem2  24891  abelthlem1  24948  abelthlem2  24949  abelthlem6  24953  abelthlem7  24955  logdivlti  25130  advlog  25164  advlogexp  25165  logtayl  25170  cxpmul2  25199  dvcxp1  25248  dvcxp2  25249  dvcncxp1  25251  dvcnsqrt  25252  loglesqrt  25266  relogbdiv  25284  ang180lem4  25317  ang180lem5  25318  isosctrlem2  25324  isosctrlem3  25325  affineequiv  25328  affineequiv2  25329  affineequiv3  25330  angpieqvdlem  25333  chordthmlem2  25338  chordthmlem3  25339  chordthmlem5  25341  dcubic2  25349  dcubic  25351  quart1lem  25360  quart1  25361  quart  25366  asinlem  25373  asinlem3  25376  atansopn  25437  dvatan  25440  leibpi  25448  birthdaylem2  25458  efrlim  25475  cxplim  25477  divsqrtsumlem  25485  logdifbnd  25499  emcllem2  25502  emcllem3  25503  emcllem5  25505  zetacvg  25520  lgamgulmlem2  25535  lgamgulmlem3  25536  lgamgulmlem4  25537  lgamgulmlem5  25538  lgamgulmlem6  25539  lgamgulm2  25541  lgamcvg2  25560  gamcvg  25561  gamcvg2lem  25564  lgam1  25569  gamfac  25572  wilthlem2  25574  wilthimp  25577  ftalem5  25582  basellem3  25588  basellem5  25590  basellem8  25593  basellem9  25594  sqff1o  25687  muinv  25698  logfaclbnd  25726  logfacrlim  25728  logexprlim  25729  perfectlem2  25734  dchr1cl  25755  dchrinvcl  25757  dchrfi  25759  dchr1  25761  dchrsum2  25772  bcmono  25781  bcp1ctr  25783  bclbnd  25784  bposlem9  25796  gausslemma2dlem1a  25869  gausslemma2dlem5  25875  lgseisenlem4  25882  lgsquadlem1  25884  m1lgs  25892  2lgslem3a  25900  2lgslem3b  25901  2lgslem3c  25902  2lgslem3d  25903  2lgslem3d1  25907  2lgsoddprmlem1  25912  2sqlem8  25930  2sq2  25937  addsqn2reu  25945  addsqrexnreu  25946  addsqnreup  25947  addsq2nreurex  25948  chtppilim  25979  rpvmasumlem  25991  dchrisumlem1  25993  dchrisum0re  26017  dchrisum0lem2a  26021  mudivsum  26034  mulogsumlem  26035  mulogsum  26036  2vmadivsumlem  26044  selberg4lem1  26064  pntrsumo1  26069  selberg34r  26075  pntrlog2bndlem2  26082  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  pntibndlem2  26095  pntlemg  26102  pntlemr  26106  pntlemf  26109  pntlemk  26110  pntlemo  26111  pntlem3  26113  ostth2lem2  26138  ttgcontlem1  26599  cusgrsize2inds  27163  wlklenvclwlk  27364  wlklenvclwlkOLD  27365  pthdadjvtx  27439  crctcshwlkn0lem1  27516  crctcshwlkn0lem4  27519  crctcshwlkn0lem5  27520  wlklnwwlkln2lem  27588  wlknwwlksnbij  27594  wwlksnred  27598  wwlksnext  27599  wwlksnextbi  27600  wwlksnredwwlkn  27601  wwlksnextwrd  27603  wwlksnextinj  27605  wwlksnextproplem2  27617  wwlksnextproplem3  27618  clwwlkccatlem  27695  clwlkclwwlklem2a1  27698  clwlkclwwlklem2a4  27703  clwlkclwwlklem2a  27704  clwlkclwwlklem2  27706  clwlkclwwlklem3  27707  clwlkclwwlk  27708  clwwisshclwwslemlem  27719  clwwisshclwws  27721  clwwlkel  27753  clwwlkf  27754  clwwlkwwlksb  27761  clwwlkext2edg  27763  wwlksext2clwwlk  27764  clwwlknonex2lem1  27814  clwwlknonex2lem2  27815  eucrct2eupth  27952  numclwwlk1lem2foalem  28058  numclwwlk1lem2fo  28065  numclwlk2lem2f  28084  numclwlk2lem2f1o  28086  numclwwlk6  28097  smcnlem  28402  fzm1ne1  30439  bcm1n  30445  fzom1ne1  30451  ltesubnnd  30466  wrdt2ind  30555  omndmul2  30641  psgnfzto1stlem  30670  cycpmco2lem3  30698  cycpmco2lem4  30699  cycpmco2lem5  30700  cycpmco2lem6  30701  cycpmco2lem7  30702  cycpmco2  30703  archirngz  30746  archiabllem1a  30748  archiabllem2c  30752  freshmansdream  30787  ccfldextdgrr  30957  1smat1  30969  madjusmdetlem2  30993  madjusmdetlem4  30995  dya2icoseg  31435  iwrdsplit  31545  fibp1  31559  ballotlemfp1  31649  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemic  31664  ballotlem1c  31665  ballotlemsgt1  31668  ballotlemsdom  31669  ballotlemsel1i  31670  ballotlemsi  31672  ballotlemsima  31673  ballotlem1ri  31692  sgn0bi  31705  signstfvn  31739  signsvtn0  31740  signstfveq0  31747  signsvfn  31752  signsvtn  31754  signshf  31758  hashreprin  31791  circlemeth  31811  logdivsqrle  31821  revpfxsfxrev  32260  revwlk  32269  swrdwlk  32271  subfacp1lem1  32324  subfacp1lem5  32329  cvxpconn  32387  sinccvglem  32813  divcnvlin  32862  bcm1nt  32867  bcprod  32868  bccolsum  32869  iprodgam  32872  faclimlem1  32873  faclimlem2  32874  faclimlem3  32875  faclim  32876  iprodfac  32877  faclim2  32878  fwddifnp1  33524  dnizphlfeqhlf  33713  dnibndlem3  33717  dnibndlem13  33727  unblimceq0  33744  knoppndvlem6  33754  knoppndvlem9  33757  knoppndvlem14  33762  knoppndvlem15  33763  knoppndvlem16  33764  knoppndvlem17  33765  bj-bary1lem1  34481  poimirlem25  34799  poimirlem26  34800  poimirlem32  34806  opnmbllem0  34810  itg2addnclem2  34826  dvasin  34860  dvacos  34861  areacirclem1  34864  areacirclem4  34867  areacirc  34869  bfp  34985  nnadd1com  39040  nnaddcom  39041  nnadddir  39043  nnmul1com  39044  nnmulcom  39045  fltnltalem  39154  fltnlta  39155  3cubeslem1  39161  3cubeslem2  39162  3cubeslem4  39166  pell1qrge1  39347  rmspecfund  39386  acongeq  39460  jm2.18  39465  jm2.19lem3  39468  jm2.25  39476  jm2.16nn0  39481  jm3.1lem1  39494  jm3.1lem2  39495  itgpowd  39701  areaquad  39703  relexpmulnn  39934  relexpaddss  39943  cvgdvgrat  40525  radcnvrat  40526  hashnzfzclim  40534  ofdivrec  40538  expgrowthi  40545  bccm1k  40554  dvradcnv2  40559  binomcxplemwb  40560  binomcxplemnn0  40561  binomcxplemrat  40562  binomcxplemfrat  40563  binomcxplemdvbinom  40565  binomcxplemnotnn0  40568  refsum2cnlem1  41174  fzisoeu  41447  fperiodmullem  41450  fzdifsuc2  41457  xralrple2  41502  nnsplit  41506  infleinflem2  41519  fmul01lt1lem2  41746  fprodcn  41761  clim1fr1  41762  isumneg  41763  climneg  41771  sumnnodd  41791  reclimc  41814  coseq0  42025  coskpi2  42027  cosknegpi  42030  fprodcncf  42064  fprodsubrecnncnvlem  42071  fprodaddrecnncnvlem  42073  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvnxpaek  42107  dvnmul  42108  dvmptfprod  42110  dvnprodlem3  42113  itgsinexp  42120  itgiccshift  42145  itgperiod  42146  itgsbtaddcnst  42147  stoweidlem1  42167  stoweidlem7  42173  stoweidlem10  42176  stoweidlem11  42177  stoweidlem14  42180  stoweidlem17  42183  stoweidlem34  42200  stoweidlem42  42208  wallispilem3  42233  wallispilem5  42235  wallispi  42236  wallispi2lem1  42237  wallispi2lem2  42238  wallispi2  42239  stirlinglem1  42240  stirlinglem3  42242  stirlinglem4  42243  stirlinglem5  42244  stirlinglem6  42245  stirlinglem7  42246  stirlinglem8  42247  stirlinglem10  42249  stirlinglem11  42250  stirlinglem12  42251  stirlinglem13  42252  stirlinglem15  42254  dirkertrigeqlem2  42265  dirkertrigeqlem3  42266  dirkertrigeq  42267  dirkercncflem1  42269  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem11  42284  fourierdlem15  42288  fourierdlem26  42299  fourierdlem36  42309  fourierdlem40  42313  fourierdlem41  42314  fourierdlem42  42315  fourierdlem48  42320  fourierdlem49  42321  fourierdlem56  42328  fourierdlem58  42330  fourierdlem59  42331  fourierdlem62  42334  fourierdlem64  42336  fourierdlem65  42337  fourierdlem78  42350  fourierdlem79  42351  sqwvfoura  42394  fourierswlem  42396  fouriersw  42397  etransclem23  42423  etransclem24  42424  etransclem28  42428  etransclem35  42435  etransclem38  42438  nnfoctbdjlem  42618  smfmullem1  42947  sigaradd  43004  deccarry  43392  fargshiftf1  43448  fargshiftfo  43449  fmtnof1  43544  sqrtpwpw2p  43547  fmtnorec2lem  43551  fmtnorec4  43558  fmtnoprmfac1lem  43573  fmtnoprmfac1  43574  fmtnoprmfac2  43576  2pwp1prm  43598  mod42tp1mod8  43614  sfprmdvdsmersenne  43615  lighneallem3  43619  lighneallem4  43622  onego  43658  zofldiv2ALTV  43674  oexpnegALTV  43689  opoeALTV  43695  opeoALTV  43696  epee  43717  perfectALTVlem1  43733  fppr2odd  43743  fpprwppr  43751  0nodd  43924  2nodd  43926  nnsgrpnmnd  43932  1neven  44101  altgsumbc  44298  pw2m1lepw2m1  44473  m1modmmod  44479  zofldiv2  44489  nnpw2pmod  44541  blen1b  44546  blennn0em1  44549  dignn0flhalflem1  44573  dignn0flhalflem2  44574  nn0sumshdiglemB  44578  nn0sumshdiglem1  44579  nn0sumshdiglem2  44580  affineid  44589  1subrec1sub  44590  eenglngeehlnmlem1  44622  eenglngeehlnmlem2  44623  rrx2vlinest  44626
  Copyright terms: Public domain W3C validator