Axiom ax-1cn 11168

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

This axiom is referenced by:  0cn  11206  1cnd  11209  1ex  11210  mulrid  11212  mullid  11213  1re  11214  0re  11216  muladd11  11384  peano2cn  11386  mul02lem2  11391  addrid  11394  cnegex2  11396  peano2cnm  11526  0reALT  11557  ine0  11649  mulm1  11655  0lt1  11736  ixi  11843  muleqadd  11858  reccl  11879  recne0  11885  recid  11886  recid2  11887  div1  11903  1div1e1  11904  diveq1  11905  recdiv  11920  divdiv1  11925  divdiv2  11926  recdiv2  11927  conjmul  11931  eqneg  11934  div2neg  11937  recp1lt1  12112  recreclt  12113  recgt0ii  12120  inelr  12202  ofnegsub  12210  peano5nni  12215  nnsscn  12217  nn1m1nn  12233  nn1suc  12234  nnaddcl  12235  nnmulcl  12236  nnne0  12246  nnsub  12256  1m1e0  12284  2cn  12287  3cn  12293  4cn  12297  5cn  12300  6cn  12303  7cn  12306  8cn  12309  9cn  12312  neg1cn  12326  neg1ne0  12328  negneg1e1  12330  1pneg1e0  12331  1m0e1  12333  0p1e1  12334  1p0e1  12336  2m1e1  12338  3m1e2  12340  4m1e3  12341  5m1e4  12342  6m1e5  12343  7m1e6  12344  8m1e7  12345  9m1e8  12346  2p2e4  12347  1p2e3  12355  1p2e3ALT  12356  3p2e5  12363  3p3e6  12364  4p2e6  12365  4p3e7  12366  4p4e8  12367  5p2e7  12368  5p3e8  12369  5p4e9  12370  6p2e8  12371  6p3e9  12372  7p2e9  12373  1t1e1  12374  3t3e9  12379  neg1mulneg1e1  12425  1mhlfehlf  12431  8th4div3  12432  halfpm6th  12433  addltmul  12448  elnn0nn  12514  elz2  12576  zlem1lt  12614  zltlem1  12615  nnaddm1cl  12619  zextlt  12636  zeo  12648  peano5uzi  12651  numsuc  12691  numltc  12703  numsucc  12717  numaddc  12725  6p5lem  12747  5p5e10  12748  6p4e10  12749  7p3e10  12752  8p2e10  12757  10m1e9  12773  4t3lem  12774  7t4e28  12788  9t11e99  12807  decbin2  12818  halfthird  12820  5recm6rec  12821  uzp1  12863  peano2uzr  12887  uzaddcl  12888  rebtwnz  12931  qbtwnre  13178  iccf1o  13473  fz01en  13529  fztp  13557  fzsuc2  13559  fztpval  13563  fseq1m1p1  13576  elfzp1b  13578  fz0to4untppr  13604  predfz  13626  fzoss2  13660  fzval3  13701  fzosplitsnm1  13707  fzo1to4tp  13720  fldiv4p1lem1div2  13800  ceim1l  13812  fldiv  13825  uzrdgxfr  13932  fzen2  13934  nn0ennn  13944  seqm1  13985  seqshft2  13994  monoord2  13999  sermono  14000  seqf1olem1  14007  seqf1olem2  14008  seqz  14016  ser1const  14024  expcl  14045  expclzlem  14049  m1expcl2  14051  expm1t  14056  1exp  14057  mulexpz  14068  expadd  14070  expaddz  14072  expmul  14073  expubnd  14142  sqrecii  14147  neg1sqe1  14160  irec  14165  i4  14168  binom21  14182  sq01  14188  crreczi  14191  bernneq  14192  bernneq2  14193  nn0opthlem1  14228  facndiv  14248  faclbnd4lem1  14253  faclbnd6  14259  bcnp1n  14274  bcm1k  14275  bcp1nk  14277  bcn2  14279  bcp1m1  14280  bcpasc  14281  hashgadd  14337  hashfz  14387  hashfzo  14389  hashxplem  14393  hashbclem  14411  hashf1  14418  seqcoll  14425  swrds1  14616  swrdlsw  14617  wrdind  14672  wrd2ind  14673  swrds2  14891  relexpaddg  15000  rei  15103  imi  15104  recan  15283  iserex  15603  isercoll2  15615  serf0  15627  iseraltlem2  15629  iseraltlem3  15630  iseralt  15631  sumrblem  15657  fsumm1  15697  telfsumo  15748  fsumparts  15752  hashiun  15768  binomlem  15775  binom  15776  binom1p  15777  binom11  15778  binom1dif  15779  bcxmas  15781  isumsplit  15786  isum1p  15787  climcndslem1  15795  supcvg  15802  harmonic  15805  arisum  15806  arisum2  15807  trireciplem  15808  geoserg  15812  geolim  15816  geolim2  15817  georeclim  15818  geo2sum  15819  geo2sum2  15820  geoisum1c  15826  0.999...  15827  geoihalfsum  15828  cvgrat  15829  mertenslem1  15830  mertenslem2  15831  mertens  15832  prodf1  15837  prodfclim1  15839  prodrblem  15873  fprodcvg  15874  prodmolem2a  15878  zprod  15881  fprodntriv  15886  prodss  15891  fprodss  15892  fprodsplit  15910  fprodn0f  15935  risefaccl  15959  fallfaccl  15960  risefacfac  15979  binomfallfac  15985  bpolycl  15996  bpolysum  15997  bpolydiflem  15998  fsumkthpow  16000  bpoly2  16001  bpoly3  16002  bpoly4  16003  fsumcube  16004  esum  16024  ege2le3  16033  efsub  16043  efexp  16044  efzval  16045  eftlub  16052  effsumlt  16054  ef4p  16056  tanval3  16077  efi4p  16080  tan0  16094  efival  16095  tanadd  16110  cos2t  16121  cos2tsin  16122  ef01bndlem  16127  cos1bnd  16130  cos2bnd  16131  demoivreALT  16144  eirrlem  16147  rpnnen2lem3  16159  rpnnen2lem11  16167  ruclem12  16184  3dvds  16274  3dvdsdec  16275  3dvds2dec  16276  odd2np1lem  16283  odd2np1  16284  opoe  16306  omoe  16307  opeo  16308  omeo  16309  n2dvdsm1  16312  m1exp1  16319  flodddiv4  16356  bitsfzo  16376  sqgcd  16502  nn0seqcvgd  16507  prmind2  16622  hashdvds  16708  phiprmpw  16709  phiprm  16710  eulerthlem2  16715  iserodd  16768  sumhash  16829  fldivp1  16830  prmpwdvds  16837  pockthlem  16838  pockthi  16840  prmreclem4  16852  prmreclem6  16854  4sqlem11  16888  4sqlem19  16896  vdwapun  16907  vdwapid1  16908  vdwlem3  16916  vdwlem5  16918  vdwlem6  16919  vdwlem8  16921  vdwlem9  16922  vdwnnlem2  16929  ramub1lem1  16959  ramub1lem2  16960  ramcl  16962  prmo1  16970  dec5nprm  16999  decexp2  17008  prmlem0  17039  43prm  17055  83prm  17056  139prm  17057  163prm  17058  317prm  17059  631prm  17060  1259lem2  17065  1259lem3  17066  1259lem4  17067  1259lem5  17068  1259prm  17069  2503lem1  17070  2503lem2  17071  2503lem3  17072  2503prm  17073  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001lem4  17077  4001prm  17078  gsumsgrpccat  18721  mulgnndir  18983  mulgneg2  18988  m1expaddsub  19366  sylow1lem1  19466  sylow2a  19487  efgsval2  19601  efgsrel  19602  efgsres  19606  cnfld1  20970  zsssubrg  21003  cnmgpid  21007  zringcyg  21039  mulgrhm2  21048  cnmsgnsubg  21130  cnmsgnbas  21131  cnmsgngrp  21132  psgninv  21135  evpmodpmf1o  21149  blcvx  24314  iihalf2  24449  icopnfcnv  24458  iccpnfhmeo  24461  xrhmeo  24462  icccvx  24466  lebnumii  24482  reparphti  24513  pcoass  24540  pcorevlem  24542  pcorev2  24544  pi1xfrcnv  24573  cnstrcvs  24657  cncvs  24661  ncvsm1  24671  pjthlem1  24954  divcncf  24964  ovolunlem1a  25013  ovolunlem1  25014  ovolicc2lem4  25037  uniioombllem3  25102  uniioombllem4  25103  dyadovol  25110  vitalilem4  25128  mbf0  25151  iblcnlem1  25305  itgcnlem  25307  dvid  25435  dvexp  25470  dvexp2  25471  dvexp3  25495  dveflem  25496  dvlipcn  25511  dvcvx  25537  dvfsumle  25538  dvfsumlem1  25543  degltp1le  25591  ply1divex  25654  fta1glem1  25683  plyaddlem1  25727  plymullem1  25728  coeidp  25777  dgrid  25778  dvply1  25797  dvply2g  25798  plyremlem  25817  fta1lem  25820  vieta1lem1  25823  vieta1lem2  25824  qaa  25836  iaa  25838  aalioulem3  25847  geolim3  25852  aaliou3lem2  25856  aaliou3lem7  25862  taylply2  25880  dvradcnv  25933  pserdvlem2  25940  pserdv2  25942  abelthlem1  25943  abelthlem2  25944  abelthlem6  25948  abelthlem7  25950  abelth  25953  reeff1olem  25958  reeff1o  25959  efcvx  25961  sinhalfpilem  25973  eulerid  25984  cos2pi  25986  sincosq3sgn  26010  sincosq4sgn  26011  tangtx  26015  sincos4thpi  26023  sincos6thpi  26025  pigt3  26027  pige3ALT  26029  abssinper  26030  coskpi  26032  coseq1  26034  efeq1  26037  tanregt0  26048  logneg2  26123  logdivlti  26128  logcnlem4  26153  dvlog2lem  26160  dvlog2  26161  advlog  26162  advlogexp  26163  logtayl  26168  logtayl2  26170  logccv  26171  cxpval  26172  1cxp  26180  cxpcl  26182  cxpp1  26188  cxpsqrt  26211  dvsqrt  26250  dvcnsqrt  26252  sqrtcn  26258  cxpaddlelem  26259  root1id  26262  root1cj  26264  logrec  26268  logb1  26274  logbmpt  26293  ang180lem1  26314  ang180lem2  26315  ang180lem3  26316  isosctrlem1  26323  isosctrlem2  26324  1cubrlem  26346  1cubr  26347  mcubic  26352  binom4  26355  dquartlem1  26356  quartlem1  26362  asinlem  26373  asinlem2  26374  asinlem3a  26375  asinlem3  26376  asinf  26377  atandm2  26382  atandm4  26384  atanf  26385  asinneg  26391  efiasin  26393  sinasin  26394  asinsin  26397  asin1  26399  acos1  26400  reasinsin  26401  asinbnd  26404  cosasin  26409  atanneg  26412  atancj  26415  efiatan  26417  atanlogaddlem  26418  atanlogadd  26419  atanlogsublem  26420  atanlogsub  26421  efiatan2  26422  2efiatan  26423  tanatan  26424  cosatan  26426  cosatanne0  26427  atantan  26428  atanbndlem  26430  bndatandm  26434  atans2  26436  dvatan  26440  atantayl  26442  atantayl2  26443  atantayl3  26444  leibpilem2  26446  leibpi  26447  log2cnv  26449  log2tlbnd  26450  log2ublem3  26453  log2ub  26454  birthdaylem2  26457  birthday  26459  efrlim  26474  dfef2  26475  cvxcl  26489  scvxcvx  26490  emcllem2  26501  emcllem4  26503  emcllem7  26506  harmonicbnd4  26515  fsumharmonic  26516  zetacvg  26519  lgamcvg2  26559  lgam1  26568  gam1  26569  wilthlem1  26572  wilthlem2  26573  wilthlem3  26574  basellem2  26586  basellem5  26589  basellem6  26590  basellem7  26591  basellem8  26592  basellem9  26593  0sgm  26648  mule1  26652  ppiprm  26655  ppinprm  26656  chtprm  26657  chtnprm  26658  chpp1  26659  mumullem2  26684  1sgmprm  26702  1sgm2ppw  26703  ppiub  26707  chtublem  26714  chtub  26715  logfaclbnd  26725  logfacbnd3  26726  logfacrlim  26727  logexprlim  26728  mersenne  26730  perfect1  26731  perfectlem1  26732  perfectlem2  26733  perfect  26734  dchrelbasd  26742  dchrmullid  26755  dchrfi  26758  dchrsum2  26771  sumdchr2  26773  bcp1ctr  26782  bposlem8  26794  zabsle1  26799  lgslem1  26800  lgslem2  26801  lgsfcl2  26806  lgsvalmod  26819  lgsneg  26824  lgsdilem  26827  lgsdir2lem1  26828  lgsdir2lem2  26829  lgsdir2lem3  26830  lgsdir2lem5  26832  lgsdir2  26833  lgsdir  26835  lgsdi  26837  lgsne0  26838  lgseisenlem1  26878  lgseisenlem2  26879  lgseisen  26882  lgsquadlem1  26883  lgsquadlem2  26884  lgsquad2lem1  26887  lgsquad2  26889  m1lgs  26891  2lgslem3c  26901  2lgsoddprmlem3c  26915  2lgsoddprmlem3d  26916  2sqlem10  26931  2sqlem11  26932  2sqblem  26934  addsqn2reu  26944  addsqrexnreu  26945  addsqnreup  26946  chtppilimlem2  26977  chebbnd2  26980  chto1lb  26981  rplogsumlem1  26987  rpvmasumlem  26990  dchrmusumlema  26996  dchrmusum2  26997  dchrisum0flblem1  27011  rpvmasum2  27015  mudivsum  27033  mulogsum  27035  vmalogdivsum2  27041  selberg2lem  27053  logdivbnd  27059  pntrmax  27067  pntrsumo1  27068  pntrsumbnd2  27070  pntrlog2bndlem5  27084  pntpbnd1a  27088  pntpbnd2  27090  pntibndlem2  27094  pntlemd  27097  pntlemc  27098  pntlemr  27105  brbtwn2  28194  colinearalglem4  28198  ax5seglem1  28217  ax5seglem2  28218  ax5seglem3  28220  ax5seglem5  28222  ax5seglem7  28224  ax5seglem9  28226  axbtwnid  28228  axpaschlem  28229  axlowdimlem13  28243  axlowdimlem14  28244  axlowdimlem16  28246  axeuclidlem  28251  axcontlem2  28254  axcontlem4  28256  axcontlem7  28259  axcontlem8  28260  crctcshwlkn0lem6  29100  clwwlkf1  29333  clwwlknonex2lem2  29392  ex-fl  29731  ex-ind-dvds  29745  vc2OLD  29852  vc0  29858  vcm  29860  nvm1  29949  nvmtri  29955  nvge0  29957  ipval2lem3  29989  ipidsq  29994  lnoadd  30042  ip1ilem  30110  ip1i  30111  ip2i  30112  ipdirilem  30113  ipasslem1  30115  ipasslem2  30116  ipasslem10  30123  minvecolem2  30159  hvsubid  30310  hv2times  30345  hisubcomi  30388  normlem9  30402  normlem7tALT  30403  norm-ii-i  30421  normsubi  30425  hhssnv  30548  pjhthlem1  30675  h1de2bi  30838  homullid  31084  ho2times  31103  lnop0  31250  lnopaddi  31255  lnophmlem2  31301  lnfn0i  31326  lnfnaddi  31327  hst1h  31511  sto2i  31521  stadd3i  31532  addltmulALT  31730  dpmul4  32111  psgnid  32287  cnmsgn0g  32336  altgnsg  32339  isarchi3  32364  archirngz  32366  1fldgenq  32443  ccfldextdgrr  32777  lmatfvlem  32826  qqhval2lem  32992  dya2ub  33300  omssubadd  33330  eulerpartlemgs2  33410  fib5  33435  fib6  33436  ballotlem2  33518  sgnneg  33570  signswch  33603  signlem0  33629  itgexpif  33649  reprlt  33662  breprexp  33676  breprexpnat  33677  hgt750lem2  33695  subfacp1lem5  34206  subfacp1lem6  34207  subfacval2  34209  subfaclim  34210  subfacval3  34211  cvxsconn  34265  resconn  34268  cvmliftlem7  34313  cvmliftlem10  34316  problem4  34684  sinccvglem  34688  sqdivzi  34728  faclimlem1  34744  gg-reparphti  35203  gg-dvfsumle  35213  gg-cnfld1  35232  dnibndlem5  35406  dnibndlem10  35411  ltflcei  36524  sin2h  36526  cos2h  36527  tan2h  36528  poimirlem13  36549  poimirlem16  36552  poimirlem17  36553  poimirlem19  36555  poimirlem20  36556  poimirlem31  36567  mblfinlem2  36574  mblfinlem3  36575  dvtan  36586  itg2addnclem3  36589  dvasin  36620  dvacos  36621  areacirc  36629  fdc  36661  mettrifi  36673  heiborlem4  36730  heiborlem6  36732  60gcd7e1  40918  lcmineqlem1  40942  lcmineqlem8  40949  lcmineqlem9  40950  lcmineqlem10  40951  lcmineqlem12  40953  3exp7  40966  3lexlogpow5ineq1  40967  3lexlogpow5ineq5  40973  aks4d1p1p4  40984  aks4d1p1p7  40987  aks4d1p1  40989  facp2  41007  fac2xp3  41068  2xp3dxp2ge1d  41070  factwoffsmonot  41071  sn-1ne2  41227  sqdeccom12  41249  235t711  41253  expgcd  41273  re1m1e0m0  41318  ipiiie0  41358  sn-0tie0  41360  fltnltalem  41452  sum9cubes  41462  3cubeslem3l  41472  3cubeslem3r  41473  eldioph2lem1  41546  lzenom  41556  irrapxlem1  41608  rmspecsqrtnq  41692  rmxm1  41721  rmym1  41722  2nn0ind  41732  jm2.24nn  41746  jm2.17a  41747  jm2.17b  41748  jm2.17c  41749  jm2.24  41750  acongeq  41770  jm2.18  41775  jm2.27c  41794  jm3.1lem2  41805  rngunsnply  41963  flcidc  41964  inductionexd  42954  unitadd  42995  hashnzfzclim  43129  ofdivrec  43133  lhe4.4ex1a  43136  expgrowth  43142  dvradcnv2  43154  binomcxplemrat  43157  binomcxplemnotnn0  43163  isosctrlem1ALT  43743  monoord2xrv  44242  dvsinax  44677  dvnprodlem3  44712  itgsin0pilem1  44714  itgsbtaddcnst  44746  stoweidlem13  44777  stoweidlem26  44790  stoweidlem34  44798  stoweidlem38  44802  wallispilem2  44830  wallispilem4  44832  wallispi2lem1  44835  stirlinglem1  44838  stirlinglem5  44842  stirlinglem10  44847  dirkerper  44860  dirkertrigeqlem1  44862  dirkertrigeqlem3  44864  dirkertrigeq  44865  dirkercncflem4  44870  fourierdlem24  44895  sqwvfoura  44992  sqwvfourb  44993  fourierswlem  44994  1t10e1p1e11  46066  fmtnorec3  46264  fmtno5lem4  46272  fmtno5  46273  257prm  46277  fmtno4nprmfac193  46290  m3prm  46308  139prmALT  46312  127prm  46315  m7prm  46316  lighneallem3  46323  proththd  46330  3exp4mod41  46332  41prothprmlem2  46334  perfectALTVlem2  46438  perfectALTV  46439  11t31e341  46448  evengpop3  46514  nnsum4primeseven  46516  nnsum4primesevenALTV  46517  bgoldbtbndlem1  46521  0nodd  46628  pzriprng1ALT  46868  altgsumbcALT  47077  exple2lt6  47088  nn0sumshdiglemB  47354  ackval3  47417  ackval3012  47426  line2ylem  47485  onetansqsecsq  47854  cotsqcscsq  47855  5m4e1  47892