Axiom ax-1cn 11093

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

This axiom is referenced by:  0cn  11133  1cnd  11136  1ex  11137  mulrid  11139  mullid  11140  1re  11141  0re  11143  muladd11  11313  peano2cn  11315  mul02lem2  11320  addrid  11323  cnegex2  11325  peano2cnm  11457  0reALT  11488  ine0  11582  mulm1  11588  0lt1  11669  ixi  11776  muleqadd  11791  reccl  11813  recne0  11819  recid  11820  recid2  11821  diveq1  11836  div1  11841  1div1e1  11842  recdiv  11858  divdiv1  11863  divdiv2  11864  recdiv2  11865  conjmul  11869  eqneg  11872  div2neg  11875  recp1lt1  12051  recreclt  12052  recgt0ii  12059  neg1cn  12141  neg1ne0  12143  negneg1e1  12145  ofnegsub  12154  peano5nni  12174  nnsscn  12176  nn1m1nn  12192  nn1suc  12193  nnaddcl  12194  nnmulcl  12195  nnne0  12208  nnsub  12218  1m1e0  12250  2cn  12253  3cn  12259  4cn  12263  5cn  12266  6cn  12269  7cn  12272  8cn  12275  9cn  12278  1pneg1e0  12292  1m0e1  12294  0p1e1  12295  1p0e1  12297  2m1e1  12299  3m1e2  12301  4m1e3  12302  5m1e4  12303  6m1e5  12304  7m1e6  12305  8m1e7  12306  9m1e8  12307  2p2e4  12308  1p2e3  12316  1p2e3ALT  12317  3p2e5  12324  3p3e6  12325  4p2e6  12326  4p3e7  12327  4p4e8  12328  5p2e7  12329  5p3e8  12330  5p4e9  12331  6p2e8  12332  6p3e9  12333  7p2e9  12334  1t1e1  12335  3t3e9  12340  neg1mulneg1e1  12386  1mhlfehlf  12393  8th4div3  12394  halfthird  12395  halfpm6th  12396  addltmul  12410  elnn0nn  12476  elz2  12539  zlem1lt  12576  zltlem1  12577  nnaddm1cl  12583  zextlt  12600  zeo  12612  peano5uzi  12615  numsuc  12655  numltc  12667  numsucc  12681  numaddc  12689  6p5lem  12711  5p5e10  12712  6p4e10  12713  7p3e10  12716  8p2e10  12721  10m1e9  12737  4t3lem  12738  7t4e28  12752  9t11e99  12771  decbin2  12782  5recm6rec  12784  uzp1  12822  peano2uzr  12850  uzaddcl  12851  rebtwnz  12894  qbtwnre  13148  iccf1o  13446  fz01en  13503  fztp  13531  fzsuc2  13533  fztpval  13537  fseq1m1p1  13550  elfzp1b  13552  predfz  13604  fzoss2  13639  fzval3  13686  fzosplitsnm1  13692  fzo1to4tp  13706  fldiv4p1lem1div2  13791  ceim1l  13803  fldiv  13816  uzrdgxfr  13926  fzen2  13928  nn0ennn  13938  seqm1  13978  seqshft2  13987  monoord2  13992  sermono  13993  seqf1olem1  14000  seqf1olem2  14001  seqz  14009  ser1const  14017  expcl  14038  expclzlem  14042  m1expcl2  14044  expm1t  14049  1exp  14050  mulexpz  14061  expadd  14063  expaddz  14065  expmul  14066  expubnd  14137  sqrecii  14142  neg1sqe1  14155  irec  14160  i4  14163  binom21  14178  sq01  14184  crreczi  14187  bernneq  14188  bernneq2  14189  nn0opthlem1  14227  facndiv  14247  faclbnd4lem1  14252  faclbnd6  14258  bcnp1n  14273  bcm1k  14274  bcp1nk  14276  bcn2  14278  bcp1m1  14279  bcpasc  14280  hashgadd  14336  hashfz  14386  hashfzo  14388  hashxplem  14392  hashbclem  14411  hashf1  14416  seqcoll  14423  swrds1  14626  swrdlsw  14627  wrdind  14681  wrd2ind  14682  swrds2  14899  relexpaddg  15012  rei  15115  imi  15116  recan  15296  iserex  15616  isercoll2  15628  serf0  15640  iseraltlem2  15642  iseraltlem3  15643  iseralt  15644  sumrblem  15670  fsumm1  15710  telfsumo  15762  fsumparts  15766  hashiun  15782  binomlem  15791  binom  15792  binom1p  15793  binom11  15794  binom1dif  15795  bcxmas  15797  isumsplit  15802  isum1p  15803  climcndslem1  15811  supcvg  15818  harmonic  15821  arisum  15822  arisum2  15823  trireciplem  15824  geoserg  15828  geolim  15832  geolim2  15833  georeclim  15834  geo2sum  15835  geo2sum2  15836  geoisum1c  15842  0.999...  15843  geoihalfsum  15844  cvgrat  15845  mertenslem1  15846  mertenslem2  15847  mertens  15848  prodf1  15853  prodfclim1  15855  prodrblem  15891  fprodcvg  15892  prodmolem2a  15896  zprod  15899  fprodntriv  15904  prodss  15909  fprodss  15910  fprodsplit  15928  fprodn0f  15953  risefaccl  15977  fallfaccl  15978  risefacfac  15997  binomfallfac  16003  bpolycl  16014  bpolysum  16015  bpolydiflem  16016  fsumkthpow  16018  bpoly2  16019  bpoly3  16020  bpoly4  16021  fsumcube  16022  esum  16042  ege2le3  16052  efsub  16064  efexp  16065  efzval  16066  eftlub  16073  effsumlt  16075  ef4p  16077  tanval3  16098  efi4p  16101  tan0  16115  efival  16116  tanadd  16131  cos2t  16142  cos2tsin  16143  ef01bndlem  16148  cos1bnd  16151  cos2bnd  16152  demoivreALT  16165  eirrlem  16168  rpnnen2lem3  16180  rpnnen2lem11  16188  ruclem12  16205  3dvds  16297  3dvdsdec  16298  3dvds2dec  16299  odd2np1lem  16306  odd2np1  16307  opoe  16329  omoe  16330  opeo  16331  omeo  16332  n2dvdsm1  16335  m1exp1  16342  flodddiv4  16381  bitsfzo  16401  sqgcd  16528  expgcd  16529  nn0seqcvgd  16536  prmind2  16651  hashdvds  16742  phiprmpw  16743  phiprm  16744  eulerthlem2  16749  iserodd  16803  sumhash  16864  fldivp1  16865  prmpwdvds  16872  pockthlem  16873  pockthi  16875  prmreclem4  16887  prmreclem6  16889  4sqlem11  16923  4sqlem19  16931  vdwapun  16942  vdwapid1  16943  vdwlem3  16951  vdwlem5  16953  vdwlem6  16954  vdwlem8  16956  vdwlem9  16957  vdwnnlem2  16964  ramub1lem1  16994  ramub1lem2  16995  ramcl  16997  prmo1  17005  dec5nprm  17034  prmlem0  17073  43prm  17089  83prm  17090  139prm  17091  163prm  17092  317prm  17093  631prm  17094  1259lem2  17099  1259lem3  17100  1259lem4  17101  1259lem5  17102  1259prm  17103  2503lem1  17104  2503lem2  17105  2503lem3  17106  2503prm  17107  4001lem1  17108  4001lem2  17109  4001lem3  17110  4001lem4  17111  4001prm  17112  gsumsgrpccat  18805  mulgnndir  19076  mulgneg2  19081  m1expaddsub  19470  sylow1lem1  19570  sylow2a  19591  efgsval2  19705  efgsrel  19706  efgsres  19710  cncrng  21370  cnfld1  21374  zsssubrg  21402  cnmgpid  21406  zringcyg  21446  mulgrhm2  21455  pzriprng1ALT  21473  cnmsgnsubg  21554  cnmsgnbas  21555  cnmsgngrp  21556  psgninv  21559  evpmodpmf1o  21573  psdmplcl  22125  blcvx  24760  iihalf2  24897  icopnfcnv  24906  iccpnfhmeo  24909  xrhmeo  24910  icccvx  24914  lebnumii  24930  reparphti  24961  pcoass  24988  pcorevlem  24990  pcorev2  24992  pi1xfrcnv  25021  cnstrcvs  25105  cncvs  25109  ncvsm1  25118  pjthlem1  25401  divcncf  25411  ovolunlem1a  25460  ovolunlem1  25461  ovolicc2lem4  25484  uniioombllem3  25549  uniioombllem4  25550  dyadovol  25557  vitalilem4  25575  mbf0  25598  iblcnlem1  25752  itgcnlem  25754  dvid  25882  dvexp  25917  dvexp2  25918  dvexp3  25942  dveflem  25943  dvlipcn  25958  dvcvx  25984  dvfsumle  25985  dvfsumlem1  25990  degltp1le  26035  ply1divex  26099  fta1glem1  26130  plyaddlem1  26175  plymullem1  26176  coeidp  26225  dgrid  26226  dvply1  26247  dvply2g  26248  plyremlem  26267  fta1lem  26270  vieta1lem1  26273  vieta1lem2  26274  qaa  26286  iaa  26288  aalioulem3  26297  geolim3  26302  aaliou3lem2  26306  aaliou3lem7  26312  taylply2  26330  dvradcnv  26383  pserdvlem2  26390  pserdv2  26392  abelthlem1  26393  abelthlem2  26394  abelthlem6  26398  abelthlem7  26400  abelth  26403  reeff1olem  26408  reeff1o  26409  efcvx  26411  sinhalfpilem  26424  eulerid  26435  cos2pi  26437  sincosq3sgn  26461  sincosq4sgn  26462  tangtx  26466  sincos4thpi  26474  sincos6thpi  26477  pigt3  26479  pige3ALT  26481  abssinper  26482  coskpi  26484  coseq1  26486  efeq1  26489  tanregt0  26500  logneg2  26576  logdivlti  26581  logcnlem4  26606  dvlog2lem  26613  dvlog2  26614  advlog  26615  advlogexp  26616  logtayl  26621  logtayl2  26623  logccv  26624  cxpval  26625  1cxp  26633  cxpcl  26635  cxpp1  26641  cxpsqrt  26664  dvsqrt  26703  dvcnsqrt  26705  sqrtcn  26711  cxpaddlelem  26712  root1id  26715  root1cj  26717  logrec  26724  logb1  26730  logbmpt  26749  ang180lem1  26770  ang180lem2  26771  ang180lem3  26772  isosctrlem1  26779  isosctrlem2  26780  1cubrlem  26802  1cubr  26803  mcubic  26808  binom4  26811  dquartlem1  26812  quartlem1  26818  asinlem  26829  asinlem2  26830  asinlem3a  26831  asinlem3  26832  asinf  26833  atandm2  26838  atandm4  26840  atanf  26841  asinneg  26847  efiasin  26849  sinasin  26850  asinsin  26853  asin1  26855  acos1  26856  reasinsin  26857  asinbnd  26860  cosasin  26865  atanneg  26868  atancj  26871  efiatan  26873  atanlogaddlem  26874  atanlogadd  26875  atanlogsublem  26876  atanlogsub  26877  efiatan2  26878  2efiatan  26879  tanatan  26880  cosatan  26882  cosatanne0  26883  atantan  26884  atanbndlem  26886  bndatandm  26890  atans2  26892  dvatan  26896  atantayl  26898  atantayl2  26899  atantayl3  26900  leibpilem2  26902  leibpi  26903  log2cnv  26905  log2tlbnd  26906  log2ublem3  26909  log2ub  26910  birthdaylem2  26913  birthday  26915  efrlim  26930  dfef2  26931  cvxcl  26945  scvxcvx  26946  emcllem2  26957  emcllem4  26959  emcllem7  26962  harmonicbnd4  26971  fsumharmonic  26972  zetacvg  26975  lgamcvg2  27015  lgam1  27024  gam1  27025  wilthlem1  27028  wilthlem2  27029  wilthlem3  27030  basellem2  27042  basellem5  27045  basellem6  27046  basellem7  27047  basellem8  27048  basellem9  27049  0sgm  27104  mule1  27108  ppiprm  27111  ppinprm  27112  chtprm  27113  chtnprm  27114  chpp1  27115  mumullem2  27140  1sgmprm  27159  1sgm2ppw  27160  ppiub  27164  chtublem  27171  chtub  27172  logfaclbnd  27182  logfacbnd3  27183  logfacrlim  27184  logexprlim  27185  mersenne  27187  perfect1  27188  perfectlem1  27189  perfectlem2  27190  perfect  27191  dchrelbasd  27199  dchrmullid  27212  dchrfi  27215  dchrsum2  27228  sumdchr2  27230  bcp1ctr  27239  bposlem8  27251  zabsle1  27256  lgslem1  27257  lgslem2  27258  lgsfcl2  27263  lgsvalmod  27276  lgsneg  27281  lgsdilem  27284  lgsdir2lem1  27285  lgsdir2lem2  27286  lgsdir2lem3  27287  lgsdir2lem5  27289  lgsdir2  27290  lgsdir  27292  lgsdi  27294  lgsne0  27295  lgseisenlem1  27335  lgseisenlem2  27336  lgseisen  27339  lgsquadlem1  27340  lgsquadlem2  27341  lgsquad2lem1  27344  lgsquad2  27346  m1lgs  27348  2lgslem3c  27358  2lgsoddprmlem3c  27372  2lgsoddprmlem3d  27373  2sqlem10  27388  2sqlem11  27389  2sqblem  27391  addsqn2reu  27401  addsqrexnreu  27402  addsqnreup  27403  chtppilimlem2  27434  chebbnd2  27437  chto1lb  27438  rplogsumlem1  27444  rpvmasumlem  27447  dchrmusumlema  27453  dchrmusum2  27454  dchrisum0flblem1  27468  rpvmasum2  27472  mudivsum  27490  mulogsum  27492  vmalogdivsum2  27498  selberg2lem  27510  logdivbnd  27516  pntrmax  27524  pntrsumo1  27525  pntrsumbnd2  27527  pntrlog2bndlem5  27541  pntpbnd1a  27545  pntpbnd2  27547  pntibndlem2  27551  pntlemd  27554  pntlemc  27555  pntlemr  27562  brbtwn2  28971  colinearalglem4  28975  ax5seglem1  28994  ax5seglem2  28995  ax5seglem3  28997  ax5seglem5  28999  ax5seglem7  29001  ax5seglem9  29003  axbtwnid  29005  axpaschlem  29006  axlowdimlem13  29020  axlowdimlem14  29021  axlowdimlem16  29023  axeuclidlem  29028  axcontlem2  29031  axcontlem4  29033  axcontlem7  29036  axcontlem8  29037  crctcshwlkn0lem6  29880  clwwlkf1  30116  clwwlknonex2lem2  30175  ex-fl  30514  ex-ind-dvds  30528  vc2OLD  30636  vc0  30642  vcm  30644  nvm1  30733  nvmtri  30739  nvge0  30741  ipval2lem3  30773  ipidsq  30778  lnoadd  30826  ip1ilem  30894  ip1i  30895  ip2i  30896  ipdirilem  30897  ipasslem1  30899  ipasslem2  30900  ipasslem10  30907  minvecolem2  30943  hvsubid  31094  hv2times  31129  hisubcomi  31172  normlem9  31186  normlem7tALT  31187  norm-ii-i  31205  normsubi  31209  hhssnv  31332  pjhthlem1  31459  h1de2bi  31622  homullid  31868  ho2times  31887  lnop0  32034  lnopaddi  32039  lnophmlem2  32085  lnfn0i  32110  lnfnaddi  32111  hst1h  32295  sto2i  32305  stadd3i  32316  addltmulALT  32514  sgnneg  32903  dpmul4  32970  psgnid  33155  cnmsgn0g  33204  altgnsg  33207  isarchi3  33245  archirngz  33247  1fldgenq  33380  ply1dg3rt0irred  33641  esplyfvaln  33715  ccfldextdgrr  33813  constrsscn  33881  constrabscl  33919  cos9thpiminplylem1  33923  cos9thpiminplylem4  33926  cos9thpiminplylem5  33927  lmatfvlem  33956  qqhval2lem  34122  dya2ub  34411  omssubadd  34441  eulerpartlemgs2  34521  fib5  34546  fib6  34547  ballotlem2  34630  signswch  34702  signlem0  34728  itgexpif  34747  reprlt  34760  breprexp  34774  breprexpnat  34775  hgt750lem2  34793  subfacp1lem5  35363  subfacp1lem6  35364  subfacval2  35366  subfaclim  35367  subfacval3  35368  cvxsconn  35422  resconn  35425  cvmliftlem7  35470  cvmliftlem10  35473  problem4  35847  sinccvglem  35851  sqdivzi  35907  faclimlem1  35922  dnibndlem5  36739  dnibndlem10  36744  ltflcei  37926  sin2h  37928  cos2h  37929  tan2h  37930  poimirlem13  37951  poimirlem16  37954  poimirlem17  37955  poimirlem19  37957  poimirlem20  37958  poimirlem31  37969  mblfinlem2  37976  mblfinlem3  37977  dvtan  37988  itg2addnclem3  37991  dvasin  38022  dvacos  38023  areacirc  38031  fdc  38063  mettrifi  38075  heiborlem4  38132  heiborlem6  38134  60gcd7e1  42441  lcmineqlem1  42465  lcmineqlem8  42472  lcmineqlem9  42473  lcmineqlem10  42474  lcmineqlem12  42476  3exp7  42489  3lexlogpow5ineq1  42490  3lexlogpow5ineq5  42496  aks4d1p1p4  42507  aks4d1p1p7  42510  aks4d1p1  42512  facp2  42579  1p3e4  42694  sn-1ne2  42700  sqdeccom12  42718  235t711  42734  sin2t3rdpi  42782  cos2t3rdpi  42783  re1m1e0m0  42826  ipiiie0  42867  sn-0tie0  42893  fltnltalem  43092  sum9cubes  43102  3cubeslem3l  43115  3cubeslem3r  43116  eldioph2lem1  43189  lzenom  43199  irrapxlem1  43247  rmspecsqrtnq  43331  rmxm1  43359  rmym1  43360  2nn0ind  43370  jm2.24nn  43384  jm2.17a  43385  jm2.17b  43386  jm2.17c  43387  jm2.24  43388  acongeq  43408  jm2.18  43413  jm2.27c  43432  jm3.1lem2  43443  rngunsnply  43594  flcidc  43595  inductionexd  44579  unitadd  44619  hashnzfzclim  44746  ofdivrec  44750  lhe4.4ex1a  44753  expgrowth  44759  dvradcnv2  44771  binomcxplemrat  44774  binomcxplemnotnn0  44780  isosctrlem1ALT  45357  monoord2xrv  45908  dvsinax  46338  dvnprodlem3  46373  itgsin0pilem1  46375  itgsbtaddcnst  46407  stoweidlem13  46438  stoweidlem26  46451  stoweidlem34  46459  stoweidlem38  46463  wallispilem2  46491  wallispilem4  46493  wallispi2lem1  46496  stirlinglem1  46499  stirlinglem5  46503  stirlinglem10  46508  dirkerper  46521  dirkertrigeqlem1  46523  dirkertrigeqlem3  46525  dirkertrigeq  46526  dirkercncflem4  46531  fourierdlem24  46556  sqwvfoura  46653  sqwvfourb  46654  fourierswlem  46655  lambert0  47326  lamberte  47327  cjnpoly  47328  1t10e1p1e11  47749  ceil5half3  47785  modm2nep1  47811  modm1nep2  47813  modm1nem2  47814  fmtnorec3  48002  fmtno5lem4  48010  fmtno5  48011  257prm  48015  fmtno4nprmfac193  48028  m3prm  48046  139prmALT  48050  127prm  48053  m7prm  48054  lighneallem3  48061  proththd  48068  3exp4mod41  48070  41prothprmlem2  48072  perfectALTVlem2  48189  perfectALTV  48190  11t31e341  48199  evengpop3  48265  nnsum4primeseven  48267  nnsum4primesevenALTV  48268  bgoldbtbndlem1  48272  0nodd  48637  altgsumbcALT  48820  exple2lt6  48831  nn0sumshdiglemB  49087  ackval3  49150  ackval3012  49159  line2ylem  49218  onetansqsecsq  50227  cotsqcscsq  50228  5m4e1  50263