Axiom ax-1cn 11168

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

This axiom is referenced by:  0cn  11206  1cnd  11209  1ex  11210  mulrid  11212  mullid  11213  1re  11214  0re  11216  muladd11  11384  peano2cn  11386  mul02lem2  11391  addrid  11394  cnegex2  11396  peano2cnm  11526  0reALT  11557  ine0  11649  mulm1  11655  0lt1  11736  ixi  11843  muleqadd  11858  reccl  11879  recne0  11885  recid  11886  recid2  11887  div1  11903  1div1e1  11904  diveq1  11905  recdiv  11920  divdiv1  11925  divdiv2  11926  recdiv2  11927  conjmul  11931  eqneg  11934  div2neg  11937  recp1lt1  12112  recreclt  12113  recgt0ii  12120  inelr  12202  ofnegsub  12210  peano5nni  12215  nnsscn  12217  nn1m1nn  12233  nn1suc  12234  nnaddcl  12235  nnmulcl  12236  nnne0  12246  nnsub  12256  1m1e0  12284  2cn  12287  3cn  12293  4cn  12297  5cn  12300  6cn  12303  7cn  12306  8cn  12309  9cn  12312  neg1cn  12326  neg1ne0  12328  negneg1e1  12330  1pneg1e0  12331  1m0e1  12333  0p1e1  12334  1p0e1  12336  2m1e1  12338  3m1e2  12340  4m1e3  12341  5m1e4  12342  6m1e5  12343  7m1e6  12344  8m1e7  12345  9m1e8  12346  2p2e4  12347  1p2e3  12355  1p2e3ALT  12356  3p2e5  12363  3p3e6  12364  4p2e6  12365  4p3e7  12366  4p4e8  12367  5p2e7  12368  5p3e8  12369  5p4e9  12370  6p2e8  12371  6p3e9  12372  7p2e9  12373  1t1e1  12374  3t3e9  12379  neg1mulneg1e1  12425  1mhlfehlf  12431  8th4div3  12432  halfpm6th  12433  addltmul  12448  elnn0nn  12514  elz2  12576  zlem1lt  12614  zltlem1  12615  nnaddm1cl  12619  zextlt  12636  zeo  12648  peano5uzi  12651  numsuc  12691  numltc  12703  numsucc  12717  numaddc  12725  6p5lem  12747  5p5e10  12748  6p4e10  12749  7p3e10  12752  8p2e10  12757  10m1e9  12773  4t3lem  12774  7t4e28  12788  9t11e99  12807  decbin2  12818  halfthird  12820  5recm6rec  12821  uzp1  12863  peano2uzr  12887  uzaddcl  12888  rebtwnz  12931  qbtwnre  13178  iccf1o  13473  fz01en  13529  fztp  13557  fzsuc2  13559  fztpval  13563  fseq1m1p1  13576  elfzp1b  13578  fz0to4untppr  13604  predfz  13626  fzoss2  13660  fzval3  13701  fzosplitsnm1  13707  fzo1to4tp  13720  fldiv4p1lem1div2  13800  ceim1l  13812  fldiv  13825  uzrdgxfr  13932  fzen2  13934  nn0ennn  13944  seqm1  13985  seqshft2  13994  monoord2  13999  sermono  14000  seqf1olem1  14007  seqf1olem2  14008  seqz  14016  ser1const  14024  expcl  14045  expclzlem  14049  m1expcl2  14051  expm1t  14056  1exp  14057  mulexpz  14068  expadd  14070  expaddz  14072  expmul  14073  expubnd  14142  sqrecii  14147  neg1sqe1  14160  irec  14165  i4  14168  binom21  14182  sq01  14188  crreczi  14191  bernneq  14192  bernneq2  14193  nn0opthlem1  14228  facndiv  14248  faclbnd4lem1  14253  faclbnd6  14259  bcnp1n  14274  bcm1k  14275  bcp1nk  14277  bcn2  14279  bcp1m1  14280  bcpasc  14281  hashgadd  14337  hashfz  14387  hashfzo  14389  hashxplem  14393  hashbclem  14411  hashf1  14418  seqcoll  14425  swrds1  14616  swrdlsw  14617  wrdind  14672  wrd2ind  14673  swrds2  14891  relexpaddg  15000  rei  15103  imi  15104  recan  15283  iserex  15603  isercoll2  15615  serf0  15627  iseraltlem2  15629  iseraltlem3  15630  iseralt  15631  sumrblem  15657  fsumm1  15697  telfsumo  15748  fsumparts  15752  hashiun  15768  binomlem  15775  binom  15776  binom1p  15777  binom11  15778  binom1dif  15779  bcxmas  15781  isumsplit  15786  isum1p  15787  climcndslem1  15795  supcvg  15802  harmonic  15805  arisum  15806  arisum2  15807  trireciplem  15808  geoserg  15812  geolim  15816  geolim2  15817  georeclim  15818  geo2sum  15819  geo2sum2  15820  geoisum1c  15826  0.999...  15827  geoihalfsum  15828  cvgrat  15829  mertenslem1  15830  mertenslem2  15831  mertens  15832  prodf1  15837  prodfclim1  15839  prodrblem  15873  fprodcvg  15874  prodmolem2a  15878  zprod  15881  fprodntriv  15886  prodss  15891  fprodss  15892  fprodsplit  15910  fprodn0f  15935  risefaccl  15959  fallfaccl  15960  risefacfac  15979  binomfallfac  15985  bpolycl  15996  bpolysum  15997  bpolydiflem  15998  fsumkthpow  16000  bpoly2  16001  bpoly3  16002  bpoly4  16003  fsumcube  16004  esum  16024  ege2le3  16033  efsub  16043  efexp  16044  efzval  16045  eftlub  16052  effsumlt  16054  ef4p  16056  tanval3  16077  efi4p  16080  tan0  16094  efival  16095  tanadd  16110  cos2t  16121  cos2tsin  16122  ef01bndlem  16127  cos1bnd  16130  cos2bnd  16131  demoivreALT  16144  eirrlem  16147  rpnnen2lem3  16159  rpnnen2lem11  16167  ruclem12  16184  3dvds  16274  3dvdsdec  16275  3dvds2dec  16276  odd2np1lem  16283  odd2np1  16284  opoe  16306  omoe  16307  opeo  16308  omeo  16309  n2dvdsm1  16312  m1exp1  16319  flodddiv4  16356  bitsfzo  16376  sqgcd  16502  nn0seqcvgd  16507  prmind2  16622  hashdvds  16708  phiprmpw  16709  phiprm  16710  eulerthlem2  16715  iserodd  16768  sumhash  16829  fldivp1  16830  prmpwdvds  16837  pockthlem  16838  pockthi  16840  prmreclem4  16852  prmreclem6  16854  4sqlem11  16888  4sqlem19  16896  vdwapun  16907  vdwapid1  16908  vdwlem3  16916  vdwlem5  16918  vdwlem6  16919  vdwlem8  16921  vdwlem9  16922  vdwnnlem2  16929  ramub1lem1  16959  ramub1lem2  16960  ramcl  16962  prmo1  16970  dec5nprm  16999  decexp2  17008  prmlem0  17039  43prm  17055  83prm  17056  139prm  17057  163prm  17058  317prm  17059  631prm  17060  1259lem2  17065  1259lem3  17066  1259lem4  17067  1259lem5  17068  1259prm  17069  2503lem1  17070  2503lem2  17071  2503lem3  17072  2503prm  17073  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001lem4  17077  4001prm  17078  gsumsgrpccat  18721  mulgnndir  18983  mulgneg2  18988  m1expaddsub  19366  sylow1lem1  19466  sylow2a  19487  efgsval2  19601  efgsrel  19602  efgsres  19606  cnfld1  20970  zsssubrg  21003  cnmgpid  21007  zringcyg  21039  mulgrhm2  21048  cnmsgnsubg  21130  cnmsgnbas  21131  cnmsgngrp  21132  psgninv  21135  evpmodpmf1o  21149  blcvx  24314  iihalf2  24449  icopnfcnv  24458  iccpnfhmeo  24461  xrhmeo  24462  icccvx  24466  lebnumii  24482  reparphti  24513  pcoass  24540  pcorevlem  24542  pcorev2  24544  pi1xfrcnv  24573  cnstrcvs  24657  cncvs  24661  ncvsm1  24671  pjthlem1  24954  divcncf  24964  ovolunlem1a  25013  ovolunlem1  25014  ovolicc2lem4  25037  uniioombllem3  25102  uniioombllem4  25103  dyadovol  25110  vitalilem4  25128  mbf0  25151  iblcnlem1  25305  itgcnlem  25307  dvid  25435  dvexp  25470  dvexp2  25471  dvexp3  25495  dveflem  25496  dvlipcn  25511  dvcvx  25537  dvfsumle  25538  dvfsumlem1  25543  degltp1le  25591  ply1divex  25654  fta1glem1  25683  plyaddlem1  25727  plymullem1  25728  coeidp  25777  dgrid  25778  dvply1  25797  dvply2g  25798  plyremlem  25817  fta1lem  25820  vieta1lem1  25823  vieta1lem2  25824  qaa  25836  iaa  25838  aalioulem3  25847  geolim3  25852  aaliou3lem2  25856  aaliou3lem7  25862  taylply2  25880  dvradcnv  25933  pserdvlem2  25940  pserdv2  25942  abelthlem1  25943  abelthlem2  25944  abelthlem6  25948  abelthlem7  25950  abelth  25953  reeff1olem  25958  reeff1o  25959  efcvx  25961  sinhalfpilem  25973  eulerid  25984  cos2pi  25986  sincosq3sgn  26010  sincosq4sgn  26011  tangtx  26015  sincos4thpi  26023  sincos6thpi  26025  pigt3  26027  pige3ALT  26029  abssinper  26030  coskpi  26032  coseq1  26034  efeq1  26037  tanregt0  26048  logneg2  26123  logdivlti  26128  logcnlem4  26153  dvlog2lem  26160  dvlog2  26161  advlog  26162  advlogexp  26163  logtayl  26168  logtayl2  26170  logccv  26171  cxpval  26172  1cxp  26180  cxpcl  26182  cxpp1  26188  cxpsqrt  26211  dvsqrt  26250  dvcnsqrt  26252  sqrtcn  26258  cxpaddlelem  26259  root1id  26262  root1cj  26264  logrec  26268  logb1  26274  logbmpt  26293  ang180lem1  26314  ang180lem2  26315  ang180lem3  26316  isosctrlem1  26323  isosctrlem2  26324  1cubrlem  26346  1cubr  26347  mcubic  26352  binom4  26355  dquartlem1  26356  quartlem1  26362  asinlem  26373  asinlem2  26374  asinlem3a  26375  asinlem3  26376  asinf  26377  atandm2  26382  atandm4  26384  atanf  26385  asinneg  26391  efiasin  26393  sinasin  26394  asinsin  26397  asin1  26399  acos1  26400  reasinsin  26401  asinbnd  26404  cosasin  26409  atanneg  26412  atancj  26415  efiatan  26417  atanlogaddlem  26418  atanlogadd  26419  atanlogsublem  26420  atanlogsub  26421  efiatan2  26422  2efiatan  26423  tanatan  26424  cosatan  26426  cosatanne0  26427  atantan  26428  atanbndlem  26430  bndatandm  26434  atans2  26436  dvatan  26440  atantayl  26442  atantayl2  26443  atantayl3  26444  leibpilem2  26446  leibpi  26447  log2cnv  26449  log2tlbnd  26450  log2ublem3  26453  log2ub  26454  birthdaylem2  26457  birthday  26459  efrlim  26474  dfef2  26475  cvxcl  26489  scvxcvx  26490  emcllem2  26501  emcllem4  26503  emcllem7  26506  harmonicbnd4  26515  fsumharmonic  26516  zetacvg  26519  lgamcvg2  26559  lgam1  26568  gam1  26569  wilthlem1  26572  wilthlem2  26573  wilthlem3  26574  basellem2  26586  basellem5  26589  basellem6  26590  basellem7  26591  basellem8  26592  basellem9  26593  0sgm  26648  mule1  26652  ppiprm  26655  ppinprm  26656  chtprm  26657  chtnprm  26658  chpp1  26659  mumullem2  26684  1sgmprm  26702  1sgm2ppw  26703  ppiub  26707  chtublem  26714  chtub  26715  logfaclbnd  26725  logfacbnd3  26726  logfacrlim  26727  logexprlim  26728  mersenne  26730  perfect1  26731  perfectlem1  26732  perfectlem2  26733  perfect  26734  dchrelbasd  26742  dchrmullid  26755  dchrfi  26758  dchrsum2  26771  sumdchr2  26773  bcp1ctr  26782  bposlem8  26794  zabsle1  26799  lgslem1  26800  lgslem2  26801  lgsfcl2  26806  lgsvalmod  26819  lgsneg  26824  lgsdilem  26827  lgsdir2lem1  26828  lgsdir2lem2  26829  lgsdir2lem3  26830  lgsdir2lem5  26832  lgsdir2  26833  lgsdir  26835  lgsdi  26837  lgsne0  26838  lgseisenlem1  26878  lgseisenlem2  26879  lgseisen  26882  lgsquadlem1  26883  lgsquadlem2  26884  lgsquad2lem1  26887  lgsquad2  26889  m1lgs  26891  2lgslem3c  26901  2lgsoddprmlem3c  26915  2lgsoddprmlem3d  26916  2sqlem10  26931  2sqlem11  26932  2sqblem  26934  addsqn2reu  26944  addsqrexnreu  26945  addsqnreup  26946  chtppilimlem2  26977  chebbnd2  26980  chto1lb  26981  rplogsumlem1  26987  rpvmasumlem  26990  dchrmusumlema  26996  dchrmusum2  26997  dchrisum0flblem1  27011  rpvmasum2  27015  mudivsum  27033  mulogsum  27035  vmalogdivsum2  27041  selberg2lem  27053  logdivbnd  27059  pntrmax  27067  pntrsumo1  27068  pntrsumbnd2  27070  pntrlog2bndlem5  27084  pntpbnd1a  27088  pntpbnd2  27090  pntibndlem2  27094  pntlemd  27097  pntlemc  27098  pntlemr  27105  brbtwn2  28163  colinearalglem4  28167  ax5seglem1  28186  ax5seglem2  28187  ax5seglem3  28189  ax5seglem5  28191  ax5seglem7  28193  ax5seglem9  28195  axbtwnid  28197  axpaschlem  28198  axlowdimlem13  28212  axlowdimlem14  28213  axlowdimlem16  28215  axeuclidlem  28220  axcontlem2  28223  axcontlem4  28225  axcontlem7  28228  axcontlem8  28229  crctcshwlkn0lem6  29069  clwwlkf1  29302  clwwlknonex2lem2  29361  ex-fl  29700  ex-ind-dvds  29714  vc2OLD  29821  vc0  29827  vcm  29829  nvm1  29918  nvmtri  29924  nvge0  29926  ipval2lem3  29958  ipidsq  29963  lnoadd  30011  ip1ilem  30079  ip1i  30080  ip2i  30081  ipdirilem  30082  ipasslem1  30084  ipasslem2  30085  ipasslem10  30092  minvecolem2  30128  hvsubid  30279  hv2times  30314  hisubcomi  30357  normlem9  30371  normlem7tALT  30372  norm-ii-i  30390  normsubi  30394  hhssnv  30517  pjhthlem1  30644  h1de2bi  30807  homullid  31053  ho2times  31072  lnop0  31219  lnopaddi  31224  lnophmlem2  31270  lnfn0i  31295  lnfnaddi  31296  hst1h  31480  sto2i  31490  stadd3i  31501  addltmulALT  31699  dpmul4  32080  psgnid  32256  cnmsgn0g  32305  altgnsg  32308  isarchi3  32333  archirngz  32335  1fldgenq  32412  ccfldextdgrr  32746  lmatfvlem  32795  qqhval2lem  32961  dya2ub  33269  omssubadd  33299  eulerpartlemgs2  33379  fib5  33404  fib6  33405  ballotlem2  33487  sgnneg  33539  signswch  33572  signlem0  33598  itgexpif  33618  reprlt  33631  breprexp  33645  breprexpnat  33646  hgt750lem2  33664  subfacp1lem5  34175  subfacp1lem6  34176  subfacval2  34178  subfaclim  34179  subfacval3  34180  cvxsconn  34234  resconn  34237  cvmliftlem7  34282  cvmliftlem10  34285  problem4  34653  sinccvglem  34657  sqdivzi  34697  faclimlem1  34713  gg-reparphti  35172  gg-dvfsumle  35182  dnibndlem5  35358  dnibndlem10  35363  ltflcei  36476  sin2h  36478  cos2h  36479  tan2h  36480  poimirlem13  36501  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem31  36519  mblfinlem2  36526  mblfinlem3  36527  dvtan  36538  itg2addnclem3  36541  dvasin  36572  dvacos  36573  areacirc  36581  fdc  36613  mettrifi  36625  heiborlem4  36682  heiborlem6  36684  60gcd7e1  40870  lcmineqlem1  40894  lcmineqlem8  40901  lcmineqlem9  40902  lcmineqlem10  40903  lcmineqlem12  40905  3exp7  40918  3lexlogpow5ineq1  40919  3lexlogpow5ineq5  40925  aks4d1p1p4  40936  aks4d1p1p7  40939  aks4d1p1  40941  facp2  40959  fac2xp3  41020  2xp3dxp2ge1d  41022  factwoffsmonot  41023  sn-1ne2  41179  sqdeccom12  41201  235t711  41205  expgcd  41225  re1m1e0m0  41270  ipiiie0  41310  sn-0tie0  41312  fltnltalem  41404  sum9cubes  41414  3cubeslem3l  41424  3cubeslem3r  41425  eldioph2lem1  41498  lzenom  41508  irrapxlem1  41560  rmspecsqrtnq  41644  rmxm1  41673  rmym1  41674  2nn0ind  41684  jm2.24nn  41698  jm2.17a  41699  jm2.17b  41700  jm2.17c  41701  jm2.24  41702  acongeq  41722  jm2.18  41727  jm2.27c  41746  jm3.1lem2  41757  rngunsnply  41915  flcidc  41916  inductionexd  42906  unitadd  42947  hashnzfzclim  43081  ofdivrec  43085  lhe4.4ex1a  43088  expgrowth  43094  dvradcnv2  43106  binomcxplemrat  43109  binomcxplemnotnn0  43115  isosctrlem1ALT  43695  monoord2xrv  44194  dvsinax  44629  dvnprodlem3  44664  itgsin0pilem1  44666  itgsbtaddcnst  44698  stoweidlem13  44729  stoweidlem26  44742  stoweidlem34  44750  stoweidlem38  44754  wallispilem2  44782  wallispilem4  44784  wallispi2lem1  44787  stirlinglem1  44790  stirlinglem5  44794  stirlinglem10  44799  dirkerper  44812  dirkertrigeqlem1  44814  dirkertrigeqlem3  44816  dirkertrigeq  44817  dirkercncflem4  44822  fourierdlem24  44847  sqwvfoura  44944  sqwvfourb  44945  fourierswlem  44946  1t10e1p1e11  46018  fmtnorec3  46216  fmtno5lem4  46224  fmtno5  46225  257prm  46229  fmtno4nprmfac193  46242  m3prm  46260  139prmALT  46264  127prm  46267  m7prm  46268  lighneallem3  46275  proththd  46282  3exp4mod41  46284  41prothprmlem2  46286  perfectALTVlem2  46390  perfectALTV  46391  11t31e341  46400  evengpop3  46466  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  bgoldbtbndlem1  46473  0nodd  46580  pzriprng1ALT  46820  altgsumbcALT  47029  exple2lt6  47040  nn0sumshdiglemB  47306  ackval3  47369  ackval3012  47378  line2ylem  47437  onetansqsecsq  47806  cotsqcscsq  47807  5m4e1  47844