Axiom ax-1cn 11092

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

This axiom is referenced by:  0cn  11132  1cnd  11135  1ex  11136  mulrid  11138  mullid  11139  1re  11140  0re  11142  muladd11  11312  peano2cn  11314  mul02lem2  11319  addrid  11322  cnegex2  11324  peano2cnm  11456  0reALT  11487  ine0  11581  mulm1  11587  0lt1  11668  ixi  11775  muleqadd  11790  reccl  11811  recne0  11817  recid  11818  recid2  11819  diveq1  11834  div1  11839  1div1e1  11840  recdiv  11856  divdiv1  11861  divdiv2  11862  recdiv2  11863  conjmul  11867  eqneg  11870  div2neg  11873  recp1lt1  12049  recreclt  12050  recgt0ii  12057  neg1cn  12139  neg1ne0  12141  negneg1e1  12143  ofnegsub  12152  peano5nni  12172  nnsscn  12174  nn1m1nn  12190  nn1suc  12191  nnaddcl  12192  nnmulcl  12193  nnne0  12206  nnsub  12216  1m1e0  12248  2cn  12251  3cn  12257  4cn  12261  5cn  12264  6cn  12267  7cn  12270  8cn  12273  9cn  12276  1pneg1e0  12290  1m0e1  12292  0p1e1  12293  1p0e1  12295  2m1e1  12297  3m1e2  12299  4m1e3  12300  5m1e4  12301  6m1e5  12302  7m1e6  12303  8m1e7  12304  9m1e8  12305  2p2e4  12306  1p2e3  12314  1p2e3ALT  12315  3p2e5  12322  3p3e6  12323  4p2e6  12324  4p3e7  12325  4p4e8  12326  5p2e7  12327  5p3e8  12328  5p4e9  12329  6p2e8  12330  6p3e9  12331  7p2e9  12332  1t1e1  12333  3t3e9  12338  neg1mulneg1e1  12384  1mhlfehlf  12391  8th4div3  12392  halfthird  12393  halfpm6th  12394  addltmul  12408  elnn0nn  12474  elz2  12537  zlem1lt  12574  zltlem1  12575  nnaddm1cl  12581  zextlt  12598  zeo  12610  peano5uzi  12613  numsuc  12653  numltc  12665  numsucc  12679  numaddc  12687  6p5lem  12709  5p5e10  12710  6p4e10  12711  7p3e10  12714  8p2e10  12719  10m1e9  12735  4t3lem  12736  7t4e28  12750  9t11e99  12769  decbin2  12780  5recm6rec  12782  uzp1  12820  peano2uzr  12848  uzaddcl  12849  rebtwnz  12892  qbtwnre  13146  iccf1o  13444  fz01en  13501  fztp  13529  fzsuc2  13531  fztpval  13535  fseq1m1p1  13548  elfzp1b  13550  predfz  13602  fzoss2  13637  fzval3  13684  fzosplitsnm1  13690  fzo1to4tp  13704  fldiv4p1lem1div2  13789  ceim1l  13801  fldiv  13814  uzrdgxfr  13924  fzen2  13926  nn0ennn  13936  seqm1  13976  seqshft2  13985  monoord2  13990  sermono  13991  seqf1olem1  13998  seqf1olem2  13999  seqz  14007  ser1const  14015  expcl  14036  expclzlem  14040  m1expcl2  14042  expm1t  14047  1exp  14048  mulexpz  14059  expadd  14061  expaddz  14063  expmul  14064  expubnd  14135  sqrecii  14140  neg1sqe1  14153  irec  14158  i4  14161  binom21  14176  sq01  14182  crreczi  14185  bernneq  14186  bernneq2  14187  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  14409  hashf1  14414  seqcoll  14421  swrds1  14624  swrdlsw  14625  wrdind  14679  wrd2ind  14680  swrds2  14897  relexpaddg  15010  rei  15113  imi  15114  recan  15294  iserex  15614  isercoll2  15626  serf0  15638  iseraltlem2  15640  iseraltlem3  15641  iseralt  15642  sumrblem  15668  fsumm1  15708  telfsumo  15760  fsumparts  15764  hashiun  15780  binomlem  15789  binom  15790  binom1p  15791  binom11  15792  binom1dif  15793  bcxmas  15795  isumsplit  15800  isum1p  15801  climcndslem1  15809  supcvg  15816  harmonic  15819  arisum  15820  arisum2  15821  trireciplem  15822  geoserg  15826  geolim  15830  geolim2  15831  georeclim  15832  geo2sum  15833  geo2sum2  15834  geoisum1c  15840  0.999...  15841  geoihalfsum  15842  cvgrat  15843  mertenslem1  15844  mertenslem2  15845  mertens  15846  prodf1  15851  prodfclim1  15853  prodrblem  15889  fprodcvg  15890  prodmolem2a  15894  zprod  15897  fprodntriv  15902  prodss  15907  fprodss  15908  fprodsplit  15926  fprodn0f  15951  risefaccl  15975  fallfaccl  15976  risefacfac  15995  binomfallfac  16001  bpolycl  16012  bpolysum  16013  bpolydiflem  16014  fsumkthpow  16016  bpoly2  16017  bpoly3  16018  bpoly4  16019  fsumcube  16020  esum  16040  ege2le3  16050  efsub  16062  efexp  16063  efzval  16064  eftlub  16071  effsumlt  16073  ef4p  16075  tanval3  16096  efi4p  16099  tan0  16113  efival  16114  tanadd  16129  cos2t  16140  cos2tsin  16141  ef01bndlem  16146  cos1bnd  16149  cos2bnd  16150  demoivreALT  16163  eirrlem  16166  rpnnen2lem3  16178  rpnnen2lem11  16186  ruclem12  16203  3dvds  16295  3dvdsdec  16296  3dvds2dec  16297  odd2np1lem  16304  odd2np1  16305  opoe  16327  omoe  16328  opeo  16329  omeo  16330  n2dvdsm1  16333  m1exp1  16340  flodddiv4  16379  bitsfzo  16399  sqgcd  16526  expgcd  16527  nn0seqcvgd  16534  prmind2  16649  hashdvds  16740  phiprmpw  16741  phiprm  16742  eulerthlem2  16747  iserodd  16801  sumhash  16862  fldivp1  16863  prmpwdvds  16870  pockthlem  16871  pockthi  16873  prmreclem4  16885  prmreclem6  16887  4sqlem11  16921  4sqlem19  16929  vdwapun  16940  vdwapid1  16941  vdwlem3  16949  vdwlem5  16951  vdwlem6  16952  vdwlem8  16954  vdwlem9  16955  vdwnnlem2  16962  ramub1lem1  16992  ramub1lem2  16993  ramcl  16995  prmo1  17003  dec5nprm  17032  prmlem0  17071  43prm  17087  83prm  17088  139prm  17089  163prm  17090  317prm  17091  631prm  17092  1259lem2  17097  1259lem3  17098  1259lem4  17099  1259lem5  17100  1259prm  17101  2503lem1  17102  2503lem2  17103  2503lem3  17104  2503prm  17105  4001lem1  17106  4001lem2  17107  4001lem3  17108  4001lem4  17109  4001prm  17110  gsumsgrpccat  18803  mulgnndir  19074  mulgneg2  19079  m1expaddsub  19467  sylow1lem1  19567  sylow2a  19588  efgsval2  19702  efgsrel  19703  efgsres  19707  cncrng  21371  cnfld1  21375  zsssubrg  21403  cnmgpid  21407  zringcyg  21447  mulgrhm2  21456  pzriprng1ALT  21474  cnmsgnsubg  21555  cnmsgnbas  21556  cnmsgngrp  21557  psgninv  21560  evpmodpmf1o  21574  psdmplcl  22153  blcvx  24784  iihalf2  24921  icopnfcnv  24930  iccpnfhmeo  24933  xrhmeo  24934  icccvx  24938  lebnumii  24954  reparphti  24985  pcoass  25012  pcorevlem  25014  pcorev2  25016  pi1xfrcnv  25045  cnstrcvs  25129  cncvs  25133  ncvsm1  25142  pjthlem1  25425  divcncf  25435  ovolunlem1a  25484  ovolunlem1  25485  ovolicc2lem4  25508  uniioombllem3  25573  uniioombllem4  25574  dyadovol  25581  vitalilem4  25599  mbf0  25622  iblcnlem1  25776  itgcnlem  25778  dvid  25906  dvexp  25941  dvexp2  25942  dvexp3  25966  dveflem  25967  dvlipcn  25982  dvcvx  26008  dvfsumle  26009  dvfsumlem1  26014  degltp1le  26059  ply1divex  26123  fta1glem1  26154  plyaddlem1  26199  plymullem1  26200  coeidp  26249  dgrid  26250  dvply1  26271  dvply2g  26272  plyremlem  26291  fta1lem  26294  vieta1lem1  26297  vieta1lem2  26298  qaa  26310  iaa  26312  aalioulem3  26321  geolim3  26326  aaliou3lem2  26330  aaliou3lem7  26336  taylply2  26354  dvradcnv  26407  pserdvlem2  26414  pserdv2  26416  abelthlem1  26417  abelthlem2  26418  abelthlem6  26422  abelthlem7  26424  abelth  26427  reeff1olem  26432  reeff1o  26433  efcvx  26435  sinhalfpilem  26448  eulerid  26459  cos2pi  26461  sincosq3sgn  26485  sincosq4sgn  26486  tangtx  26490  sincos4thpi  26498  sincos6thpi  26501  pigt3  26503  pige3ALT  26505  abssinper  26506  coskpi  26508  coseq1  26510  efeq1  26513  tanregt0  26524  logneg2  26600  logdivlti  26605  logcnlem4  26630  dvlog2lem  26637  dvlog2  26638  advlog  26639  advlogexp  26640  logtayl  26645  logtayl2  26647  logccv  26648  cxpval  26649  1cxp  26657  cxpcl  26659  cxpp1  26665  cxpsqrt  26688  dvsqrt  26727  dvcnsqrt  26729  sqrtcn  26735  cxpaddlelem  26736  root1id  26739  root1cj  26741  logrec  26748  logb1  26754  logbmpt  26773  ang180lem1  26794  ang180lem2  26795  ang180lem3  26796  isosctrlem1  26803  isosctrlem2  26804  1cubrlem  26826  1cubr  26827  mcubic  26832  binom4  26835  dquartlem1  26836  quartlem1  26842  asinlem  26853  asinlem2  26854  asinlem3a  26855  asinlem3  26856  asinf  26857  atandm2  26862  atandm4  26864  atanf  26865  asinneg  26871  efiasin  26873  sinasin  26874  asinsin  26877  asin1  26879  acos1  26880  reasinsin  26881  asinbnd  26884  cosasin  26889  atanneg  26892  atancj  26895  efiatan  26897  atanlogaddlem  26898  atanlogadd  26899  atanlogsublem  26900  atanlogsub  26901  efiatan2  26902  2efiatan  26903  tanatan  26904  cosatan  26906  cosatanne0  26907  atantan  26908  atanbndlem  26910  bndatandm  26914  atans2  26916  dvatan  26920  atantayl  26922  atantayl2  26923  atantayl3  26924  leibpilem2  26926  leibpi  26927  log2cnv  26929  log2tlbnd  26930  log2ublem3  26933  log2ub  26934  birthdaylem2  26937  birthday  26939  efrlim  26954  dfef2  26955  cvxcl  26969  scvxcvx  26970  emcllem2  26981  emcllem4  26983  emcllem7  26986  harmonicbnd4  26995  fsumharmonic  26996  zetacvg  26999  lgamcvg2  27039  lgam1  27048  gam1  27049  wilthlem1  27052  wilthlem2  27053  wilthlem3  27054  basellem2  27066  basellem5  27069  basellem6  27070  basellem7  27071  basellem8  27072  basellem9  27073  0sgm  27128  mule1  27132  ppiprm  27135  ppinprm  27136  chtprm  27137  chtnprm  27138  chpp1  27139  mumullem2  27164  1sgmprm  27183  1sgm2ppw  27184  ppiub  27188  chtublem  27195  chtub  27196  logfaclbnd  27206  logfacbnd3  27207  logfacrlim  27208  logexprlim  27209  mersenne  27211  perfect1  27212  perfectlem1  27213  perfectlem2  27214  perfect  27215  dchrelbasd  27223  dchrmullid  27236  dchrfi  27239  dchrsum2  27252  sumdchr2  27254  bcp1ctr  27263  bposlem8  27275  zabsle1  27280  lgslem1  27281  lgslem2  27282  lgsfcl2  27287  lgsvalmod  27300  lgsneg  27305  lgsdilem  27308  lgsdir2lem1  27309  lgsdir2lem2  27310  lgsdir2lem3  27311  lgsdir2lem5  27313  lgsdir2  27314  lgsdir  27316  lgsdi  27318  lgsne0  27319  lgseisenlem1  27359  lgseisenlem2  27360  lgseisen  27363  lgsquadlem1  27364  lgsquadlem2  27365  lgsquad2lem1  27368  lgsquad2  27370  m1lgs  27372  2lgslem3c  27382  2lgsoddprmlem3c  27396  2lgsoddprmlem3d  27397  2sqlem10  27412  2sqlem11  27413  2sqblem  27415  addsqn2reu  27425  addsqrexnreu  27426  addsqnreup  27427  chtppilimlem2  27458  chebbnd2  27461  chto1lb  27462  rplogsumlem1  27468  rpvmasumlem  27471  dchrmusumlema  27477  dchrmusum2  27478  dchrisum0flblem1  27492  rpvmasum2  27496  mudivsum  27514  mulogsum  27516  vmalogdivsum2  27522  selberg2lem  27534  logdivbnd  27540  pntrmax  27548  pntrsumo1  27549  pntrsumbnd2  27551  pntrlog2bndlem5  27565  pntpbnd1a  27569  pntpbnd2  27571  pntibndlem2  27575  pntlemd  27578  pntlemc  27579  pntlemr  27586  brbtwn2  28994  colinearalglem4  28998  ax5seglem1  29017  ax5seglem2  29018  ax5seglem3  29020  ax5seglem5  29022  ax5seglem7  29024  ax5seglem9  29026  axbtwnid  29028  axpaschlem  29029  axlowdimlem13  29043  axlowdimlem14  29044  axlowdimlem16  29046  axeuclidlem  29051  axcontlem2  29054  axcontlem4  29056  axcontlem7  29059  axcontlem8  29060  crctcshwlkn0lem6  29903  clwwlkf1  30139  clwwlknonex2lem2  30198  ex-fl  30537  ex-ind-dvds  30551  vc2OLD  30659  vc0  30665  vcm  30667  nvm1  30756  nvmtri  30762  nvge0  30764  ipval2lem3  30796  ipidsq  30801  lnoadd  30849  ip1ilem  30917  ip1i  30918  ip2i  30919  ipdirilem  30920  ipasslem1  30922  ipasslem2  30923  ipasslem10  30930  minvecolem2  30966  hvsubid  31117  hv2times  31152  hisubcomi  31195  normlem9  31209  normlem7tALT  31210  norm-ii-i  31228  normsubi  31232  hhssnv  31355  pjhthlem1  31482  h1de2bi  31645  homullid  31891  ho2times  31910  lnop0  32057  lnopaddi  32062  lnophmlem2  32108  lnfn0i  32133  lnfnaddi  32134  hst1h  32318  sto2i  32328  stadd3i  32339  addltmulALT  32537  sgnneg  32927  dpmul4  32994  psgnid  33180  cnmsgn0g  33229  altgnsg  33232  isarchi3  33270  archirngz  33272  1fldgenq  33408  ply1dg3rt0irred  33677  esplyfvaln  33768  ccfldextdgrr  33866  constrsscn  33934  constrabscl  33972  cos9thpiminplylem1  33976  cos9thpiminplylem4  33979  cos9thpiminplylem5  33980  lmatfvlem  34009  qqhval2lem  34175  dya2ub  34464  omssubadd  34494  eulerpartlemgs2  34574  fib5  34599  fib6  34600  ballotlem2  34683  signswch  34755  signlem0  34781  itgexpif  34800  reprlt  34813  breprexp  34827  breprexpnat  34828  hgt750lem2  34846  subfacp1lem5  35425  subfacp1lem6  35426  subfacval2  35428  subfaclim  35429  subfacval3  35430  cvxsconn  35484  resconn  35487  cvmliftlem7  35532  cvmliftlem10  35535  problem4  35909  sinccvglem  35913  sqdivzi  35969  faclimlem1  35984  dnibndlem5  36801  dnibndlem10  36806  ltflcei  37988  sin2h  37990  cos2h  37991  tan2h  37992  poimirlem13  38013  poimirlem16  38016  poimirlem17  38017  poimirlem19  38019  poimirlem20  38020  poimirlem31  38031  mblfinlem2  38038  mblfinlem3  38039  dvtan  38050  itg2addnclem3  38053  dvasin  38084  dvacos  38085  areacirc  38093  fdc  38125  mettrifi  38137  heiborlem4  38194  heiborlem6  38196  60gcd7e1  42503  lcmineqlem1  42527  lcmineqlem8  42534  lcmineqlem9  42535  lcmineqlem10  42536  lcmineqlem12  42538  3exp7  42551  3lexlogpow5ineq1  42552  3lexlogpow5ineq5  42558  aks4d1p1p4  42569  aks4d1p1p7  42572  aks4d1p1  42574  facp2  42641  1p3e4  42755  sn-1ne2  42761  sqdeccom12  42779  235t711  42795  sin2t3rdpi  42843  cos2t3rdpi  42844  re1m1e0m0  42887  ipiiie0  42928  sn-0tie0  42954  fltnltalem  43125  sum9cubes  43135  3cubeslem3l  43148  3cubeslem3r  43149  eldioph2lem1  43222  lzenom  43232  irrapxlem1  43280  rmspecsqrtnq  43364  rmxm1  43392  rmym1  43393  2nn0ind  43403  jm2.24nn  43417  jm2.17a  43418  jm2.17b  43419  jm2.17c  43420  jm2.24  43421  acongeq  43441  jm2.18  43446  jm2.27c  43465  jm3.1lem2  43476  rngunsnply  43627  flcidc  43628  inductionexd  44612  unitadd  44652  hashnzfzclim  44779  ofdivrec  44783  lhe4.4ex1a  44786  expgrowth  44792  dvradcnv2  44804  binomcxplemrat  44807  binomcxplemnotnn0  44813  isosctrlem1ALT  45390  monoord2xrv  45938  dvsinax  46368  dvnprodlem3  46403  itgsin0pilem1  46405  itgsbtaddcnst  46437  stoweidlem13  46468  stoweidlem26  46481  stoweidlem34  46489  stoweidlem38  46493  wallispilem2  46521  wallispilem4  46523  wallispi2lem1  46526  stirlinglem1  46529  stirlinglem5  46533  stirlinglem10  46538  dirkerper  46551  dirkertrigeqlem1  46553  dirkertrigeqlem3  46555  dirkertrigeq  46556  dirkercncflem4  46561  fourierdlem24  46586  sqwvfoura  46683  sqwvfourb  46684  fourierswlem  46685  cos5t  47354  goldratmolem2  47361  lambert0  47362  lamberte  47363  cjnpoly  47364  1t10e1p1e11  47785  ceil5half3  47821  modm2nep1  47847  modm1nep2  47849  modm1nem2  47850  fmtnorec3  48038  fmtno5lem4  48046  fmtno5  48047  257prm  48051  fmtno4nprmfac193  48064  m3prm  48082  139prmALT  48086  127prm  48089  m7prm  48090  lighneallem3  48097  proththd  48104  3exp4mod41  48106  41prothprmlem2  48108  perfectALTVlem2  48225  perfectALTV  48226  11t31e341  48235  evengpop3  48301  nnsum4primeseven  48303  nnsum4primesevenALTV  48304  bgoldbtbndlem1  48308  0nodd  48673  altgsumbcALT  48856  exple2lt6  48867  nn0sumshdiglemB  49123  ackval3  49186  ackval3012  49195  line2ylem  49254  onetansqsecsq  50263  cotsqcscsq  50264  5m4e1  50299