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

Theorem 1cnd 10630
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 10589 . 2 1 ∈ ℂ
21a1i 11 1 (𝜑 → 1 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  cc 10529  1c1 10532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-1cn 10589
This theorem is referenced by:  adddirp1d  10661  1p1times  10805  addcom  10820  addcomd  10836  muladd11r  10847  pncan1  11058  npcan1  11059  muls1d  11094  mulsubfacd  11095  recrec  11331  rec11  11332  rec11r  11333  rereccl  11352  subrec  11463  nn1m1nn  11652  add1p1  11882  sub1m1  11883  cnm2m1cnm3  11884  xp1d2m1eqxm1d2  11885  div4p1lem1div2  11886  nn0n0n1ge2  11956  zneo  12059  rpnnen1lem5  12374  lincmb01cmp  12875  iccf1o  12876  xov1plusxeqvd  12878  zpnn0elfzo1  13105  ubmelm1fzo  13127  fzosplitpr  13140  fzosplitprm1  13141  fzoshftral  13148  fladdz  13189  2tnp1ge0ge0  13193  ltdifltdiv  13198  dfceil2  13203  negmod  13278  modnegd  13288  addmodlteq  13308  binom2sub1  13576  binom3  13579  zesq  13581  sqoddm1div8  13598  bcm1k  13669  bcp1n  13670  bcp1m1  13674  bcpasc  13675  bcn2m1  13678  hashfz  13782  hashfzo  13784  hashfzp1  13786  hashf1lem2  13808  hashf1  13809  hashdifsnp1  13848  lswccatn0lsw  13939  ccatws1lenp1b  13969  revccat  14122  repswrevw  14143  cshwidxm1  14163  cshwidxn  14165  cshweqrep  14177  cshimadifsn0  14186  swrds2m  14297  swrd2lsw  14308  relexpaddnn  14404  absexpz  14659  reccn2  14947  rlimno1  15004  isercolllem1  15015  isercoll2  15019  iseraltlem2  15033  iseraltlem3  15034  hashiun  15171  hash2iun1dif1  15173  binomlem  15178  bcxmas  15184  incexc  15186  incexc2  15187  climcndslem1  15198  arisum  15209  arisum2  15210  trireciplem  15211  pwdif  15217  pwm1geoser  15218  pwm1geoserOLD  15219  geolim2  15221  georeclim  15222  mertenslem1  15234  prodfrec  15245  ntrivcvg  15247  ntrivcvgtail  15250  prodrblem  15277  prodmolem2a  15282  fprodntriv  15290  prod1  15292  fprodser  15297  fprodcl  15300  fprodm1  15315  fprodp1  15317  fprodclf  15340  risefacval2  15358  fallfacval2  15359  risefacp1  15377  fallfacp1  15378  risefacfac  15383  fallfacfwd  15384  binomfallfaclem2  15388  fallfacval4  15391  bpolydiflem  15402  ef0lem  15426  tanaddlem  15513  tanadd  15514  cos01bnd  15533  oddm1even  15686  oddp1even  15687  oexpneg  15688  ltoddhalfle  15704  halfleoddlt  15705  nn0ob  15729  pwp1fsum  15736  flodddiv4  15758  bitsp1o  15776  bitsf1  15789  sadcp1  15798  qredeu  15996  prmdiv  16116  prmdiveq  16117  vfermltlALT  16133  pc2dvds  16209  4sqlem11  16285  4sqlem12  16286  vdwapun  16304  vdwlem3  16313  vdwlem6  16316  vdwlem9  16319  ramub1lem2  16357  prmop1  16368  prmdvdsprmo  16372  prmgaplem8  16388  cshwshashnsame  16431  gsumsgrpccat  17998  gsumccatOLD  17999  psgnunilem5  18616  psgnunilem2  18617  sylow1lem1  18717  efgredlemc  18865  odadd2  18963  ablsimpgfindlem1  19223  srgbinomlem3  19286  srgbinomlem4  19287  cncrng  20560  gzrngunit  20605  zringunit  20629  prmirredlem  20634  cayhamlem1  21468  expcn  23474  iirevcn  23528  iihalf2cn  23532  icchmeo  23539  icopnfcnv  23540  icopnfhmeo  23541  evth  23557  pcoass  23622  pjthlem1  24034  ovolunlem1a  24091  ovolunlem1  24092  opnmbllem  24196  mbfi1fseqlem6  24315  bddibl  24434  dvnadd  24520  dvmptid  24548  dvmptdiv  24565  dvcnvlem  24567  dveflem  24570  dvef  24571  dvsincos  24572  dvlipcn  24585  dvivthlem1  24599  lhop2  24606  dvcvx  24611  dvfsumle  24612  dvfsumabs  24614  dvfsumlem1  24617  dvfsumlem2  24618  ply1divex  24724  fta1glem1  24753  dgrcolem1  24857  dgrcolem2  24858  vieta1lem1  24893  aaliou3lem2  24926  aaliou3lem8  24928  dvtaylp  24952  dvntaylp  24953  taylthlem1  24955  taylthlem2  24956  abelthlem1  25013  abelthlem2  25014  abelthlem6  25018  abelthlem7  25020  logdivlti  25197  advlog  25231  advlogexp  25232  logtayl  25237  cxpmul2  25266  dvcxp1  25315  dvcxp2  25316  dvcncxp1  25318  dvcnsqrt  25319  loglesqrt  25333  relogbdiv  25351  ang180lem4  25384  ang180lem5  25385  isosctrlem2  25391  isosctrlem3  25392  affineequiv  25395  affineequiv2  25396  affineequiv3  25397  angpieqvdlem  25400  chordthmlem2  25405  chordthmlem3  25406  chordthmlem5  25408  dcubic2  25416  dcubic  25418  quart1lem  25427  quart1  25428  quart  25433  asinlem  25440  asinlem3  25443  atansopn  25504  dvatan  25507  leibpi  25514  birthdaylem2  25524  efrlim  25541  cxplim  25543  divsqrtsumlem  25551  logdifbnd  25565  emcllem2  25568  emcllem3  25569  emcllem5  25571  zetacvg  25586  lgamgulmlem2  25601  lgamgulmlem3  25602  lgamgulmlem4  25603  lgamgulmlem5  25604  lgamgulmlem6  25605  lgamgulm2  25607  lgamcvg2  25626  gamcvg  25627  gamcvg2lem  25630  lgam1  25635  gamfac  25638  wilthlem2  25640  wilthimp  25643  ftalem5  25648  basellem3  25654  basellem5  25656  basellem8  25659  basellem9  25660  sqff1o  25753  muinv  25764  logfaclbnd  25792  logfacrlim  25794  logexprlim  25795  perfectlem2  25800  dchr1cl  25821  dchrinvcl  25823  dchrfi  25825  dchr1  25827  dchrsum2  25838  bcmono  25847  bcp1ctr  25849  bclbnd  25850  bposlem9  25862  gausslemma2dlem1a  25935  gausslemma2dlem5  25941  lgseisenlem4  25948  lgsquadlem1  25950  m1lgs  25958  2lgslem3a  25966  2lgslem3b  25967  2lgslem3c  25968  2lgslem3d  25969  2lgslem3d1  25973  2lgsoddprmlem1  25978  2sqlem8  25996  2sq2  26003  addsqn2reu  26011  addsqrexnreu  26012  addsqnreup  26013  addsq2nreurex  26014  chtppilim  26045  rpvmasumlem  26057  dchrisumlem1  26059  dchrisum0re  26083  dchrisum0lem2a  26087  mudivsum  26100  mulogsumlem  26101  mulogsum  26102  2vmadivsumlem  26110  selberg4lem1  26130  pntrsumo1  26135  selberg34r  26141  pntrlog2bndlem2  26148  pntrlog2bndlem4  26150  pntrlog2bndlem5  26151  pntrlog2bndlem6  26153  pntibndlem2  26161  pntlemg  26168  pntlemr  26172  pntlemf  26175  pntlemk  26176  pntlemo  26177  pntlem3  26179  ostth2lem2  26204  ttgcontlem1  26665  cusgrsize2inds  27229  wlklenvclwlk  27430  wlklenvclwlkOLD  27431  pthdadjvtx  27505  crctcshwlkn0lem1  27582  crctcshwlkn0lem4  27585  crctcshwlkn0lem5  27586  wlklnwwlkln2lem  27654  wlknwwlksnbij  27660  wwlksnred  27664  wwlksnext  27665  wwlksnextbi  27666  wwlksnredwwlkn  27667  wwlksnextwrd  27669  wwlksnextinj  27671  wwlksnextproplem2  27683  wwlksnextproplem3  27684  clwwlkccatlem  27761  clwlkclwwlklem2a1  27764  clwlkclwwlklem2a4  27769  clwlkclwwlklem2a  27770  clwlkclwwlklem2  27772  clwlkclwwlklem3  27773  clwlkclwwlk  27774  clwwisshclwwslemlem  27785  clwwisshclwws  27787  clwwlkel  27819  clwwlkf  27820  clwwlkwwlksb  27827  clwwlkext2edg  27829  wwlksext2clwwlk  27830  clwwlknonex2lem1  27880  clwwlknonex2lem2  27881  eucrct2eupth  28018  numclwwlk1lem2foalem  28124  numclwwlk1lem2fo  28131  numclwlk2lem2f  28150  numclwlk2lem2f1o  28152  numclwwlk6  28163  smcnlem  28468  fzm1ne1  30506  bcm1n  30512  fzom1ne1  30518  ltesubnnd  30533  wrdt2ind  30622  omndmul2  30708  psgnfzto1stlem  30737  cycpmco2lem3  30765  cycpmco2lem4  30766  cycpmco2lem5  30767  cycpmco2lem6  30768  cycpmco2lem7  30769  cycpmco2  30770  archirngz  30813  archiabllem1a  30815  archiabllem2c  30819  freshmansdream  30854  ccfldextdgrr  31052  1smat1  31064  madjusmdetlem2  31088  madjusmdetlem4  31090  dya2icoseg  31530  iwrdsplit  31640  fibp1  31654  ballotlemfp1  31744  ballotlemfc0  31745  ballotlemfcc  31746  ballotlemic  31759  ballotlem1c  31760  ballotlemsgt1  31763  ballotlemsdom  31764  ballotlemsel1i  31765  ballotlemsi  31767  ballotlemsima  31768  ballotlem1ri  31787  sgn0bi  31800  signstfvn  31834  signsvtn0  31835  signstfveq0  31842  signsvfn  31847  signsvtn  31849  signshf  31853  hashreprin  31886  circlemeth  31906  logdivsqrle  31916  revpfxsfxrev  32357  revwlk  32366  swrdwlk  32368  subfacp1lem1  32421  subfacp1lem5  32426  cvxpconn  32484  sinccvglem  32910  divcnvlin  32959  bcm1nt  32964  bcprod  32965  bccolsum  32966  iprodgam  32969  faclimlem1  32970  faclimlem2  32971  faclimlem3  32972  faclim  32973  iprodfac  32974  faclim2  32975  fwddifnp1  33621  dnizphlfeqhlf  33810  dnibndlem3  33814  dnibndlem13  33824  unblimceq0  33841  knoppndvlem6  33851  knoppndvlem9  33854  knoppndvlem14  33859  knoppndvlem15  33860  knoppndvlem16  33861  knoppndvlem17  33862  bj-bary1lem1  34586  poimirlem25  34911  poimirlem26  34912  poimirlem32  34918  opnmbllem0  34922  itg2addnclem2  34938  dvasin  34972  dvacos  34973  areacirclem1  34976  areacirclem4  34979  areacirc  34981  bfp  35096  nnadd1com  39153  nnaddcom  39154  nnadddir  39156  nnmul1com  39157  nnmulcom  39158  fltnltalem  39267  fltnlta  39268  3cubeslem1  39274  3cubeslem2  39275  3cubeslem4  39279  pell1qrge1  39460  rmspecfund  39499  acongeq  39573  jm2.18  39578  jm2.19lem3  39581  jm2.25  39589  jm2.16nn0  39594  jm3.1lem1  39607  jm3.1lem2  39608  itgpowd  39814  areaquad  39816  relexpmulnn  40047  relexpaddss  40056  cvgdvgrat  40638  radcnvrat  40639  hashnzfzclim  40647  ofdivrec  40651  expgrowthi  40658  bccm1k  40667  dvradcnv2  40672  binomcxplemwb  40673  binomcxplemnn0  40674  binomcxplemrat  40675  binomcxplemfrat  40676  binomcxplemdvbinom  40678  binomcxplemnotnn0  40681  refsum2cnlem1  41287  fzisoeu  41559  fperiodmullem  41562  fzdifsuc2  41569  xralrple2  41614  nnsplit  41618  infleinflem2  41631  fmul01lt1lem2  41858  fprodcn  41873  clim1fr1  41874  isumneg  41875  climneg  41883  sumnnodd  41903  reclimc  41926  coseq0  42137  coskpi2  42139  cosknegpi  42142  fprodcncf  42176  fprodsubrecnncnvlem  42183  fprodaddrecnncnvlem  42185  ioodvbdlimc1lem2  42209  ioodvbdlimc2lem  42211  dvnxpaek  42219  dvnmul  42220  dvmptfprod  42222  dvnprodlem3  42225  itgsinexp  42232  itgiccshift  42257  itgperiod  42258  itgsbtaddcnst  42259  stoweidlem1  42279  stoweidlem7  42285  stoweidlem10  42288  stoweidlem11  42289  stoweidlem14  42292  stoweidlem17  42295  stoweidlem34  42312  stoweidlem42  42320  wallispilem3  42345  wallispilem5  42347  wallispi  42348  wallispi2lem1  42349  wallispi2lem2  42350  wallispi2  42351  stirlinglem1  42352  stirlinglem3  42354  stirlinglem4  42355  stirlinglem5  42356  stirlinglem6  42357  stirlinglem7  42358  stirlinglem8  42359  stirlinglem10  42361  stirlinglem11  42362  stirlinglem12  42363  stirlinglem13  42364  stirlinglem15  42366  dirkertrigeqlem2  42377  dirkertrigeqlem3  42378  dirkertrigeq  42379  dirkercncflem1  42381  dirkercncflem2  42382  dirkercncflem4  42384  fourierdlem11  42396  fourierdlem15  42400  fourierdlem26  42411  fourierdlem36  42421  fourierdlem40  42425  fourierdlem41  42426  fourierdlem42  42427  fourierdlem48  42432  fourierdlem49  42433  fourierdlem56  42440  fourierdlem58  42442  fourierdlem59  42443  fourierdlem62  42446  fourierdlem64  42448  fourierdlem65  42449  fourierdlem78  42462  fourierdlem79  42463  sqwvfoura  42506  fourierswlem  42508  fouriersw  42509  etransclem23  42535  etransclem24  42536  etransclem28  42540  etransclem35  42547  etransclem38  42550  nnfoctbdjlem  42730  smfmullem1  43059  sigaradd  43116  deccarry  43504  fargshiftf1  43594  fargshiftfo  43595  fmtnof1  43690  sqrtpwpw2p  43693  fmtnorec2lem  43697  fmtnorec4  43704  fmtnoprmfac1lem  43719  fmtnoprmfac1  43720  fmtnoprmfac2  43722  2pwp1prm  43744  mod42tp1mod8  43760  sfprmdvdsmersenne  43761  lighneallem3  43765  lighneallem4  43768  onego  43804  zofldiv2ALTV  43820  oexpnegALTV  43835  opoeALTV  43841  opeoALTV  43842  epee  43863  perfectALTVlem1  43879  fppr2odd  43889  fpprwppr  43897  0nodd  44070  2nodd  44072  nnsgrpnmnd  44078  1neven  44196  altgsumbc  44393  pw2m1lepw2m1  44568  m1modmmod  44574  zofldiv2  44584  nnpw2pmod  44636  blen1b  44641  blennn0em1  44644  dignn0flhalflem1  44668  dignn0flhalflem2  44669  nn0sumshdiglemB  44673  nn0sumshdiglem1  44674  nn0sumshdiglem2  44675  affineid  44684  1subrec1sub  44685  eenglngeehlnmlem1  44717  eenglngeehlnmlem2  44718  rrx2vlinest  44721
  Copyright terms: Public domain W3C validator