Axiom ax-1cn 11213

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

This axiom is referenced by:  0cn  11253  1cnd  11256  1ex  11257  mulrid  11259  mullid  11260  1re  11261  0re  11263  muladd11  11431  peano2cn  11433  mul02lem2  11438  addrid  11441  cnegex2  11443  peano2cnm  11575  0reALT  11606  ine0  11698  mulm1  11704  0lt1  11785  ixi  11892  muleqadd  11907  reccl  11929  recne0  11935  recid  11936  recid2  11937  diveq1  11952  div1  11957  1div1e1  11958  recdiv  11973  divdiv1  11978  divdiv2  11979  recdiv2  11980  conjmul  11984  eqneg  11987  div2neg  11990  recp1lt1  12166  recreclt  12167  recgt0ii  12174  inelr  12256  ofnegsub  12264  peano5nni  12269  nnsscn  12271  nn1m1nn  12287  nn1suc  12288  nnaddcl  12289  nnmulcl  12290  nnne0  12300  nnsub  12310  1m1e0  12338  2cn  12341  3cn  12347  4cn  12351  5cn  12354  6cn  12357  7cn  12360  8cn  12363  9cn  12366  neg1cn  12380  neg1ne0  12382  negneg1e1  12384  1pneg1e0  12385  1m0e1  12387  0p1e1  12388  1p0e1  12390  2m1e1  12392  3m1e2  12394  4m1e3  12395  5m1e4  12396  6m1e5  12397  7m1e6  12398  8m1e7  12399  9m1e8  12400  2p2e4  12401  1p2e3  12409  1p2e3ALT  12410  3p2e5  12417  3p3e6  12418  4p2e6  12419  4p3e7  12420  4p4e8  12421  5p2e7  12422  5p3e8  12423  5p4e9  12424  6p2e8  12425  6p3e9  12426  7p2e9  12427  1t1e1  12428  3t3e9  12433  neg1mulneg1e1  12479  1mhlfehlf  12485  8th4div3  12486  halfpm6th  12487  addltmul  12502  elnn0nn  12568  elz2  12631  zlem1lt  12669  zltlem1  12670  nnaddm1cl  12675  zextlt  12692  zeo  12704  peano5uzi  12707  numsuc  12747  numltc  12759  numsucc  12773  numaddc  12781  6p5lem  12803  5p5e10  12804  6p4e10  12805  7p3e10  12808  8p2e10  12813  10m1e9  12829  4t3lem  12830  7t4e28  12844  9t11e99  12863  decbin2  12874  halfthird  12876  5recm6rec  12877  uzp1  12919  peano2uzr  12945  uzaddcl  12946  rebtwnz  12989  qbtwnre  13241  iccf1o  13536  fz01en  13592  fztp  13620  fzsuc2  13622  fztpval  13626  fseq1m1p1  13639  elfzp1b  13641  predfz  13693  fzoss2  13727  fzval3  13773  fzosplitsnm1  13779  fzo1to4tp  13793  fldiv4p1lem1div2  13875  ceim1l  13887  fldiv  13900  uzrdgxfr  14008  fzen2  14010  nn0ennn  14020  seqm1  14060  seqshft2  14069  monoord2  14074  sermono  14075  seqf1olem1  14082  seqf1olem2  14083  seqz  14091  ser1const  14099  expcl  14120  expclzlem  14124  m1expcl2  14126  expm1t  14131  1exp  14132  mulexpz  14143  expadd  14145  expaddz  14147  expmul  14148  expubnd  14217  sqrecii  14222  neg1sqe1  14235  irec  14240  i4  14243  binom21  14258  sq01  14264  crreczi  14267  bernneq  14268  bernneq2  14269  nn0opthlem1  14307  facndiv  14327  faclbnd4lem1  14332  faclbnd6  14338  bcnp1n  14353  bcm1k  14354  bcp1nk  14356  bcn2  14358  bcp1m1  14359  bcpasc  14360  hashgadd  14416  hashfz  14466  hashfzo  14468  hashxplem  14472  hashbclem  14491  hashf1  14496  seqcoll  14503  swrds1  14704  swrdlsw  14705  wrdind  14760  wrd2ind  14761  swrds2  14979  relexpaddg  15092  rei  15195  imi  15196  recan  15375  iserex  15693  isercoll2  15705  serf0  15717  iseraltlem2  15719  iseraltlem3  15720  iseralt  15721  sumrblem  15747  fsumm1  15787  telfsumo  15838  fsumparts  15842  hashiun  15858  binomlem  15865  binom  15866  binom1p  15867  binom11  15868  binom1dif  15869  bcxmas  15871  isumsplit  15876  isum1p  15877  climcndslem1  15885  supcvg  15892  harmonic  15895  arisum  15896  arisum2  15897  trireciplem  15898  geoserg  15902  geolim  15906  geolim2  15907  georeclim  15908  geo2sum  15909  geo2sum2  15910  geoisum1c  15916  0.999...  15917  geoihalfsum  15918  cvgrat  15919  mertenslem1  15920  mertenslem2  15921  mertens  15922  prodf1  15927  prodfclim1  15929  prodrblem  15965  fprodcvg  15966  prodmolem2a  15970  zprod  15973  fprodntriv  15978  prodss  15983  fprodss  15984  fprodsplit  16002  fprodn0f  16027  risefaccl  16051  fallfaccl  16052  risefacfac  16071  binomfallfac  16077  bpolycl  16088  bpolysum  16089  bpolydiflem  16090  fsumkthpow  16092  bpoly2  16093  bpoly3  16094  bpoly4  16095  fsumcube  16096  esum  16116  ege2le3  16126  efsub  16136  efexp  16137  efzval  16138  eftlub  16145  effsumlt  16147  ef4p  16149  tanval3  16170  efi4p  16173  tan0  16187  efival  16188  tanadd  16203  cos2t  16214  cos2tsin  16215  ef01bndlem  16220  cos1bnd  16223  cos2bnd  16224  demoivreALT  16237  eirrlem  16240  rpnnen2lem3  16252  rpnnen2lem11  16260  ruclem12  16277  3dvds  16368  3dvdsdec  16369  3dvds2dec  16370  odd2np1lem  16377  odd2np1  16378  opoe  16400  omoe  16401  opeo  16402  omeo  16403  n2dvdsm1  16406  m1exp1  16413  flodddiv4  16452  bitsfzo  16472  sqgcd  16599  expgcd  16600  nn0seqcvgd  16607  prmind2  16722  hashdvds  16812  phiprmpw  16813  phiprm  16814  eulerthlem2  16819  iserodd  16873  sumhash  16934  fldivp1  16935  prmpwdvds  16942  pockthlem  16943  pockthi  16945  prmreclem4  16957  prmreclem6  16959  4sqlem11  16993  4sqlem19  17001  vdwapun  17012  vdwapid1  17013  vdwlem3  17021  vdwlem5  17023  vdwlem6  17024  vdwlem8  17026  vdwlem9  17027  vdwnnlem2  17034  ramub1lem1  17064  ramub1lem2  17065  ramcl  17067  prmo1  17075  dec5nprm  17104  prmlem0  17143  43prm  17159  83prm  17160  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  1259prm  17173  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  4001prm  17182  gsumsgrpccat  18853  mulgnndir  19121  mulgneg2  19126  m1expaddsub  19516  sylow1lem1  19616  sylow2a  19637  efgsval2  19751  efgsrel  19752  efgsres  19756  cncrng  21401  cnfld1  21406  cnfld1OLD  21407  zsssubrg  21443  cnmgpid  21447  zringcyg  21480  mulgrhm2  21489  pzriprng1ALT  21507  cnmsgnsubg  21595  cnmsgnbas  21596  cnmsgngrp  21597  psgninv  21600  evpmodpmf1o  21614  psdmplcl  22166  blcvx  24819  iihalf2  24961  icopnfcnv  24973  iccpnfhmeo  24976  xrhmeo  24977  icccvx  24981  lebnumii  24998  reparphti  25029  reparphtiOLD  25030  pcoass  25057  pcorevlem  25059  pcorev2  25061  pi1xfrcnv  25090  cnstrcvs  25174  cncvs  25178  ncvsm1  25188  pjthlem1  25471  divcncf  25482  ovolunlem1a  25531  ovolunlem1  25532  ovolicc2lem4  25555  uniioombllem3  25620  uniioombllem4  25621  dyadovol  25628  vitalilem4  25646  mbf0  25669  iblcnlem1  25823  itgcnlem  25825  dvid  25953  dvexp  25991  dvexp2  25992  dvexp3  26016  dveflem  26017  dvlipcn  26033  dvcvx  26059  dvfsumle  26060  dvfsumleOLD  26061  dvfsumlem1  26066  degltp1le  26112  ply1divex  26176  fta1glem1  26207  plyaddlem1  26252  plymullem1  26253  coeidp  26303  dgrid  26304  dvply1  26325  dvply2g  26326  dvply2gOLD  26327  plyremlem  26346  fta1lem  26349  vieta1lem1  26352  vieta1lem2  26353  qaa  26365  iaa  26367  aalioulem3  26376  geolim3  26381  aaliou3lem2  26385  aaliou3lem7  26391  taylply2  26409  taylply2OLD  26410  dvradcnv  26464  pserdvlem2  26472  pserdv2  26474  abelthlem1  26475  abelthlem2  26476  abelthlem6  26480  abelthlem7  26482  abelth  26485  reeff1olem  26490  reeff1o  26491  efcvx  26493  sinhalfpilem  26505  eulerid  26516  cos2pi  26518  sincosq3sgn  26542  sincosq4sgn  26543  tangtx  26547  sincos4thpi  26555  sincos6thpi  26558  pigt3  26560  pige3ALT  26562  abssinper  26563  coskpi  26565  coseq1  26567  efeq1  26570  tanregt0  26581  logneg2  26657  logdivlti  26662  logcnlem4  26687  dvlog2lem  26694  dvlog2  26695  advlog  26696  advlogexp  26697  logtayl  26702  logtayl2  26704  logccv  26705  cxpval  26706  1cxp  26714  cxpcl  26716  cxpp1  26722  cxpsqrt  26745  dvsqrt  26784  dvcnsqrt  26786  sqrtcn  26793  cxpaddlelem  26794  root1id  26797  root1cj  26799  logrec  26806  logb1  26812  logbmpt  26831  ang180lem1  26852  ang180lem2  26853  ang180lem3  26854  isosctrlem1  26861  isosctrlem2  26862  1cubrlem  26884  1cubr  26885  mcubic  26890  binom4  26893  dquartlem1  26894  quartlem1  26900  asinlem  26911  asinlem2  26912  asinlem3a  26913  asinlem3  26914  asinf  26915  atandm2  26920  atandm4  26922  atanf  26923  asinneg  26929  efiasin  26931  sinasin  26932  asinsin  26935  asin1  26937  acos1  26938  reasinsin  26939  asinbnd  26942  cosasin  26947  atanneg  26950  atancj  26953  efiatan  26955  atanlogaddlem  26956  atanlogadd  26957  atanlogsublem  26958  atanlogsub  26959  efiatan2  26960  2efiatan  26961  tanatan  26962  cosatan  26964  cosatanne0  26965  atantan  26966  atanbndlem  26968  bndatandm  26972  atans2  26974  dvatan  26978  atantayl  26980  atantayl2  26981  atantayl3  26982  leibpilem2  26984  leibpi  26985  log2cnv  26987  log2tlbnd  26988  log2ublem3  26991  log2ub  26992  birthdaylem2  26995  birthday  26997  efrlim  27012  efrlimOLD  27013  dfef2  27014  cvxcl  27028  scvxcvx  27029  emcllem2  27040  emcllem4  27042  emcllem7  27045  harmonicbnd4  27054  fsumharmonic  27055  zetacvg  27058  lgamcvg2  27098  lgam1  27107  gam1  27108  wilthlem1  27111  wilthlem2  27112  wilthlem3  27113  basellem2  27125  basellem5  27128  basellem6  27129  basellem7  27130  basellem8  27131  basellem9  27132  0sgm  27187  mule1  27191  ppiprm  27194  ppinprm  27195  chtprm  27196  chtnprm  27197  chpp1  27198  mumullem2  27223  1sgmprm  27243  1sgm2ppw  27244  ppiub  27248  chtublem  27255  chtub  27256  logfaclbnd  27266  logfacbnd3  27267  logfacrlim  27268  logexprlim  27269  mersenne  27271  perfect1  27272  perfectlem1  27273  perfectlem2  27274  perfect  27275  dchrelbasd  27283  dchrmullid  27296  dchrfi  27299  dchrsum2  27312  sumdchr2  27314  bcp1ctr  27323  bposlem8  27335  zabsle1  27340  lgslem1  27341  lgslem2  27342  lgsfcl2  27347  lgsvalmod  27360  lgsneg  27365  lgsdilem  27368  lgsdir2lem1  27369  lgsdir2lem2  27370  lgsdir2lem3  27371  lgsdir2lem5  27373  lgsdir2  27374  lgsdir  27376  lgsdi  27378  lgsne0  27379  lgseisenlem1  27419  lgseisenlem2  27420  lgseisen  27423  lgsquadlem1  27424  lgsquadlem2  27425  lgsquad2lem1  27428  lgsquad2  27430  m1lgs  27432  2lgslem3c  27442  2lgsoddprmlem3c  27456  2lgsoddprmlem3d  27457  2sqlem10  27472  2sqlem11  27473  2sqblem  27475  addsqn2reu  27485  addsqrexnreu  27486  addsqnreup  27487  chtppilimlem2  27518  chebbnd2  27521  chto1lb  27522  rplogsumlem1  27528  rpvmasumlem  27531  dchrmusumlema  27537  dchrmusum2  27538  dchrisum0flblem1  27552  rpvmasum2  27556  mudivsum  27574  mulogsum  27576  vmalogdivsum2  27582  selberg2lem  27594  logdivbnd  27600  pntrmax  27608  pntrsumo1  27609  pntrsumbnd2  27611  pntrlog2bndlem5  27625  pntpbnd1a  27629  pntpbnd2  27631  pntibndlem2  27635  pntlemd  27638  pntlemc  27639  pntlemr  27646  brbtwn2  28920  colinearalglem4  28924  ax5seglem1  28943  ax5seglem2  28944  ax5seglem3  28946  ax5seglem5  28948  ax5seglem7  28950  ax5seglem9  28952  axbtwnid  28954  axpaschlem  28955  axlowdimlem13  28969  axlowdimlem14  28970  axlowdimlem16  28972  axeuclidlem  28977  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  axcontlem8  28986  crctcshwlkn0lem6  29835  clwwlkf1  30068  clwwlknonex2lem2  30127  ex-fl  30466  ex-ind-dvds  30480  vc2OLD  30587  vc0  30593  vcm  30595  nvm1  30684  nvmtri  30690  nvge0  30692  ipval2lem3  30724  ipidsq  30729  lnoadd  30777  ip1ilem  30845  ip1i  30846  ip2i  30847  ipdirilem  30848  ipasslem1  30850  ipasslem2  30851  ipasslem10  30858  minvecolem2  30894  hvsubid  31045  hv2times  31080  hisubcomi  31123  normlem9  31137  normlem7tALT  31138  norm-ii-i  31156  normsubi  31160  hhssnv  31283  pjhthlem1  31410  h1de2bi  31573  homullid  31819  ho2times  31838  lnop0  31985  lnopaddi  31990  lnophmlem2  32036  lnfn0i  32061  lnfnaddi  32062  hst1h  32246  sto2i  32256  stadd3i  32267  addltmulALT  32465  dpmul4  32896  psgnid  33117  cnmsgn0g  33166  altgnsg  33169  isarchi3  33194  archirngz  33196  1fldgenq  33324  ply1dg3rt0irred  33607  ccfldextdgrr  33722  constrsscn  33781  lmatfvlem  33814  qqhval2lem  33982  dya2ub  34272  omssubadd  34302  eulerpartlemgs2  34382  fib5  34407  fib6  34408  ballotlem2  34491  sgnneg  34543  signswch  34576  signlem0  34602  itgexpif  34621  reprlt  34634  breprexp  34648  breprexpnat  34649  hgt750lem2  34667  subfacp1lem5  35189  subfacp1lem6  35190  subfacval2  35192  subfaclim  35193  subfacval3  35194  cvxsconn  35248  resconn  35251  cvmliftlem7  35296  cvmliftlem10  35299  problem4  35673  sinccvglem  35677  sqdivzi  35728  faclimlem1  35743  dnibndlem5  36483  dnibndlem10  36488  ltflcei  37615  sin2h  37617  cos2h  37618  tan2h  37619  poimirlem13  37640  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem31  37658  mblfinlem2  37665  mblfinlem3  37666  dvtan  37677  itg2addnclem3  37680  dvasin  37711  dvacos  37712  areacirc  37720  fdc  37752  mettrifi  37764  heiborlem4  37821  heiborlem6  37823  60gcd7e1  42006  lcmineqlem1  42030  lcmineqlem8  42037  lcmineqlem9  42038  lcmineqlem10  42039  lcmineqlem12  42041  3exp7  42054  3lexlogpow5ineq1  42055  3lexlogpow5ineq5  42061  aks4d1p1p4  42072  aks4d1p1p7  42075  aks4d1p1  42077  facp2  42144  fac2xp3  42240  2xp3dxp2ge1d  42242  factwoffsmonot  42243  sn-1ne2  42300  sqdeccom12  42324  235t711  42339  re1m1e0m0  42427  ipiiie0  42467  sn-0tie0  42469  fltnltalem  42672  sum9cubes  42682  3cubeslem3l  42697  3cubeslem3r  42698  eldioph2lem1  42771  lzenom  42781  irrapxlem1  42833  rmspecsqrtnq  42917  rmxm1  42946  rmym1  42947  2nn0ind  42957  jm2.24nn  42971  jm2.17a  42972  jm2.17b  42973  jm2.17c  42974  jm2.24  42975  acongeq  42995  jm2.18  43000  jm2.27c  43019  jm3.1lem2  43030  rngunsnply  43181  flcidc  43182  inductionexd  44168  unitadd  44208  hashnzfzclim  44341  ofdivrec  44345  lhe4.4ex1a  44348  expgrowth  44354  dvradcnv2  44366  binomcxplemrat  44369  binomcxplemnotnn0  44375  isosctrlem1ALT  44954  monoord2xrv  45494  dvsinax  45928  dvnprodlem3  45963  itgsin0pilem1  45965  itgsbtaddcnst  45997  stoweidlem13  46028  stoweidlem26  46041  stoweidlem34  46049  stoweidlem38  46053  wallispilem2  46081  wallispilem4  46083  wallispi2lem1  46086  stirlinglem1  46089  stirlinglem5  46093  stirlinglem10  46098  dirkerper  46111  dirkertrigeqlem1  46113  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkercncflem4  46121  fourierdlem24  46146  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  1t10e1p1e11  47322  ceil5half3  47342  fmtnorec3  47535  fmtno5lem4  47543  fmtno5  47544  257prm  47548  fmtno4nprmfac193  47561  m3prm  47579  139prmALT  47583  127prm  47586  m7prm  47587  lighneallem3  47594  proththd  47601  3exp4mod41  47603  41prothprmlem2  47605  perfectALTVlem2  47709  perfectALTV  47710  11t31e341  47719  evengpop3  47785  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  bgoldbtbndlem1  47792  0nodd  48086  altgsumbcALT  48269  exple2lt6  48280  nn0sumshdiglemB  48541  ackval3  48604  ackval3012  48613  line2ylem  48672  onetansqsecsq  49280  cotsqcscsq  49281  5m4e1  49316