Axiom ax-1cn 10938

Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by Theorem ax1cn 10914. (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 10881	. 2 class 1
2		cc 10878	. 2 class ℂ
3	1, 2	wcel 2107	1 wff 1 ∈ ℂ

This axiom is referenced by:  0cn  10976  1cnd  10979  1ex  10980  mulid1  10982  mulid2  10983  1re  10984  0re  10986  muladd11  11154  peano2cn  11156  mul02lem2  11161  addid1  11164  cnegex2  11166  peano2cnm  11296  0reALT  11327  ine0  11419  mulm1  11425  0lt1  11506  ixi  11613  muleqadd  11628  reccl  11649  recne0  11655  recid  11656  recid2  11657  div1  11673  1div1e1  11674  diveq1  11675  recdiv  11690  divdiv1  11695  divdiv2  11696  recdiv2  11697  conjmul  11701  eqneg  11704  div2neg  11707  recp1lt1  11882  recreclt  11883  recgt0ii  11890  inelr  11972  ofnegsub  11980  peano5nni  11985  nnsscn  11987  nn1m1nn  12003  nn1suc  12004  nnaddcl  12005  nnmulcl  12006  nnne0  12016  nnsub  12026  1m1e0  12054  2cn  12057  3cn  12063  4cn  12067  5cn  12070  6cn  12073  7cn  12076  8cn  12079  9cn  12082  neg1cn  12096  neg1ne0  12098  negneg1e1  12100  1pneg1e0  12101  1m0e1  12103  0p1e1  12104  1p0e1  12106  2m1e1  12108  3m1e2  12110  4m1e3  12111  5m1e4  12112  6m1e5  12113  7m1e6  12114  8m1e7  12115  9m1e8  12116  2p2e4  12117  1p2e3  12125  1p2e3ALT  12126  3p2e5  12133  3p3e6  12134  4p2e6  12135  4p3e7  12136  4p4e8  12137  5p2e7  12138  5p3e8  12139  5p4e9  12140  6p2e8  12141  6p3e9  12142  7p2e9  12143  1t1e1  12144  3t3e9  12149  neg1mulneg1e1  12195  1mhlfehlf  12201  8th4div3  12202  halfpm6th  12203  addltmul  12218  elnn0nn  12284  elz2  12346  zlem1lt  12381  zltlem1  12382  nnaddm1cl  12386  zextlt  12403  zeo  12415  peano5uzi  12418  numsuc  12460  numltc  12472  numsucc  12486  numaddc  12494  6p5lem  12516  5p5e10  12517  6p4e10  12518  7p3e10  12521  8p2e10  12526  10m1e9  12542  4t3lem  12543  7t4e28  12557  9t11e99  12576  decbin2  12587  halfthird  12589  5recm6rec  12590  uzp1  12628  peano2uzr  12652  uzaddcl  12653  rebtwnz  12696  qbtwnre  12942  iccf1o  13237  fz01en  13293  fztp  13321  fzsuc2  13323  fztpval  13327  fseq1m1p1  13340  elfzp1b  13342  fz0to4untppr  13368  predfz  13390  fzoss2  13424  fzval3  13465  fzosplitsnm1  13471  fzo1to4tp  13484  fldiv4p1lem1div2  13564  ceim1l  13576  fldiv  13589  uzrdgxfr  13696  fzen2  13698  nn0ennn  13708  seqm1  13749  seqshft2  13758  monoord2  13763  sermono  13764  seqf1olem1  13771  seqf1olem2  13772  seqz  13780  ser1const  13788  expcl  13809  m1expcl2  13813  expclzlem  13815  expm1t  13820  1exp  13821  mulexpz  13832  expadd  13834  expaddz  13836  expmul  13837  expubnd  13904  sqrecii  13909  neg1sqe1  13922  irec  13927  i4  13930  binom21  13943  sq01  13949  crreczi  13952  bernneq  13953  bernneq2  13954  nn0opthlem1  13991  facndiv  14011  faclbnd4lem1  14016  faclbnd6  14022  bcnp1n  14037  bcm1k  14038  bcp1nk  14040  bcn2  14042  bcp1m1  14043  bcpasc  14044  hashgadd  14101  hashfz  14151  hashfzo  14153  hashxplem  14157  hashbclem  14173  hashf1  14180  seqcoll  14187  swrds1  14388  swrdlsw  14389  wrdind  14444  wrd2ind  14445  swrds2  14662  relexpaddg  14773  rei  14876  imi  14877  recan  15057  iserex  15377  isercoll2  15389  serf0  15401  iseraltlem2  15403  iseraltlem3  15404  iseralt  15405  sumrblem  15432  fsumm1  15472  fsump1  15477  telfsumo  15523  fsumparts  15527  hashiun  15543  binomlem  15550  binom  15551  binom1p  15552  binom11  15553  binom1dif  15554  bcxmas  15556  isumsplit  15561  isum1p  15562  climcndslem1  15570  supcvg  15577  harmonic  15580  arisum  15581  arisum2  15582  trireciplem  15583  geoserg  15587  geolim  15591  geolim2  15592  georeclim  15593  geo2sum  15594  geo2sum2  15595  geoisum1c  15601  0.999...  15602  geoihalfsum  15603  cvgrat  15604  mertenslem1  15605  mertenslem2  15606  mertens  15607  prodf1  15612  prodfclim1  15614  prodrblem  15648  fprodcvg  15649  prodmolem2a  15653  zprod  15656  fprodntriv  15661  prodss  15666  fprodss  15667  fprodsplit  15685  fprodn0f  15710  risefaccl  15734  fallfaccl  15735  risefacfac  15754  binomfallfac  15760  bpolycl  15771  bpolysum  15772  bpolydiflem  15773  fsumkthpow  15775  bpoly2  15776  bpoly3  15777  bpoly4  15778  fsumcube  15779  esum  15799  ege2le3  15808  efsub  15818  efexp  15819  efzval  15820  eftlub  15827  effsumlt  15829  ef4p  15831  tanval3  15852  efi4p  15855  tan0  15869  efival  15870  tanadd  15885  cos2t  15896  cos2tsin  15897  ef01bndlem  15902  cos1bnd  15905  cos2bnd  15906  demoivreALT  15919  eirrlem  15922  rpnnen2lem3  15934  rpnnen2lem11  15942  ruclem12  15959  3dvds  16049  3dvdsdec  16050  3dvds2dec  16051  odd2np1lem  16058  odd2np1  16059  opoe  16081  omoe  16082  opeo  16083  omeo  16084  n2dvdsm1  16087  m1exp1  16094  flodddiv4  16131  bitsfzo  16151  gcdmultipleOLD  16269  sqgcd  16279  nn0seqcvgd  16284  prmind2  16399  hashdvds  16485  phiprmpw  16486  phiprm  16487  eulerthlem2  16492  iserodd  16545  sumhash  16606  fldivp1  16607  prmpwdvds  16614  pockthlem  16615  pockthi  16617  prmreclem4  16629  prmreclem6  16631  4sqlem11  16665  4sqlem19  16673  vdwapun  16684  vdwapid1  16685  vdwlem3  16693  vdwlem5  16695  vdwlem6  16696  vdwlem8  16698  vdwlem9  16699  vdwnnlem2  16706  ramub1lem1  16736  ramub1lem2  16737  ramcl  16739  prmo1  16747  dec5nprm  16776  decexp2  16785  prmlem0  16816  43prm  16832  83prm  16833  139prm  16834  163prm  16835  317prm  16836  631prm  16837  1259lem2  16842  1259lem3  16843  1259lem4  16844  1259lem5  16845  1259prm  16846  2503lem1  16847  2503lem2  16848  2503lem3  16849  2503prm  16850  4001lem1  16851  4001lem2  16852  4001lem3  16853  4001lem4  16854  4001prm  16855  gsumsgrpccat  18487  gsumccatOLD  18488  mulgnndir  18741  mulgneg2  18746  m1expaddsub  19115  sylow1lem1  19212  sylow2a  19233  efgsval2  19348  efgsrel  19349  efgsres  19353  cnfld1  20632  zsssubrg  20665  cnmgpid  20669  zringcyg  20700  mulgrhm2  20709  cnmsgnsubg  20791  cnmsgnbas  20792  cnmsgngrp  20793  psgninv  20796  evpmodpmf1o  20810  blcvx  23970  iihalf2  24105  icopnfcnv  24114  iccpnfhmeo  24117  xrhmeo  24118  icccvx  24122  lebnumii  24138  reparphti  24169  pcoass  24196  pcorevlem  24198  pcorev2  24200  pi1xfrcnv  24229  cnstrcvs  24313  cncvs  24317  ncvsm1  24327  pjthlem1  24610  divcncf  24620  ovolunlem1a  24669  ovolunlem1  24670  ovolicc2lem4  24693  uniioombllem3  24758  uniioombllem4  24759  dyadovol  24766  vitalilem4  24784  mbf0  24807  iblcnlem1  24961  itgcnlem  24963  dvid  25091  dvexp  25126  dvexp2  25127  dvexp3  25151  dveflem  25152  dvlipcn  25167  dvcvx  25193  dvfsumle  25194  dvfsumlem1  25199  degltp1le  25247  ply1divex  25310  fta1glem1  25339  plyaddlem1  25383  plymullem1  25384  coeidp  25433  dgrid  25434  dvply1  25453  dvply2g  25454  plyremlem  25473  fta1lem  25476  vieta1lem1  25479  vieta1lem2  25480  qaa  25492  iaa  25494  aalioulem3  25503  geolim3  25508  aaliou3lem2  25512  aaliou3lem7  25518  taylply2  25536  dvradcnv  25589  pserdvlem2  25596  pserdv2  25598  abelthlem1  25599  abelthlem2  25600  abelthlem6  25604  abelthlem7  25606  abelth  25609  reeff1olem  25614  reeff1o  25615  efcvx  25617  sinhalfpilem  25629  eulerid  25640  cos2pi  25642  sincosq3sgn  25666  sincosq4sgn  25667  tangtx  25671  sincos4thpi  25679  sincos6thpi  25681  pigt3  25683  pige3ALT  25685  abssinper  25686  coskpi  25688  coseq1  25690  efeq1  25693  tanregt0  25704  logneg2  25779  logdivlti  25784  logcnlem4  25809  dvlog2lem  25816  dvlog2  25817  advlog  25818  advlogexp  25819  logtayl  25824  logtayl2  25826  logccv  25827  cxpval  25828  1cxp  25836  cxpcl  25838  cxpp1  25844  cxpsqrt  25867  dvsqrt  25904  dvcnsqrt  25906  sqrtcn  25912  cxpaddlelem  25913  root1id  25916  root1cj  25918  logrec  25922  logb1  25928  logbmpt  25947  ang180lem1  25968  ang180lem2  25969  ang180lem3  25970  isosctrlem1  25977  isosctrlem2  25978  1cubrlem  26000  1cubr  26001  mcubic  26006  binom4  26009  dquartlem1  26010  quartlem1  26016  asinlem  26027  asinlem2  26028  asinlem3a  26029  asinlem3  26030  asinf  26031  atandm2  26036  atandm4  26038  atanf  26039  asinneg  26045  efiasin  26047  sinasin  26048  asinsin  26051  asin1  26053  acos1  26054  reasinsin  26055  asinbnd  26058  cosasin  26063  atanneg  26066  atancj  26069  efiatan  26071  atanlogaddlem  26072  atanlogadd  26073  atanlogsublem  26074  atanlogsub  26075  efiatan2  26076  2efiatan  26077  tanatan  26078  cosatan  26080  cosatanne0  26081  atantan  26082  atanbndlem  26084  bndatandm  26088  atans2  26090  dvatan  26094  atantayl  26096  atantayl2  26097  atantayl3  26098  leibpilem2  26100  leibpi  26101  log2cnv  26103  log2tlbnd  26104  log2ublem3  26107  log2ub  26108  birthdaylem2  26111  birthday  26113  efrlim  26128  dfef2  26129  cvxcl  26143  scvxcvx  26144  emcllem2  26155  emcllem4  26157  emcllem7  26160  harmonicbnd4  26169  fsumharmonic  26170  zetacvg  26173  lgamcvg2  26213  lgam1  26222  gam1  26223  wilthlem1  26226  wilthlem2  26227  wilthlem3  26228  basellem2  26240  basellem5  26243  basellem6  26244  basellem7  26245  basellem8  26246  basellem9  26247  0sgm  26302  mule1  26306  ppiprm  26309  ppinprm  26310  chtprm  26311  chtnprm  26312  chpp1  26313  mumullem2  26338  1sgmprm  26356  1sgm2ppw  26357  ppiub  26361  chtublem  26368  chtub  26369  logfaclbnd  26379  logfacbnd3  26380  logfacrlim  26381  logexprlim  26382  mersenne  26384  perfect1  26385  perfectlem1  26386  perfectlem2  26387  perfect  26388  dchrelbasd  26396  dchrmulid2  26409  dchrfi  26412  dchrsum2  26425  sumdchr2  26427  bcp1ctr  26436  bposlem8  26448  zabsle1  26453  lgslem1  26454  lgslem2  26455  lgsfcl2  26460  lgsvalmod  26473  lgsneg  26478  lgsdilem  26481  lgsdir2lem1  26482  lgsdir2lem2  26483  lgsdir2lem3  26484  lgsdir2lem5  26486  lgsdir2  26487  lgsdir  26489  lgsdi  26491  lgsne0  26492  lgseisenlem1  26532  lgseisenlem2  26533  lgseisen  26536  lgsquadlem1  26537  lgsquadlem2  26538  lgsquad2lem1  26541  lgsquad2  26543  m1lgs  26545  2lgslem3c  26555  2lgsoddprmlem3c  26569  2lgsoddprmlem3d  26570  2sqlem10  26585  2sqlem11  26586  2sqblem  26588  addsqn2reu  26598  addsqrexnreu  26599  addsqnreup  26600  chtppilimlem2  26631  chebbnd2  26634  chto1lb  26635  rplogsumlem1  26641  rpvmasumlem  26644  dchrmusumlema  26650  dchrmusum2  26651  dchrisum0flblem1  26665  rpvmasum2  26669  mudivsum  26687  mulogsum  26689  vmalogdivsum2  26695  selberg2lem  26707  logdivbnd  26713  pntrmax  26721  pntrsumo1  26722  pntrsumbnd2  26724  pntrlog2bndlem5  26738  pntpbnd1a  26742  pntpbnd2  26744  pntibndlem2  26748  pntlemd  26751  pntlemc  26752  pntlemr  26759  brbtwn2  27282  colinearalglem4  27286  ax5seglem1  27305  ax5seglem2  27306  ax5seglem3  27308  ax5seglem5  27310  ax5seglem7  27312  ax5seglem9  27314  axbtwnid  27316  axpaschlem  27317  axlowdimlem13  27331  axlowdimlem14  27332  axlowdimlem16  27334  axeuclidlem  27339  axcontlem2  27342  axcontlem4  27344  axcontlem7  27347  axcontlem8  27348  crctcshwlkn0lem6  28189  clwwlkf1  28422  clwwlknonex2lem2  28481  ex-fl  28820  ex-ind-dvds  28834  vc2OLD  28939  vc0  28945  vcm  28947  nvm1  29036  nvmtri  29042  nvge0  29044  ipval2lem3  29076  ipidsq  29081  lnoadd  29129  ip1ilem  29197  ip1i  29198  ip2i  29199  ipdirilem  29200  ipasslem1  29202  ipasslem2  29203  ipasslem10  29210  minvecolem2  29246  hvsubid  29397  hv2times  29432  hisubcomi  29475  normlem9  29489  normlem7tALT  29490  norm-ii-i  29508  normsubi  29512  hhssnv  29635  pjhthlem1  29762  h1de2bi  29925  homulid2  30171  ho2times  30190  lnop0  30337  lnopaddi  30342  lnophmlem2  30388  lnfn0i  30413  lnfnaddi  30414  hst1h  30598  sto2i  30608  stadd3i  30619  addltmulALT  30817  dpmul4  31197  psgnid  31373  cnmsgn0g  31422  altgnsg  31425  isarchi3  31450  archirngz  31452  ccfldextdgrr  31751  lmatfvlem  31774  qqhval2lem  31940  dya2ub  32246  omssubadd  32276  eulerpartlemgs2  32356  fib5  32381  fib6  32382  ballotlem2  32464  sgnneg  32516  signswch  32549  signlem0  32575  itgexpif  32595  reprlt  32608  breprexp  32622  breprexpnat  32623  hgt750lem2  32641  subfacp1lem5  33155  subfacp1lem6  33156  subfacval2  33158  subfaclim  33159  subfacval3  33160  cvxsconn  33214  resconn  33217  cvmliftlem7  33262  cvmliftlem10  33265  problem4  33635  sinccvglem  33639  sqdivzi  33702  faclimlem1  33718  dnibndlem5  34671  dnibndlem10  34676  ltflcei  35774  sin2h  35776  cos2h  35777  tan2h  35778  poimirlem13  35799  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem31  35817  mblfinlem2  35824  mblfinlem3  35825  dvtan  35836  itg2addnclem3  35839  dvasin  35870  dvacos  35871  areacirc  35879  fdc  35912  mettrifi  35924  heiborlem4  35981  heiborlem6  35983  60gcd7e1  40020  lcmineqlem1  40044  lcmineqlem8  40051  lcmineqlem9  40052  lcmineqlem10  40053  lcmineqlem12  40055  3exp7  40068  3lexlogpow5ineq1  40069  3lexlogpow5ineq5  40075  aks4d1p1p4  40086  aks4d1p1p7  40089  aks4d1p1  40091  facp2  40106  fac2xp3  40167  2xp3dxp2ge1d  40169  factwoffsmonot  40170  sn-1ne2  40302  sqdeccom12  40324  235t711  40326  expgcd  40341  re1m1e0m0  40387  ipiiie0  40426  sn-0tie0  40428  fltnltalem  40506  3cubeslem3l  40515  3cubeslem3r  40516  eldioph2lem1  40589  lzenom  40599  irrapxlem1  40651  rmspecsqrtnq  40735  rmxm1  40763  rmym1  40764  2nn0ind  40774  jm2.24nn  40788  jm2.17a  40789  jm2.17b  40790  jm2.17c  40791  jm2.24  40792  acongeq  40812  jm2.18  40817  jm2.27c  40836  jm3.1lem2  40847  rngunsnply  41005  flcidc  41006  inductionexd  41772  unitadd  41813  hashnzfzclim  41947  ofdivrec  41951  lhe4.4ex1a  41954  expgrowth  41960  dvradcnv2  41972  binomcxplemrat  41975  binomcxplemnotnn0  41981  isosctrlem1ALT  42561  monoord2xrv  43031  dvsinax  43461  dvnprodlem3  43496  itgsin0pilem1  43498  itgsbtaddcnst  43530  stoweidlem13  43561  stoweidlem26  43574  stoweidlem34  43582  stoweidlem38  43586  wallispilem2  43614  wallispilem4  43616  wallispi2lem1  43619  stirlinglem1  43622  stirlinglem5  43626  stirlinglem10  43631  dirkerper  43644  dirkertrigeqlem1  43646  dirkertrigeqlem3  43648  dirkertrigeq  43649  dirkercncflem4  43654  fourierdlem24  43679  sqwvfoura  43776  sqwvfourb  43777  fourierswlem  43778  1t10e1p1e11  44813  fmtnorec3  45011  fmtno5lem4  45019  fmtno5  45020  257prm  45024  fmtno4nprmfac193  45037  m3prm  45055  139prmALT  45059  127prm  45062  m7prm  45063  lighneallem3  45070  proththd  45077  3exp4mod41  45079  41prothprmlem2  45081  perfectALTVlem2  45185  perfectALTV  45186  11t31e341  45195  evengpop3  45261  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  bgoldbtbndlem1  45268  0nodd  45375  altgsumbcALT  45700  exple2lt6  45711  nn0sumshdiglemB  45977  ackval3  46040  ackval3012  46049  line2ylem  46108  onetansqsecsq  46474  cotsqcscsq  46475  5m4e1  46512