Axiom ax-1cn 11210

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

This axiom is referenced by:  0cn  11250  1cnd  11253  1ex  11254  mulrid  11256  mullid  11257  1re  11258  0re  11260  muladd11  11428  peano2cn  11430  mul02lem2  11435  addrid  11438  cnegex2  11440  peano2cnm  11572  0reALT  11603  ine0  11695  mulm1  11701  0lt1  11782  ixi  11889  muleqadd  11904  reccl  11926  recne0  11932  recid  11933  recid2  11934  diveq1  11949  div1  11954  1div1e1  11955  recdiv  11970  divdiv1  11975  divdiv2  11976  recdiv2  11977  conjmul  11981  eqneg  11984  div2neg  11987  recp1lt1  12163  recreclt  12164  recgt0ii  12171  inelr  12253  ofnegsub  12261  peano5nni  12266  nnsscn  12268  nn1m1nn  12284  nn1suc  12285  nnaddcl  12286  nnmulcl  12287  nnne0  12297  nnsub  12307  1m1e0  12335  2cn  12338  3cn  12344  4cn  12348  5cn  12351  6cn  12354  7cn  12357  8cn  12360  9cn  12363  neg1cn  12377  neg1ne0  12379  negneg1e1  12381  1pneg1e0  12382  1m0e1  12384  0p1e1  12385  1p0e1  12387  2m1e1  12389  3m1e2  12391  4m1e3  12392  5m1e4  12393  6m1e5  12394  7m1e6  12395  8m1e7  12396  9m1e8  12397  2p2e4  12398  1p2e3  12406  1p2e3ALT  12407  3p2e5  12414  3p3e6  12415  4p2e6  12416  4p3e7  12417  4p4e8  12418  5p2e7  12419  5p3e8  12420  5p4e9  12421  6p2e8  12422  6p3e9  12423  7p2e9  12424  1t1e1  12425  3t3e9  12430  neg1mulneg1e1  12476  1mhlfehlf  12482  8th4div3  12483  halfpm6th  12484  addltmul  12499  elnn0nn  12565  elz2  12628  zlem1lt  12666  zltlem1  12667  nnaddm1cl  12672  zextlt  12689  zeo  12701  peano5uzi  12704  numsuc  12744  numltc  12756  numsucc  12770  numaddc  12778  6p5lem  12800  5p5e10  12801  6p4e10  12802  7p3e10  12805  8p2e10  12810  10m1e9  12826  4t3lem  12827  7t4e28  12841  9t11e99  12860  decbin2  12871  halfthird  12873  5recm6rec  12874  uzp1  12916  peano2uzr  12942  uzaddcl  12943  rebtwnz  12986  qbtwnre  13237  iccf1o  13532  fz01en  13588  fztp  13616  fzsuc2  13618  fztpval  13622  fseq1m1p1  13635  elfzp1b  13637  predfz  13689  fzoss2  13723  fzval3  13769  fzosplitsnm1  13775  fzo1to4tp  13789  fldiv4p1lem1div2  13871  ceim1l  13883  fldiv  13896  uzrdgxfr  14004  fzen2  14006  nn0ennn  14016  seqm1  14056  seqshft2  14065  monoord2  14070  sermono  14071  seqf1olem1  14078  seqf1olem2  14079  seqz  14087  ser1const  14095  expcl  14116  expclzlem  14120  m1expcl2  14122  expm1t  14127  1exp  14128  mulexpz  14139  expadd  14141  expaddz  14143  expmul  14144  expubnd  14213  sqrecii  14218  neg1sqe1  14231  irec  14236  i4  14239  binom21  14254  sq01  14260  crreczi  14263  bernneq  14264  bernneq2  14265  nn0opthlem1  14303  facndiv  14323  faclbnd4lem1  14328  faclbnd6  14334  bcnp1n  14349  bcm1k  14350  bcp1nk  14352  bcn2  14354  bcp1m1  14355  bcpasc  14356  hashgadd  14412  hashfz  14462  hashfzo  14464  hashxplem  14468  hashbclem  14487  hashf1  14492  seqcoll  14499  swrds1  14700  swrdlsw  14701  wrdind  14756  wrd2ind  14757  swrds2  14975  relexpaddg  15088  rei  15191  imi  15192  recan  15371  iserex  15689  isercoll2  15701  serf0  15713  iseraltlem2  15715  iseraltlem3  15716  iseralt  15717  sumrblem  15743  fsumm1  15783  telfsumo  15834  fsumparts  15838  hashiun  15854  binomlem  15861  binom  15862  binom1p  15863  binom11  15864  binom1dif  15865  bcxmas  15867  isumsplit  15872  isum1p  15873  climcndslem1  15881  supcvg  15888  harmonic  15891  arisum  15892  arisum2  15893  trireciplem  15894  geoserg  15898  geolim  15902  geolim2  15903  georeclim  15904  geo2sum  15905  geo2sum2  15906  geoisum1c  15912  0.999...  15913  geoihalfsum  15914  cvgrat  15915  mertenslem1  15916  mertenslem2  15917  mertens  15918  prodf1  15923  prodfclim1  15925  prodrblem  15961  fprodcvg  15962  prodmolem2a  15966  zprod  15969  fprodntriv  15974  prodss  15979  fprodss  15980  fprodsplit  15998  fprodn0f  16023  risefaccl  16047  fallfaccl  16048  risefacfac  16067  binomfallfac  16073  bpolycl  16084  bpolysum  16085  bpolydiflem  16086  fsumkthpow  16088  bpoly2  16089  bpoly3  16090  bpoly4  16091  fsumcube  16092  esum  16112  ege2le3  16122  efsub  16132  efexp  16133  efzval  16134  eftlub  16141  effsumlt  16143  ef4p  16145  tanval3  16166  efi4p  16169  tan0  16183  efival  16184  tanadd  16199  cos2t  16210  cos2tsin  16211  ef01bndlem  16216  cos1bnd  16219  cos2bnd  16220  demoivreALT  16233  eirrlem  16236  rpnnen2lem3  16248  rpnnen2lem11  16256  ruclem12  16273  3dvds  16364  3dvdsdec  16365  3dvds2dec  16366  odd2np1lem  16373  odd2np1  16374  opoe  16396  omoe  16397  opeo  16398  omeo  16399  n2dvdsm1  16402  m1exp1  16409  flodddiv4  16448  bitsfzo  16468  sqgcd  16595  expgcd  16596  nn0seqcvgd  16603  prmind2  16718  hashdvds  16808  phiprmpw  16809  phiprm  16810  eulerthlem2  16815  iserodd  16868  sumhash  16929  fldivp1  16930  prmpwdvds  16937  pockthlem  16938  pockthi  16940  prmreclem4  16952  prmreclem6  16954  4sqlem11  16988  4sqlem19  16996  vdwapun  17007  vdwapid1  17008  vdwlem3  17016  vdwlem5  17018  vdwlem6  17019  vdwlem8  17021  vdwlem9  17022  vdwnnlem2  17029  ramub1lem1  17059  ramub1lem2  17060  ramcl  17062  prmo1  17070  dec5nprm  17099  decexp2  17108  prmlem0  17139  43prm  17155  83prm  17156  139prm  17157  163prm  17158  317prm  17159  631prm  17160  1259lem2  17165  1259lem3  17166  1259lem4  17167  1259lem5  17168  1259prm  17169  2503lem1  17170  2503lem2  17171  2503lem3  17172  2503prm  17173  4001lem1  17174  4001lem2  17175  4001lem3  17176  4001lem4  17177  4001prm  17178  gsumsgrpccat  18865  mulgnndir  19133  mulgneg2  19138  m1expaddsub  19530  sylow1lem1  19630  sylow2a  19651  efgsval2  19765  efgsrel  19766  efgsres  19770  cncrng  21418  cnfld1  21423  cnfld1OLD  21424  zsssubrg  21460  cnmgpid  21464  zringcyg  21497  mulgrhm2  21506  pzriprng1ALT  21524  cnmsgnsubg  21612  cnmsgnbas  21613  cnmsgngrp  21614  psgninv  21617  evpmodpmf1o  21631  psdmplcl  22183  blcvx  24833  iihalf2  24974  icopnfcnv  24986  iccpnfhmeo  24989  xrhmeo  24990  icccvx  24994  lebnumii  25011  reparphti  25042  reparphtiOLD  25043  pcoass  25070  pcorevlem  25072  pcorev2  25074  pi1xfrcnv  25103  cnstrcvs  25187  cncvs  25191  ncvsm1  25201  pjthlem1  25484  divcncf  25495  ovolunlem1a  25544  ovolunlem1  25545  ovolicc2lem4  25568  uniioombllem3  25633  uniioombllem4  25634  dyadovol  25641  vitalilem4  25659  mbf0  25682  iblcnlem1  25837  itgcnlem  25839  dvid  25967  dvexp  26005  dvexp2  26006  dvexp3  26030  dveflem  26031  dvlipcn  26047  dvcvx  26073  dvfsumle  26074  dvfsumleOLD  26075  dvfsumlem1  26080  degltp1le  26126  ply1divex  26190  fta1glem1  26221  plyaddlem1  26266  plymullem1  26267  coeidp  26317  dgrid  26318  dvply1  26339  dvply2g  26340  dvply2gOLD  26341  plyremlem  26360  fta1lem  26363  vieta1lem1  26366  vieta1lem2  26367  qaa  26379  iaa  26381  aalioulem3  26390  geolim3  26395  aaliou3lem2  26399  aaliou3lem7  26405  taylply2  26423  taylply2OLD  26424  dvradcnv  26478  pserdvlem2  26486  pserdv2  26488  abelthlem1  26489  abelthlem2  26490  abelthlem6  26494  abelthlem7  26496  abelth  26499  reeff1olem  26504  reeff1o  26505  efcvx  26507  sinhalfpilem  26519  eulerid  26530  cos2pi  26532  sincosq3sgn  26556  sincosq4sgn  26557  tangtx  26561  sincos4thpi  26569  sincos6thpi  26572  pigt3  26574  pige3ALT  26576  abssinper  26577  coskpi  26579  coseq1  26581  efeq1  26584  tanregt0  26595  logneg2  26671  logdivlti  26676  logcnlem4  26701  dvlog2lem  26708  dvlog2  26709  advlog  26710  advlogexp  26711  logtayl  26716  logtayl2  26718  logccv  26719  cxpval  26720  1cxp  26728  cxpcl  26730  cxpp1  26736  cxpsqrt  26759  dvsqrt  26798  dvcnsqrt  26800  sqrtcn  26807  cxpaddlelem  26808  root1id  26811  root1cj  26813  logrec  26820  logb1  26826  logbmpt  26845  ang180lem1  26866  ang180lem2  26867  ang180lem3  26868  isosctrlem1  26875  isosctrlem2  26876  1cubrlem  26898  1cubr  26899  mcubic  26904  binom4  26907  dquartlem1  26908  quartlem1  26914  asinlem  26925  asinlem2  26926  asinlem3a  26927  asinlem3  26928  asinf  26929  atandm2  26934  atandm4  26936  atanf  26937  asinneg  26943  efiasin  26945  sinasin  26946  asinsin  26949  asin1  26951  acos1  26952  reasinsin  26953  asinbnd  26956  cosasin  26961  atanneg  26964  atancj  26967  efiatan  26969  atanlogaddlem  26970  atanlogadd  26971  atanlogsublem  26972  atanlogsub  26973  efiatan2  26974  2efiatan  26975  tanatan  26976  cosatan  26978  cosatanne0  26979  atantan  26980  atanbndlem  26982  bndatandm  26986  atans2  26988  dvatan  26992  atantayl  26994  atantayl2  26995  atantayl3  26996  leibpilem2  26998  leibpi  26999  log2cnv  27001  log2tlbnd  27002  log2ublem3  27005  log2ub  27006  birthdaylem2  27009  birthday  27011  efrlim  27026  efrlimOLD  27027  dfef2  27028  cvxcl  27042  scvxcvx  27043  emcllem2  27054  emcllem4  27056  emcllem7  27059  harmonicbnd4  27068  fsumharmonic  27069  zetacvg  27072  lgamcvg2  27112  lgam1  27121  gam1  27122  wilthlem1  27125  wilthlem2  27126  wilthlem3  27127  basellem2  27139  basellem5  27142  basellem6  27143  basellem7  27144  basellem8  27145  basellem9  27146  0sgm  27201  mule1  27205  ppiprm  27208  ppinprm  27209  chtprm  27210  chtnprm  27211  chpp1  27212  mumullem2  27237  1sgmprm  27257  1sgm2ppw  27258  ppiub  27262  chtublem  27269  chtub  27270  logfaclbnd  27280  logfacbnd3  27281  logfacrlim  27282  logexprlim  27283  mersenne  27285  perfect1  27286  perfectlem1  27287  perfectlem2  27288  perfect  27289  dchrelbasd  27297  dchrmullid  27310  dchrfi  27313  dchrsum2  27326  sumdchr2  27328  bcp1ctr  27337  bposlem8  27349  zabsle1  27354  lgslem1  27355  lgslem2  27356  lgsfcl2  27361  lgsvalmod  27374  lgsneg  27379  lgsdilem  27382  lgsdir2lem1  27383  lgsdir2lem2  27384  lgsdir2lem3  27385  lgsdir2lem5  27387  lgsdir2  27388  lgsdir  27390  lgsdi  27392  lgsne0  27393  lgseisenlem1  27433  lgseisenlem2  27434  lgseisen  27437  lgsquadlem1  27438  lgsquadlem2  27439  lgsquad2lem1  27442  lgsquad2  27444  m1lgs  27446  2lgslem3c  27456  2lgsoddprmlem3c  27470  2lgsoddprmlem3d  27471  2sqlem10  27486  2sqlem11  27487  2sqblem  27489  addsqn2reu  27499  addsqrexnreu  27500  addsqnreup  27501  chtppilimlem2  27532  chebbnd2  27535  chto1lb  27536  rplogsumlem1  27542  rpvmasumlem  27545  dchrmusumlema  27551  dchrmusum2  27552  dchrisum0flblem1  27566  rpvmasum2  27570  mudivsum  27588  mulogsum  27590  vmalogdivsum2  27596  selberg2lem  27608  logdivbnd  27614  pntrmax  27622  pntrsumo1  27623  pntrsumbnd2  27625  pntrlog2bndlem5  27639  pntpbnd1a  27643  pntpbnd2  27645  pntibndlem2  27649  pntlemd  27652  pntlemc  27653  pntlemr  27660  brbtwn2  28934  colinearalglem4  28938  ax5seglem1  28957  ax5seglem2  28958  ax5seglem3  28960  ax5seglem5  28962  ax5seglem7  28964  ax5seglem9  28966  axbtwnid  28968  axpaschlem  28969  axlowdimlem13  28983  axlowdimlem14  28984  axlowdimlem16  28986  axeuclidlem  28991  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  axcontlem8  29000  crctcshwlkn0lem6  29844  clwwlkf1  30077  clwwlknonex2lem2  30136  ex-fl  30475  ex-ind-dvds  30489  vc2OLD  30596  vc0  30602  vcm  30604  nvm1  30693  nvmtri  30699  nvge0  30701  ipval2lem3  30733  ipidsq  30738  lnoadd  30786  ip1ilem  30854  ip1i  30855  ip2i  30856  ipdirilem  30857  ipasslem1  30859  ipasslem2  30860  ipasslem10  30867  minvecolem2  30903  hvsubid  31054  hv2times  31089  hisubcomi  31132  normlem9  31146  normlem7tALT  31147  norm-ii-i  31165  normsubi  31169  hhssnv  31292  pjhthlem1  31419  h1de2bi  31582  homullid  31828  ho2times  31847  lnop0  31994  lnopaddi  31999  lnophmlem2  32045  lnfn0i  32070  lnfnaddi  32071  hst1h  32255  sto2i  32265  stadd3i  32276  addltmulALT  32474  dpmul4  32880  psgnid  33099  cnmsgn0g  33148  altgnsg  33151  isarchi3  33176  archirngz  33178  1fldgenq  33303  ply1dg3rt0irred  33586  ccfldextdgrr  33696  constrsscn  33744  lmatfvlem  33775  qqhval2lem  33943  dya2ub  34251  omssubadd  34281  eulerpartlemgs2  34361  fib5  34386  fib6  34387  ballotlem2  34469  sgnneg  34521  signswch  34554  signlem0  34580  itgexpif  34599  reprlt  34612  breprexp  34626  breprexpnat  34627  hgt750lem2  34645  subfacp1lem5  35168  subfacp1lem6  35169  subfacval2  35171  subfaclim  35172  subfacval3  35173  cvxsconn  35227  resconn  35230  cvmliftlem7  35275  cvmliftlem10  35278  problem4  35652  sinccvglem  35656  sqdivzi  35707  faclimlem1  35722  dnibndlem5  36464  dnibndlem10  36469  ltflcei  37594  sin2h  37596  cos2h  37597  tan2h  37598  poimirlem13  37619  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem31  37637  mblfinlem2  37644  mblfinlem3  37645  dvtan  37656  itg2addnclem3  37659  dvasin  37690  dvacos  37691  areacirc  37699  fdc  37731  mettrifi  37743  heiborlem4  37800  heiborlem6  37802  60gcd7e1  41986  lcmineqlem1  42010  lcmineqlem8  42017  lcmineqlem9  42018  lcmineqlem10  42019  lcmineqlem12  42021  3exp7  42034  3lexlogpow5ineq1  42035  3lexlogpow5ineq5  42041  aks4d1p1p4  42052  aks4d1p1p7  42055  aks4d1p1  42057  facp2  42124  fac2xp3  42220  2xp3dxp2ge1d  42222  factwoffsmonot  42223  sn-1ne2  42278  sqdeccom12  42302  235t711  42317  re1m1e0m0  42403  ipiiie0  42443  sn-0tie0  42445  fltnltalem  42648  sum9cubes  42658  3cubeslem3l  42673  3cubeslem3r  42674  eldioph2lem1  42747  lzenom  42757  irrapxlem1  42809  rmspecsqrtnq  42893  rmxm1  42922  rmym1  42923  2nn0ind  42933  jm2.24nn  42947  jm2.17a  42948  jm2.17b  42949  jm2.17c  42950  jm2.24  42951  acongeq  42971  jm2.18  42976  jm2.27c  42995  jm3.1lem2  43006  rngunsnply  43157  flcidc  43158  inductionexd  44144  unitadd  44184  hashnzfzclim  44317  ofdivrec  44321  lhe4.4ex1a  44324  expgrowth  44330  dvradcnv2  44342  binomcxplemrat  44345  binomcxplemnotnn0  44351  isosctrlem1ALT  44931  monoord2xrv  45433  dvsinax  45868  dvnprodlem3  45903  itgsin0pilem1  45905  itgsbtaddcnst  45937  stoweidlem13  45968  stoweidlem26  45981  stoweidlem34  45989  stoweidlem38  45993  wallispilem2  46021  wallispilem4  46023  wallispi2lem1  46026  stirlinglem1  46029  stirlinglem5  46033  stirlinglem10  46038  dirkerper  46051  dirkertrigeqlem1  46053  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkercncflem4  46061  fourierdlem24  46086  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  1t10e1p1e11  47259  ceil5half3  47279  fmtnorec3  47472  fmtno5lem4  47480  fmtno5  47481  257prm  47485  fmtno4nprmfac193  47498  m3prm  47516  139prmALT  47520  127prm  47523  m7prm  47524  lighneallem3  47531  proththd  47538  3exp4mod41  47540  41prothprmlem2  47542  perfectALTVlem2  47646  perfectALTV  47647  11t31e341  47656  evengpop3  47722  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  bgoldbtbndlem1  47729  0nodd  48013  altgsumbcALT  48197  exple2lt6  48208  nn0sumshdiglemB  48469  ackval3  48532  ackval3012  48541  line2ylem  48600  onetansqsecsq  48991  cotsqcscsq  48992  5m4e1  49027