Axiom ax-1cn 11165

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

This axiom is referenced by:  0cn  11203  1cnd  11206  1ex  11207  mulrid  11209  mullid  11210  1re  11211  0re  11213  muladd11  11381  peano2cn  11383  mul02lem2  11388  addrid  11391  cnegex2  11393  peano2cnm  11523  0reALT  11554  ine0  11646  mulm1  11652  0lt1  11733  ixi  11840  muleqadd  11855  reccl  11876  recne0  11882  recid  11883  recid2  11884  div1  11900  1div1e1  11901  diveq1  11902  recdiv  11917  divdiv1  11922  divdiv2  11923  recdiv2  11924  conjmul  11928  eqneg  11931  div2neg  11934  recp1lt1  12109  recreclt  12110  recgt0ii  12117  inelr  12199  ofnegsub  12207  peano5nni  12212  nnsscn  12214  nn1m1nn  12230  nn1suc  12231  nnaddcl  12232  nnmulcl  12233  nnne0  12243  nnsub  12253  1m1e0  12281  2cn  12284  3cn  12290  4cn  12294  5cn  12297  6cn  12300  7cn  12303  8cn  12306  9cn  12309  neg1cn  12323  neg1ne0  12325  negneg1e1  12327  1pneg1e0  12328  1m0e1  12330  0p1e1  12331  1p0e1  12333  2m1e1  12335  3m1e2  12337  4m1e3  12338  5m1e4  12339  6m1e5  12340  7m1e6  12341  8m1e7  12342  9m1e8  12343  2p2e4  12344  1p2e3  12352  1p2e3ALT  12353  3p2e5  12360  3p3e6  12361  4p2e6  12362  4p3e7  12363  4p4e8  12364  5p2e7  12365  5p3e8  12366  5p4e9  12367  6p2e8  12368  6p3e9  12369  7p2e9  12370  1t1e1  12371  3t3e9  12376  neg1mulneg1e1  12422  1mhlfehlf  12428  8th4div3  12429  halfpm6th  12430  addltmul  12445  elnn0nn  12511  elz2  12573  zlem1lt  12611  zltlem1  12612  nnaddm1cl  12616  zextlt  12633  zeo  12645  peano5uzi  12648  numsuc  12688  numltc  12700  numsucc  12714  numaddc  12722  6p5lem  12744  5p5e10  12745  6p4e10  12746  7p3e10  12749  8p2e10  12754  10m1e9  12770  4t3lem  12771  7t4e28  12785  9t11e99  12804  decbin2  12815  halfthird  12817  5recm6rec  12818  uzp1  12860  peano2uzr  12884  uzaddcl  12885  rebtwnz  12928  qbtwnre  13175  iccf1o  13470  fz01en  13526  fztp  13554  fzsuc2  13556  fztpval  13560  fseq1m1p1  13573  elfzp1b  13575  fz0to4untppr  13601  predfz  13623  fzoss2  13657  fzval3  13698  fzosplitsnm1  13704  fzo1to4tp  13717  fldiv4p1lem1div2  13797  ceim1l  13809  fldiv  13822  uzrdgxfr  13929  fzen2  13931  nn0ennn  13941  seqm1  13982  seqshft2  13991  monoord2  13996  sermono  13997  seqf1olem1  14004  seqf1olem2  14005  seqz  14013  ser1const  14021  expcl  14042  expclzlem  14046  m1expcl2  14048  expm1t  14053  1exp  14054  mulexpz  14065  expadd  14067  expaddz  14069  expmul  14070  expubnd  14139  sqrecii  14144  neg1sqe1  14157  irec  14162  i4  14165  binom21  14179  sq01  14185  crreczi  14188  bernneq  14189  bernneq2  14190  nn0opthlem1  14225  facndiv  14245  faclbnd4lem1  14250  faclbnd6  14256  bcnp1n  14271  bcm1k  14272  bcp1nk  14274  bcn2  14276  bcp1m1  14277  bcpasc  14278  hashgadd  14334  hashfz  14384  hashfzo  14386  hashxplem  14390  hashbclem  14408  hashf1  14415  seqcoll  14422  swrds1  14613  swrdlsw  14614  wrdind  14669  wrd2ind  14670  swrds2  14888  relexpaddg  14997  rei  15100  imi  15101  recan  15280  iserex  15600  isercoll2  15612  serf0  15624  iseraltlem2  15626  iseraltlem3  15627  iseralt  15628  sumrblem  15654  fsumm1  15694  telfsumo  15745  fsumparts  15749  hashiun  15765  binomlem  15772  binom  15773  binom1p  15774  binom11  15775  binom1dif  15776  bcxmas  15778  isumsplit  15783  isum1p  15784  climcndslem1  15792  supcvg  15799  harmonic  15802  arisum  15803  arisum2  15804  trireciplem  15805  geoserg  15809  geolim  15813  geolim2  15814  georeclim  15815  geo2sum  15816  geo2sum2  15817  geoisum1c  15823  0.999...  15824  geoihalfsum  15825  cvgrat  15826  mertenslem1  15827  mertenslem2  15828  mertens  15829  prodf1  15834  prodfclim1  15836  prodrblem  15870  fprodcvg  15871  prodmolem2a  15875  zprod  15878  fprodntriv  15883  prodss  15888  fprodss  15889  fprodsplit  15907  fprodn0f  15932  risefaccl  15956  fallfaccl  15957  risefacfac  15976  binomfallfac  15982  bpolycl  15993  bpolysum  15994  bpolydiflem  15995  fsumkthpow  15997  bpoly2  15998  bpoly3  15999  bpoly4  16000  fsumcube  16001  esum  16021  ege2le3  16030  efsub  16040  efexp  16041  efzval  16042  eftlub  16049  effsumlt  16051  ef4p  16053  tanval3  16074  efi4p  16077  tan0  16091  efival  16092  tanadd  16107  cos2t  16118  cos2tsin  16119  ef01bndlem  16124  cos1bnd  16127  cos2bnd  16128  demoivreALT  16141  eirrlem  16144  rpnnen2lem3  16156  rpnnen2lem11  16164  ruclem12  16181  3dvds  16271  3dvdsdec  16272  3dvds2dec  16273  odd2np1lem  16280  odd2np1  16281  opoe  16303  omoe  16304  opeo  16305  omeo  16306  n2dvdsm1  16309  m1exp1  16316  flodddiv4  16353  bitsfzo  16373  sqgcd  16499  nn0seqcvgd  16504  prmind2  16619  hashdvds  16705  phiprmpw  16706  phiprm  16707  eulerthlem2  16712  iserodd  16765  sumhash  16826  fldivp1  16827  prmpwdvds  16834  pockthlem  16835  pockthi  16837  prmreclem4  16849  prmreclem6  16851  4sqlem11  16885  4sqlem19  16893  vdwapun  16904  vdwapid1  16905  vdwlem3  16913  vdwlem5  16915  vdwlem6  16916  vdwlem8  16918  vdwlem9  16919  vdwnnlem2  16926  ramub1lem1  16956  ramub1lem2  16957  ramcl  16959  prmo1  16967  dec5nprm  16996  decexp2  17005  prmlem0  17036  43prm  17052  83prm  17053  139prm  17054  163prm  17055  317prm  17056  631prm  17057  1259lem2  17062  1259lem3  17063  1259lem4  17064  1259lem5  17065  1259prm  17066  2503lem1  17067  2503lem2  17068  2503lem3  17069  2503prm  17070  4001lem1  17071  4001lem2  17072  4001lem3  17073  4001lem4  17074  4001prm  17075  gsumsgrpccat  18718  mulgnndir  18978  mulgneg2  18983  m1expaddsub  19361  sylow1lem1  19461  sylow2a  19482  efgsval2  19596  efgsrel  19597  efgsres  19601  cnfld1  20963  zsssubrg  20996  cnmgpid  21000  zringcyg  21031  mulgrhm2  21040  cnmsgnsubg  21122  cnmsgnbas  21123  cnmsgngrp  21124  psgninv  21127  evpmodpmf1o  21141  blcvx  24306  iihalf2  24441  icopnfcnv  24450  iccpnfhmeo  24453  xrhmeo  24454  icccvx  24458  lebnumii  24474  reparphti  24505  pcoass  24532  pcorevlem  24534  pcorev2  24536  pi1xfrcnv  24565  cnstrcvs  24649  cncvs  24653  ncvsm1  24663  pjthlem1  24946  divcncf  24956  ovolunlem1a  25005  ovolunlem1  25006  ovolicc2lem4  25029  uniioombllem3  25094  uniioombllem4  25095  dyadovol  25102  vitalilem4  25120  mbf0  25143  iblcnlem1  25297  itgcnlem  25299  dvid  25427  dvexp  25462  dvexp2  25463  dvexp3  25487  dveflem  25488  dvlipcn  25503  dvcvx  25529  dvfsumle  25530  dvfsumlem1  25535  degltp1le  25583  ply1divex  25646  fta1glem1  25675  plyaddlem1  25719  plymullem1  25720  coeidp  25769  dgrid  25770  dvply1  25789  dvply2g  25790  plyremlem  25809  fta1lem  25812  vieta1lem1  25815  vieta1lem2  25816  qaa  25828  iaa  25830  aalioulem3  25839  geolim3  25844  aaliou3lem2  25848  aaliou3lem7  25854  taylply2  25872  dvradcnv  25925  pserdvlem2  25932  pserdv2  25934  abelthlem1  25935  abelthlem2  25936  abelthlem6  25940  abelthlem7  25942  abelth  25945  reeff1olem  25950  reeff1o  25951  efcvx  25953  sinhalfpilem  25965  eulerid  25976  cos2pi  25978  sincosq3sgn  26002  sincosq4sgn  26003  tangtx  26007  sincos4thpi  26015  sincos6thpi  26017  pigt3  26019  pige3ALT  26021  abssinper  26022  coskpi  26024  coseq1  26026  efeq1  26029  tanregt0  26040  logneg2  26115  logdivlti  26120  logcnlem4  26145  dvlog2lem  26152  dvlog2  26153  advlog  26154  advlogexp  26155  logtayl  26160  logtayl2  26162  logccv  26163  cxpval  26164  1cxp  26172  cxpcl  26174  cxpp1  26180  cxpsqrt  26203  dvsqrt  26240  dvcnsqrt  26242  sqrtcn  26248  cxpaddlelem  26249  root1id  26252  root1cj  26254  logrec  26258  logb1  26264  logbmpt  26283  ang180lem1  26304  ang180lem2  26305  ang180lem3  26306  isosctrlem1  26313  isosctrlem2  26314  1cubrlem  26336  1cubr  26337  mcubic  26342  binom4  26345  dquartlem1  26346  quartlem1  26352  asinlem  26363  asinlem2  26364  asinlem3a  26365  asinlem3  26366  asinf  26367  atandm2  26372  atandm4  26374  atanf  26375  asinneg  26381  efiasin  26383  sinasin  26384  asinsin  26387  asin1  26389  acos1  26390  reasinsin  26391  asinbnd  26394  cosasin  26399  atanneg  26402  atancj  26405  efiatan  26407  atanlogaddlem  26408  atanlogadd  26409  atanlogsublem  26410  atanlogsub  26411  efiatan2  26412  2efiatan  26413  tanatan  26414  cosatan  26416  cosatanne0  26417  atantan  26418  atanbndlem  26420  bndatandm  26424  atans2  26426  dvatan  26430  atantayl  26432  atantayl2  26433  atantayl3  26434  leibpilem2  26436  leibpi  26437  log2cnv  26439  log2tlbnd  26440  log2ublem3  26443  log2ub  26444  birthdaylem2  26447  birthday  26449  efrlim  26464  dfef2  26465  cvxcl  26479  scvxcvx  26480  emcllem2  26491  emcllem4  26493  emcllem7  26496  harmonicbnd4  26505  fsumharmonic  26506  zetacvg  26509  lgamcvg2  26549  lgam1  26558  gam1  26559  wilthlem1  26562  wilthlem2  26563  wilthlem3  26564  basellem2  26576  basellem5  26579  basellem6  26580  basellem7  26581  basellem8  26582  basellem9  26583  0sgm  26638  mule1  26642  ppiprm  26645  ppinprm  26646  chtprm  26647  chtnprm  26648  chpp1  26649  mumullem2  26674  1sgmprm  26692  1sgm2ppw  26693  ppiub  26697  chtublem  26704  chtub  26705  logfaclbnd  26715  logfacbnd3  26716  logfacrlim  26717  logexprlim  26718  mersenne  26720  perfect1  26721  perfectlem1  26722  perfectlem2  26723  perfect  26724  dchrelbasd  26732  dchrmullid  26745  dchrfi  26748  dchrsum2  26761  sumdchr2  26763  bcp1ctr  26772  bposlem8  26784  zabsle1  26789  lgslem1  26790  lgslem2  26791  lgsfcl2  26796  lgsvalmod  26809  lgsneg  26814  lgsdilem  26817  lgsdir2lem1  26818  lgsdir2lem2  26819  lgsdir2lem3  26820  lgsdir2lem5  26822  lgsdir2  26823  lgsdir  26825  lgsdi  26827  lgsne0  26828  lgseisenlem1  26868  lgseisenlem2  26869  lgseisen  26872  lgsquadlem1  26873  lgsquadlem2  26874  lgsquad2lem1  26877  lgsquad2  26879  m1lgs  26881  2lgslem3c  26891  2lgsoddprmlem3c  26905  2lgsoddprmlem3d  26906  2sqlem10  26921  2sqlem11  26922  2sqblem  26924  addsqn2reu  26934  addsqrexnreu  26935  addsqnreup  26936  chtppilimlem2  26967  chebbnd2  26970  chto1lb  26971  rplogsumlem1  26977  rpvmasumlem  26980  dchrmusumlema  26986  dchrmusum2  26987  dchrisum0flblem1  27001  rpvmasum2  27005  mudivsum  27023  mulogsum  27025  vmalogdivsum2  27031  selberg2lem  27043  logdivbnd  27049  pntrmax  27057  pntrsumo1  27058  pntrsumbnd2  27060  pntrlog2bndlem5  27074  pntpbnd1a  27078  pntpbnd2  27080  pntibndlem2  27084  pntlemd  27087  pntlemc  27088  pntlemr  27095  brbtwn2  28153  colinearalglem4  28157  ax5seglem1  28176  ax5seglem2  28177  ax5seglem3  28179  ax5seglem5  28181  ax5seglem7  28183  ax5seglem9  28185  axbtwnid  28187  axpaschlem  28188  axlowdimlem13  28202  axlowdimlem14  28203  axlowdimlem16  28205  axeuclidlem  28210  axcontlem2  28213  axcontlem4  28215  axcontlem7  28218  axcontlem8  28219  crctcshwlkn0lem6  29059  clwwlkf1  29292  clwwlknonex2lem2  29351  ex-fl  29690  ex-ind-dvds  29704  vc2OLD  29809  vc0  29815  vcm  29817  nvm1  29906  nvmtri  29912  nvge0  29914  ipval2lem3  29946  ipidsq  29951  lnoadd  29999  ip1ilem  30067  ip1i  30068  ip2i  30069  ipdirilem  30070  ipasslem1  30072  ipasslem2  30073  ipasslem10  30080  minvecolem2  30116  hvsubid  30267  hv2times  30302  hisubcomi  30345  normlem9  30359  normlem7tALT  30360  norm-ii-i  30378  normsubi  30382  hhssnv  30505  pjhthlem1  30632  h1de2bi  30795  homullid  31041  ho2times  31060  lnop0  31207  lnopaddi  31212  lnophmlem2  31258  lnfn0i  31283  lnfnaddi  31284  hst1h  31468  sto2i  31478  stadd3i  31489  addltmulALT  31687  dpmul4  32068  psgnid  32244  cnmsgn0g  32293  altgnsg  32296  isarchi3  32321  archirngz  32323  1fldgenq  32401  ccfldextdgrr  32735  lmatfvlem  32784  qqhval2lem  32950  dya2ub  33258  omssubadd  33288  eulerpartlemgs2  33368  fib5  33393  fib6  33394  ballotlem2  33476  sgnneg  33528  signswch  33561  signlem0  33587  itgexpif  33607  reprlt  33620  breprexp  33634  breprexpnat  33635  hgt750lem2  33653  subfacp1lem5  34164  subfacp1lem6  34165  subfacval2  34167  subfaclim  34168  subfacval3  34169  cvxsconn  34223  resconn  34226  cvmliftlem7  34271  cvmliftlem10  34274  problem4  34642  sinccvglem  34646  sqdivzi  34686  faclimlem1  34702  gg-reparphti  35161  gg-dvfsumle  35171  dnibndlem5  35347  dnibndlem10  35352  ltflcei  36465  sin2h  36467  cos2h  36468  tan2h  36469  poimirlem13  36490  poimirlem16  36493  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem31  36508  mblfinlem2  36515  mblfinlem3  36516  dvtan  36527  itg2addnclem3  36530  dvasin  36561  dvacos  36562  areacirc  36570  fdc  36602  mettrifi  36614  heiborlem4  36671  heiborlem6  36673  60gcd7e1  40859  lcmineqlem1  40883  lcmineqlem8  40890  lcmineqlem9  40891  lcmineqlem10  40892  lcmineqlem12  40894  3exp7  40907  3lexlogpow5ineq1  40908  3lexlogpow5ineq5  40914  aks4d1p1p4  40925  aks4d1p1p7  40928  aks4d1p1  40930  facp2  40948  fac2xp3  41009  2xp3dxp2ge1d  41011  factwoffsmonot  41012  sn-1ne2  41177  sqdeccom12  41199  235t711  41201  expgcd  41221  re1m1e0m0  41267  ipiiie0  41307  sn-0tie0  41309  fltnltalem  41401  3cubeslem3l  41410  3cubeslem3r  41411  eldioph2lem1  41484  lzenom  41494  irrapxlem1  41546  rmspecsqrtnq  41630  rmxm1  41659  rmym1  41660  2nn0ind  41670  jm2.24nn  41684  jm2.17a  41685  jm2.17b  41686  jm2.17c  41687  jm2.24  41688  acongeq  41708  jm2.18  41713  jm2.27c  41732  jm3.1lem2  41743  rngunsnply  41901  flcidc  41902  inductionexd  42892  unitadd  42933  hashnzfzclim  43067  ofdivrec  43071  lhe4.4ex1a  43074  expgrowth  43080  dvradcnv2  43092  binomcxplemrat  43095  binomcxplemnotnn0  43101  isosctrlem1ALT  43681  monoord2xrv  44181  dvsinax  44616  dvnprodlem3  44651  itgsin0pilem1  44653  itgsbtaddcnst  44685  stoweidlem13  44716  stoweidlem26  44729  stoweidlem34  44737  stoweidlem38  44741  wallispilem2  44769  wallispilem4  44771  wallispi2lem1  44774  stirlinglem1  44777  stirlinglem5  44781  stirlinglem10  44786  dirkerper  44799  dirkertrigeqlem1  44801  dirkertrigeqlem3  44803  dirkertrigeq  44804  dirkercncflem4  44809  fourierdlem24  44834  sqwvfoura  44931  sqwvfourb  44932  fourierswlem  44933  1t10e1p1e11  46005  fmtnorec3  46203  fmtno5lem4  46211  fmtno5  46212  257prm  46216  fmtno4nprmfac193  46229  m3prm  46247  139prmALT  46251  127prm  46254  m7prm  46255  lighneallem3  46262  proththd  46269  3exp4mod41  46271  41prothprmlem2  46273  perfectALTVlem2  46377  perfectALTV  46378  11t31e341  46387  evengpop3  46453  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  bgoldbtbndlem1  46460  0nodd  46567  altgsumbcALT  46983  exple2lt6  46994  nn0sumshdiglemB  47260  ackval3  47323  ackval3012  47332  line2ylem  47391  onetansqsecsq  47760  cotsqcscsq  47761  5m4e1  47798