Axiom ax-1cn 10913

Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by Theorem ax1cn 10889. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-1cn	⊢ 1 ∈ ℂ

Detailed syntax breakdown of Axiom ax-1cn

Step	Hyp	Ref	Expression
1		c1 10856	. 2 class 1
2		cc 10853	. 2 class ℂ
3	1, 2	wcel 2109	1 wff 1 ∈ ℂ

This axiom is referenced by:  0cn  10951  1cnd  10954  1ex  10955  mulid1  10957  mulid2  10958  1re  10959  0re  10961  muladd11  11128  peano2cn  11130  mul02lem2  11135  addid1  11138  cnegex2  11140  peano2cnm  11270  0reALT  11301  ine0  11393  mulm1  11399  0lt1  11480  ixi  11587  muleqadd  11602  reccl  11623  recne0  11629  recid  11630  recid2  11631  div1  11647  1div1e1  11648  diveq1  11649  recdiv  11664  divdiv1  11669  divdiv2  11670  recdiv2  11671  conjmul  11675  eqneg  11678  div2neg  11681  recp1lt1  11856  recreclt  11857  recgt0ii  11864  inelr  11946  ofnegsub  11954  peano5nni  11959  nnsscn  11961  nn1m1nn  11977  nn1suc  11978  nnaddcl  11979  nnmulcl  11980  nnne0  11990  nnsub  12000  1m1e0  12028  2cn  12031  3cn  12037  4cn  12041  5cn  12044  6cn  12047  7cn  12050  8cn  12053  9cn  12056  neg1cn  12070  neg1ne0  12072  negneg1e1  12074  1pneg1e0  12075  1m0e1  12077  0p1e1  12078  1p0e1  12080  2m1e1  12082  3m1e2  12084  4m1e3  12085  5m1e4  12086  6m1e5  12087  7m1e6  12088  8m1e7  12089  9m1e8  12090  2p2e4  12091  1p2e3  12099  1p2e3ALT  12100  3p2e5  12107  3p3e6  12108  4p2e6  12109  4p3e7  12110  4p4e8  12111  5p2e7  12112  5p3e8  12113  5p4e9  12114  6p2e8  12115  6p3e9  12116  7p2e9  12117  1t1e1  12118  3t3e9  12123  neg1mulneg1e1  12169  1mhlfehlf  12175  8th4div3  12176  halfpm6th  12177  addltmul  12192  elnn0nn  12258  elz2  12320  zlem1lt  12355  zltlem1  12356  nnaddm1cl  12360  zextlt  12377  zeo  12389  peano5uzi  12392  numsuc  12433  numltc  12445  numsucc  12459  numaddc  12467  6p5lem  12489  5p5e10  12490  6p4e10  12491  7p3e10  12494  8p2e10  12499  10m1e9  12515  4t3lem  12516  7t4e28  12530  9t11e99  12549  decbin2  12560  halfthird  12562  5recm6rec  12563  uzp1  12601  peano2uzr  12625  uzaddcl  12626  rebtwnz  12669  qbtwnre  12915  iccf1o  13210  fz01en  13266  fztp  13294  fzsuc2  13296  fztpval  13300  fseq1m1p1  13313  elfzp1b  13315  fz0to4untppr  13341  predfz  13363  fzoss2  13396  fzval3  13437  fzosplitsnm1  13443  fzo1to4tp  13456  fldiv4p1lem1div2  13536  ceim1l  13548  fldiv  13561  uzrdgxfr  13668  fzen2  13670  nn0ennn  13680  seqm1  13721  seqshft2  13730  monoord2  13735  sermono  13736  seqf1olem1  13743  seqf1olem2  13744  seqz  13752  ser1const  13760  expcl  13781  m1expcl2  13785  expclzlem  13787  expm1t  13792  1exp  13793  mulexpz  13804  expadd  13806  expaddz  13808  expmul  13809  expubnd  13876  sqrecii  13881  neg1sqe1  13894  irec  13899  i4  13902  binom21  13915  sq01  13921  crreczi  13924  bernneq  13925  bernneq2  13926  nn0opthlem1  13963  facndiv  13983  faclbnd4lem1  13988  faclbnd6  13994  bcnp1n  14009  bcm1k  14010  bcp1nk  14012  bcn2  14014  bcp1m1  14015  bcpasc  14016  hashgadd  14073  hashfz  14123  hashfzo  14125  hashxplem  14129  hashbclem  14145  hashf1  14152  seqcoll  14159  swrds1  14360  swrdlsw  14361  wrdind  14416  wrd2ind  14417  swrds2  14634  relexpaddg  14745  rei  14848  imi  14849  recan  15029  iserex  15349  isercoll2  15361  serf0  15373  iseraltlem2  15375  iseraltlem3  15376  iseralt  15377  sumrblem  15404  fsumm1  15444  fsump1  15449  telfsumo  15495  fsumparts  15499  hashiun  15515  binomlem  15522  binom  15523  binom1p  15524  binom11  15525  binom1dif  15526  bcxmas  15528  isumsplit  15533  isum1p  15534  climcndslem1  15542  supcvg  15549  harmonic  15552  arisum  15553  arisum2  15554  trireciplem  15555  geoserg  15559  geolim  15563  geolim2  15564  georeclim  15565  geo2sum  15566  geo2sum2  15567  geoisum1c  15573  0.999...  15574  geoihalfsum  15575  cvgrat  15576  mertenslem1  15577  mertenslem2  15578  mertens  15579  prodf1  15584  prodfclim1  15586  prodrblem  15620  fprodcvg  15621  prodmolem2a  15625  zprod  15628  fprodntriv  15633  prodss  15638  fprodss  15639  fprodsplit  15657  fprodn0f  15682  risefaccl  15706  fallfaccl  15707  risefacfac  15726  binomfallfac  15732  bpolycl  15743  bpolysum  15744  bpolydiflem  15745  fsumkthpow  15747  bpoly2  15748  bpoly3  15749  bpoly4  15750  fsumcube  15751  esum  15771  ege2le3  15780  efsub  15790  efexp  15791  efzval  15792  eftlub  15799  effsumlt  15801  ef4p  15803  tanval3  15824  efi4p  15827  tan0  15841  efival  15842  tanadd  15857  cos2t  15868  cos2tsin  15869  ef01bndlem  15874  cos1bnd  15877  cos2bnd  15878  demoivreALT  15891  eirrlem  15894  rpnnen2lem3  15906  rpnnen2lem11  15914  ruclem12  15931  3dvds  16021  3dvdsdec  16022  3dvds2dec  16023  odd2np1lem  16030  odd2np1  16031  opoe  16053  omoe  16054  opeo  16055  omeo  16056  n2dvdsm1  16059  m1exp1  16066  flodddiv4  16103  bitsfzo  16123  gcdmultipleOLD  16241  sqgcd  16251  nn0seqcvgd  16256  prmind2  16371  hashdvds  16457  phiprmpw  16458  phiprm  16459  eulerthlem2  16464  iserodd  16517  sumhash  16578  fldivp1  16579  prmpwdvds  16586  pockthlem  16587  pockthi  16589  prmreclem4  16601  prmreclem6  16603  4sqlem11  16637  4sqlem19  16645  vdwapun  16656  vdwapid1  16657  vdwlem3  16665  vdwlem5  16667  vdwlem6  16668  vdwlem8  16670  vdwlem9  16671  vdwnnlem2  16678  ramub1lem1  16708  ramub1lem2  16709  ramcl  16711  prmo1  16719  dec5nprm  16748  decexp2  16757  prmlem0  16788  43prm  16804  83prm  16805  139prm  16806  163prm  16807  317prm  16808  631prm  16809  1259lem2  16814  1259lem3  16815  1259lem4  16816  1259lem5  16817  1259prm  16818  2503lem1  16819  2503lem2  16820  2503lem3  16821  2503prm  16822  4001lem1  16823  4001lem2  16824  4001lem3  16825  4001lem4  16826  4001prm  16827  gsumsgrpccat  18459  gsumccatOLD  18460  mulgnndir  18713  mulgneg2  18718  m1expaddsub  19087  sylow1lem1  19184  sylow2a  19205  efgsval2  19320  efgsrel  19321  efgsres  19325  cnfld1  20604  zsssubrg  20637  cnmgpid  20641  zringcyg  20672  mulgrhm2  20681  cnmsgnsubg  20763  cnmsgnbas  20764  cnmsgngrp  20765  psgninv  20768  evpmodpmf1o  20782  blcvx  23942  iihalf2  24077  icopnfcnv  24086  iccpnfhmeo  24089  xrhmeo  24090  icccvx  24094  lebnumii  24110  reparphti  24141  pcoass  24168  pcorevlem  24170  pcorev2  24172  pi1xfrcnv  24201  cnstrcvs  24285  cncvs  24289  ncvsm1  24299  pjthlem1  24582  divcncf  24592  ovolunlem1a  24641  ovolunlem1  24642  ovolicc2lem4  24665  uniioombllem3  24730  uniioombllem4  24731  dyadovol  24738  vitalilem4  24756  mbf0  24779  iblcnlem1  24933  itgcnlem  24935  dvid  25063  dvexp  25098  dvexp2  25099  dvexp3  25123  dveflem  25124  dvlipcn  25139  dvcvx  25165  dvfsumle  25166  dvfsumlem1  25171  degltp1le  25219  ply1divex  25282  fta1glem1  25311  plyaddlem1  25355  plymullem1  25356  coeidp  25405  dgrid  25406  dvply1  25425  dvply2g  25426  plyremlem  25445  fta1lem  25448  vieta1lem1  25451  vieta1lem2  25452  qaa  25464  iaa  25466  aalioulem3  25475  geolim3  25480  aaliou3lem2  25484  aaliou3lem7  25490  taylply2  25508  dvradcnv  25561  pserdvlem2  25568  pserdv2  25570  abelthlem1  25571  abelthlem2  25572  abelthlem6  25576  abelthlem7  25578  abelth  25581  reeff1olem  25586  reeff1o  25587  efcvx  25589  sinhalfpilem  25601  eulerid  25612  cos2pi  25614  sincosq3sgn  25638  sincosq4sgn  25639  tangtx  25643  sincos4thpi  25651  sincos6thpi  25653  pigt3  25655  pige3ALT  25657  abssinper  25658  coskpi  25660  coseq1  25662  efeq1  25665  tanregt0  25676  logneg2  25751  logdivlti  25756  logcnlem4  25781  dvlog2lem  25788  dvlog2  25789  advlog  25790  advlogexp  25791  logtayl  25796  logtayl2  25798  logccv  25799  cxpval  25800  1cxp  25808  cxpcl  25810  cxpp1  25816  cxpsqrt  25839  dvsqrt  25876  dvcnsqrt  25878  sqrtcn  25884  cxpaddlelem  25885  root1id  25888  root1cj  25890  logrec  25894  logb1  25900  logbmpt  25919  ang180lem1  25940  ang180lem2  25941  ang180lem3  25942  isosctrlem1  25949  isosctrlem2  25950  1cubrlem  25972  1cubr  25973  mcubic  25978  binom4  25981  dquartlem1  25982  quartlem1  25988  asinlem  25999  asinlem2  26000  asinlem3a  26001  asinlem3  26002  asinf  26003  atandm2  26008  atandm4  26010  atanf  26011  asinneg  26017  efiasin  26019  sinasin  26020  asinsin  26023  asin1  26025  acos1  26026  reasinsin  26027  asinbnd  26030  cosasin  26035  atanneg  26038  atancj  26041  efiatan  26043  atanlogaddlem  26044  atanlogadd  26045  atanlogsublem  26046  atanlogsub  26047  efiatan2  26048  2efiatan  26049  tanatan  26050  cosatan  26052  cosatanne0  26053  atantan  26054  atanbndlem  26056  bndatandm  26060  atans2  26062  dvatan  26066  atantayl  26068  atantayl2  26069  atantayl3  26070  leibpilem2  26072  leibpi  26073  log2cnv  26075  log2tlbnd  26076  log2ublem3  26079  log2ub  26080  birthdaylem2  26083  birthday  26085  efrlim  26100  dfef2  26101  cvxcl  26115  scvxcvx  26116  emcllem2  26127  emcllem4  26129  emcllem7  26132  harmonicbnd4  26141  fsumharmonic  26142  zetacvg  26145  lgamcvg2  26185  lgam1  26194  gam1  26195  wilthlem1  26198  wilthlem2  26199  wilthlem3  26200  basellem2  26212  basellem5  26215  basellem6  26216  basellem7  26217  basellem8  26218  basellem9  26219  0sgm  26274  mule1  26278  ppiprm  26281  ppinprm  26282  chtprm  26283  chtnprm  26284  chpp1  26285  mumullem2  26310  1sgmprm  26328  1sgm2ppw  26329  ppiub  26333  chtublem  26340  chtub  26341  logfaclbnd  26351  logfacbnd3  26352  logfacrlim  26353  logexprlim  26354  mersenne  26356  perfect1  26357  perfectlem1  26358  perfectlem2  26359  perfect  26360  dchrelbasd  26368  dchrmulid2  26381  dchrfi  26384  dchrsum2  26397  sumdchr2  26399  bcp1ctr  26408  bposlem8  26420  zabsle1  26425  lgslem1  26426  lgslem2  26427  lgsfcl2  26432  lgsvalmod  26445  lgsneg  26450  lgsdilem  26453  lgsdir2lem1  26454  lgsdir2lem2  26455  lgsdir2lem3  26456  lgsdir2lem5  26458  lgsdir2  26459  lgsdir  26461  lgsdi  26463  lgsne0  26464  lgseisenlem1  26504  lgseisenlem2  26505  lgseisen  26508  lgsquadlem1  26509  lgsquadlem2  26510  lgsquad2lem1  26513  lgsquad2  26515  m1lgs  26517  2lgslem3c  26527  2lgsoddprmlem3c  26541  2lgsoddprmlem3d  26542  2sqlem10  26557  2sqlem11  26558  2sqblem  26560  addsqn2reu  26570  addsqrexnreu  26571  addsqnreup  26572  chtppilimlem2  26603  chebbnd2  26606  chto1lb  26607  rplogsumlem1  26613  rpvmasumlem  26616  dchrmusumlema  26622  dchrmusum2  26623  dchrisum0flblem1  26637  rpvmasum2  26641  mudivsum  26659  mulogsum  26661  vmalogdivsum2  26667  selberg2lem  26679  logdivbnd  26685  pntrmax  26693  pntrsumo1  26694  pntrsumbnd2  26696  pntrlog2bndlem5  26710  pntpbnd1a  26714  pntpbnd2  26716  pntibndlem2  26720  pntlemd  26723  pntlemc  26724  pntlemr  26731  brbtwn2  27254  colinearalglem4  27258  ax5seglem1  27277  ax5seglem2  27278  ax5seglem3  27280  ax5seglem5  27282  ax5seglem7  27284  ax5seglem9  27286  axbtwnid  27288  axpaschlem  27289  axlowdimlem13  27303  axlowdimlem14  27304  axlowdimlem16  27306  axeuclidlem  27311  axcontlem2  27314  axcontlem4  27316  axcontlem7  27319  axcontlem8  27320  crctcshwlkn0lem6  28159  clwwlkf1  28392  clwwlknonex2lem2  28451  ex-fl  28790  ex-ind-dvds  28804  vc2OLD  28909  vc0  28915  vcm  28917  nvm1  29006  nvmtri  29012  nvge0  29014  ipval2lem3  29046  ipidsq  29051  lnoadd  29099  ip1ilem  29167  ip1i  29168  ip2i  29169  ipdirilem  29170  ipasslem1  29172  ipasslem2  29173  ipasslem10  29180  minvecolem2  29216  hvsubid  29367  hv2times  29402  hisubcomi  29445  normlem9  29459  normlem7tALT  29460  norm-ii-i  29478  normsubi  29482  hhssnv  29605  pjhthlem1  29732  h1de2bi  29895  homulid2  30141  ho2times  30160  lnop0  30307  lnopaddi  30312  lnophmlem2  30358  lnfn0i  30383  lnfnaddi  30384  hst1h  30568  sto2i  30578  stadd3i  30589  addltmulALT  30787  dpmul4  31167  psgnid  31343  cnmsgn0g  31392  altgnsg  31395  isarchi3  31420  archirngz  31422  ccfldextdgrr  31721  lmatfvlem  31744  qqhval2lem  31910  dya2ub  32216  omssubadd  32246  eulerpartlemgs2  32326  fib5  32351  fib6  32352  ballotlem2  32434  sgnneg  32486  signswch  32519  signlem0  32545  itgexpif  32565  reprlt  32578  breprexp  32592  breprexpnat  32593  hgt750lem2  32611  subfacp1lem5  33125  subfacp1lem6  33126  subfacval2  33128  subfaclim  33129  subfacval3  33130  cvxsconn  33184  resconn  33187  cvmliftlem7  33232  cvmliftlem10  33235  problem4  33605  sinccvglem  33609  sqdivzi  33672  faclimlem1  33688  dnibndlem5  34641  dnibndlem10  34646  ltflcei  35744  sin2h  35746  cos2h  35747  tan2h  35748  poimirlem13  35769  poimirlem16  35772  poimirlem17  35773  poimirlem19  35775  poimirlem20  35776  poimirlem31  35787  mblfinlem2  35794  mblfinlem3  35795  dvtan  35806  itg2addnclem3  35809  dvasin  35840  dvacos  35841  areacirc  35849  fdc  35882  mettrifi  35894  heiborlem4  35951  heiborlem6  35953  60gcd7e1  39993  lcmineqlem1  40017  lcmineqlem8  40024  lcmineqlem9  40025  lcmineqlem10  40026  lcmineqlem12  40028  3exp7  40041  3lexlogpow5ineq1  40042  3lexlogpow5ineq5  40048  aks4d1p1p4  40059  aks4d1p1p7  40062  aks4d1p1  40064  facp2  40079  fac2xp3  40140  2xp3dxp2ge1d  40142  factwoffsmonot  40143  sn-1ne2  40275  sqdeccom12  40297  235t711  40299  expgcd  40314  re1m1e0m0  40360  ipiiie0  40399  sn-0tie0  40401  fltnltalem  40479  3cubeslem3l  40488  3cubeslem3r  40489  eldioph2lem1  40562  lzenom  40572  irrapxlem1  40624  rmspecsqrtnq  40708  rmxm1  40736  rmym1  40737  2nn0ind  40747  jm2.24nn  40761  jm2.17a  40762  jm2.17b  40763  jm2.17c  40764  jm2.24  40765  acongeq  40785  jm2.18  40790  jm2.27c  40809  jm3.1lem2  40820  rngunsnply  40978  flcidc  40979  inductionexd  41718  unitadd  41759  hashnzfzclim  41893  ofdivrec  41897  lhe4.4ex1a  41900  expgrowth  41906  dvradcnv2  41918  binomcxplemrat  41921  binomcxplemnotnn0  41927  isosctrlem1ALT  42507  monoord2xrv  42978  dvsinax  43408  dvnprodlem3  43443  itgsin0pilem1  43445  itgsbtaddcnst  43477  stoweidlem13  43508  stoweidlem26  43521  stoweidlem34  43529  stoweidlem38  43533  wallispilem2  43561  wallispilem4  43563  wallispi2lem1  43566  stirlinglem1  43569  stirlinglem5  43573  stirlinglem10  43578  dirkerper  43591  dirkertrigeqlem1  43593  dirkertrigeqlem3  43595  dirkertrigeq  43596  dirkercncflem4  43601  fourierdlem24  43626  sqwvfoura  43723  sqwvfourb  43724  fourierswlem  43725  1t10e1p1e11  44754  fmtnorec3  44952  fmtno5lem4  44960  fmtno5  44961  257prm  44965  fmtno4nprmfac193  44978  m3prm  44996  139prmALT  45000  127prm  45003  m7prm  45004  lighneallem3  45011  proththd  45018  3exp4mod41  45020  41prothprmlem2  45022  perfectALTVlem2  45126  perfectALTV  45127  11t31e341  45136  evengpop3  45202  nnsum4primeseven  45204  nnsum4primesevenALTV  45205  bgoldbtbndlem1  45209  0nodd  45316  altgsumbcALT  45641  exple2lt6  45652  nn0sumshdiglemB  45918  ackval3  45981  ackval3012  45990  line2ylem  46049  onetansqsecsq  46415  cotsqcscsq  46416  5m4e1  46453