Axiom ax-1cn 11133

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

This axiom is referenced by:  0cn  11173  1cnd  11176  1ex  11177  mulrid  11179  mullid  11180  1re  11181  0re  11183  muladd11  11351  peano2cn  11353  mul02lem2  11358  addrid  11361  cnegex2  11363  peano2cnm  11495  0reALT  11526  ine0  11620  mulm1  11626  0lt1  11707  ixi  11814  muleqadd  11829  reccl  11851  recne0  11857  recid  11858  recid2  11859  diveq1  11874  div1  11879  1div1e1  11880  recdiv  11895  divdiv1  11900  divdiv2  11901  recdiv2  11902  conjmul  11906  eqneg  11909  div2neg  11912  recp1lt1  12088  recreclt  12089  recgt0ii  12096  neg1cn  12178  neg1ne0  12180  negneg1e1  12182  ofnegsub  12191  peano5nni  12196  nnsscn  12198  nn1m1nn  12214  nn1suc  12215  nnaddcl  12216  nnmulcl  12217  nnne0  12227  nnsub  12237  1m1e0  12265  2cn  12268  3cn  12274  4cn  12278  5cn  12281  6cn  12284  7cn  12287  8cn  12290  9cn  12293  1pneg1e0  12307  1m0e1  12309  0p1e1  12310  1p0e1  12312  2m1e1  12314  3m1e2  12316  4m1e3  12317  5m1e4  12318  6m1e5  12319  7m1e6  12320  8m1e7  12321  9m1e8  12322  2p2e4  12323  1p2e3  12331  1p2e3ALT  12332  3p2e5  12339  3p3e6  12340  4p2e6  12341  4p3e7  12342  4p4e8  12343  5p2e7  12344  5p3e8  12345  5p4e9  12346  6p2e8  12347  6p3e9  12348  7p2e9  12349  1t1e1  12350  3t3e9  12355  neg1mulneg1e1  12401  1mhlfehlf  12408  8th4div3  12409  halfthird  12410  halfpm6th  12411  addltmul  12425  elnn0nn  12491  elz2  12554  zlem1lt  12592  zltlem1  12593  nnaddm1cl  12598  zextlt  12615  zeo  12627  peano5uzi  12630  numsuc  12670  numltc  12682  numsucc  12696  numaddc  12704  6p5lem  12726  5p5e10  12727  6p4e10  12728  7p3e10  12731  8p2e10  12736  10m1e9  12752  4t3lem  12753  7t4e28  12767  9t11e99  12786  decbin2  12797  5recm6rec  12799  uzp1  12841  peano2uzr  12869  uzaddcl  12870  rebtwnz  12913  qbtwnre  13166  iccf1o  13464  fz01en  13520  fztp  13548  fzsuc2  13550  fztpval  13554  fseq1m1p1  13567  elfzp1b  13569  predfz  13621  fzoss2  13655  fzval3  13702  fzosplitsnm1  13708  fzo1to4tp  13722  fldiv4p1lem1div2  13804  ceim1l  13816  fldiv  13829  uzrdgxfr  13939  fzen2  13941  nn0ennn  13951  seqm1  13991  seqshft2  14000  monoord2  14005  sermono  14006  seqf1olem1  14013  seqf1olem2  14014  seqz  14022  ser1const  14030  expcl  14051  expclzlem  14055  m1expcl2  14057  expm1t  14062  1exp  14063  mulexpz  14074  expadd  14076  expaddz  14078  expmul  14079  expubnd  14150  sqrecii  14155  neg1sqe1  14168  irec  14173  i4  14176  binom21  14191  sq01  14197  crreczi  14200  bernneq  14201  bernneq2  14202  nn0opthlem1  14240  facndiv  14260  faclbnd4lem1  14265  faclbnd6  14271  bcnp1n  14286  bcm1k  14287  bcp1nk  14289  bcn2  14291  bcp1m1  14292  bcpasc  14293  hashgadd  14349  hashfz  14399  hashfzo  14401  hashxplem  14405  hashbclem  14424  hashf1  14429  seqcoll  14436  swrds1  14638  swrdlsw  14639  wrdind  14694  wrd2ind  14695  swrds2  14913  relexpaddg  15026  rei  15129  imi  15130  recan  15310  iserex  15630  isercoll2  15642  serf0  15654  iseraltlem2  15656  iseraltlem3  15657  iseralt  15658  sumrblem  15684  fsumm1  15724  telfsumo  15775  fsumparts  15779  hashiun  15795  binomlem  15802  binom  15803  binom1p  15804  binom11  15805  binom1dif  15806  bcxmas  15808  isumsplit  15813  isum1p  15814  climcndslem1  15822  supcvg  15829  harmonic  15832  arisum  15833  arisum2  15834  trireciplem  15835  geoserg  15839  geolim  15843  geolim2  15844  georeclim  15845  geo2sum  15846  geo2sum2  15847  geoisum1c  15853  0.999...  15854  geoihalfsum  15855  cvgrat  15856  mertenslem1  15857  mertenslem2  15858  mertens  15859  prodf1  15864  prodfclim1  15866  prodrblem  15902  fprodcvg  15903  prodmolem2a  15907  zprod  15910  fprodntriv  15915  prodss  15920  fprodss  15921  fprodsplit  15939  fprodn0f  15964  risefaccl  15988  fallfaccl  15989  risefacfac  16008  binomfallfac  16014  bpolycl  16025  bpolysum  16026  bpolydiflem  16027  fsumkthpow  16029  bpoly2  16030  bpoly3  16031  bpoly4  16032  fsumcube  16033  esum  16053  ege2le3  16063  efsub  16075  efexp  16076  efzval  16077  eftlub  16084  effsumlt  16086  ef4p  16088  tanval3  16109  efi4p  16112  tan0  16126  efival  16127  tanadd  16142  cos2t  16153  cos2tsin  16154  ef01bndlem  16159  cos1bnd  16162  cos2bnd  16163  demoivreALT  16176  eirrlem  16179  rpnnen2lem3  16191  rpnnen2lem11  16199  ruclem12  16216  3dvds  16308  3dvdsdec  16309  3dvds2dec  16310  odd2np1lem  16317  odd2np1  16318  opoe  16340  omoe  16341  opeo  16342  omeo  16343  n2dvdsm1  16346  m1exp1  16353  flodddiv4  16392  bitsfzo  16412  sqgcd  16539  expgcd  16540  nn0seqcvgd  16547  prmind2  16662  hashdvds  16752  phiprmpw  16753  phiprm  16754  eulerthlem2  16759  iserodd  16813  sumhash  16874  fldivp1  16875  prmpwdvds  16882  pockthlem  16883  pockthi  16885  prmreclem4  16897  prmreclem6  16899  4sqlem11  16933  4sqlem19  16941  vdwapun  16952  vdwapid1  16953  vdwlem3  16961  vdwlem5  16963  vdwlem6  16964  vdwlem8  16966  vdwlem9  16967  vdwnnlem2  16974  ramub1lem1  17004  ramub1lem2  17005  ramcl  17007  prmo1  17015  dec5nprm  17044  prmlem0  17083  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  gsumsgrpccat  18774  mulgnndir  19042  mulgneg2  19047  m1expaddsub  19435  sylow1lem1  19535  sylow2a  19556  efgsval2  19670  efgsrel  19671  efgsres  19675  cncrng  21307  cnfld1  21312  cnfld1OLD  21313  zsssubrg  21349  cnmgpid  21353  zringcyg  21386  mulgrhm2  21395  pzriprng1ALT  21413  cnmsgnsubg  21493  cnmsgnbas  21494  cnmsgngrp  21495  psgninv  21498  evpmodpmf1o  21512  psdmplcl  22056  blcvx  24693  iihalf2  24835  icopnfcnv  24847  iccpnfhmeo  24850  xrhmeo  24851  icccvx  24855  lebnumii  24872  reparphti  24903  reparphtiOLD  24904  pcoass  24931  pcorevlem  24933  pcorev2  24935  pi1xfrcnv  24964  cnstrcvs  25048  cncvs  25052  ncvsm1  25061  pjthlem1  25344  divcncf  25355  ovolunlem1a  25404  ovolunlem1  25405  ovolicc2lem4  25428  uniioombllem3  25493  uniioombllem4  25494  dyadovol  25501  vitalilem4  25519  mbf0  25542  iblcnlem1  25696  itgcnlem  25698  dvid  25826  dvexp  25864  dvexp2  25865  dvexp3  25889  dveflem  25890  dvlipcn  25906  dvcvx  25932  dvfsumle  25933  dvfsumleOLD  25934  dvfsumlem1  25939  degltp1le  25985  ply1divex  26049  fta1glem1  26080  plyaddlem1  26125  plymullem1  26126  coeidp  26176  dgrid  26177  dvply1  26198  dvply2g  26199  dvply2gOLD  26200  plyremlem  26219  fta1lem  26222  vieta1lem1  26225  vieta1lem2  26226  qaa  26238  iaa  26240  aalioulem3  26249  geolim3  26254  aaliou3lem2  26258  aaliou3lem7  26264  taylply2  26282  taylply2OLD  26283  dvradcnv  26337  pserdvlem2  26345  pserdv2  26347  abelthlem1  26348  abelthlem2  26349  abelthlem6  26353  abelthlem7  26355  abelth  26358  reeff1olem  26363  reeff1o  26364  efcvx  26366  sinhalfpilem  26379  eulerid  26390  cos2pi  26392  sincosq3sgn  26416  sincosq4sgn  26417  tangtx  26421  sincos4thpi  26429  sincos6thpi  26432  pigt3  26434  pige3ALT  26436  abssinper  26437  coskpi  26439  coseq1  26441  efeq1  26444  tanregt0  26455  logneg2  26531  logdivlti  26536  logcnlem4  26561  dvlog2lem  26568  dvlog2  26569  advlog  26570  advlogexp  26571  logtayl  26576  logtayl2  26578  logccv  26579  cxpval  26580  1cxp  26588  cxpcl  26590  cxpp1  26596  cxpsqrt  26619  dvsqrt  26658  dvcnsqrt  26660  sqrtcn  26667  cxpaddlelem  26668  root1id  26671  root1cj  26673  logrec  26680  logb1  26686  logbmpt  26705  ang180lem1  26726  ang180lem2  26727  ang180lem3  26728  isosctrlem1  26735  isosctrlem2  26736  1cubrlem  26758  1cubr  26759  mcubic  26764  binom4  26767  dquartlem1  26768  quartlem1  26774  asinlem  26785  asinlem2  26786  asinlem3a  26787  asinlem3  26788  asinf  26789  atandm2  26794  atandm4  26796  atanf  26797  asinneg  26803  efiasin  26805  sinasin  26806  asinsin  26809  asin1  26811  acos1  26812  reasinsin  26813  asinbnd  26816  cosasin  26821  atanneg  26824  atancj  26827  efiatan  26829  atanlogaddlem  26830  atanlogadd  26831  atanlogsublem  26832  atanlogsub  26833  efiatan2  26834  2efiatan  26835  tanatan  26836  cosatan  26838  cosatanne0  26839  atantan  26840  atanbndlem  26842  bndatandm  26846  atans2  26848  dvatan  26852  atantayl  26854  atantayl2  26855  atantayl3  26856  leibpilem2  26858  leibpi  26859  log2cnv  26861  log2tlbnd  26862  log2ublem3  26865  log2ub  26866  birthdaylem2  26869  birthday  26871  efrlim  26886  efrlimOLD  26887  dfef2  26888  cvxcl  26902  scvxcvx  26903  emcllem2  26914  emcllem4  26916  emcllem7  26919  harmonicbnd4  26928  fsumharmonic  26929  zetacvg  26932  lgamcvg2  26972  lgam1  26981  gam1  26982  wilthlem1  26985  wilthlem2  26986  wilthlem3  26987  basellem2  26999  basellem5  27002  basellem6  27003  basellem7  27004  basellem8  27005  basellem9  27006  0sgm  27061  mule1  27065  ppiprm  27068  ppinprm  27069  chtprm  27070  chtnprm  27071  chpp1  27072  mumullem2  27097  1sgmprm  27117  1sgm2ppw  27118  ppiub  27122  chtublem  27129  chtub  27130  logfaclbnd  27140  logfacbnd3  27141  logfacrlim  27142  logexprlim  27143  mersenne  27145  perfect1  27146  perfectlem1  27147  perfectlem2  27148  perfect  27149  dchrelbasd  27157  dchrmullid  27170  dchrfi  27173  dchrsum2  27186  sumdchr2  27188  bcp1ctr  27197  bposlem8  27209  zabsle1  27214  lgslem1  27215  lgslem2  27216  lgsfcl2  27221  lgsvalmod  27234  lgsneg  27239  lgsdilem  27242  lgsdir2lem1  27243  lgsdir2lem2  27244  lgsdir2lem3  27245  lgsdir2lem5  27247  lgsdir2  27248  lgsdir  27250  lgsdi  27252  lgsne0  27253  lgseisenlem1  27293  lgseisenlem2  27294  lgseisen  27297  lgsquadlem1  27298  lgsquadlem2  27299  lgsquad2lem1  27302  lgsquad2  27304  m1lgs  27306  2lgslem3c  27316  2lgsoddprmlem3c  27330  2lgsoddprmlem3d  27331  2sqlem10  27346  2sqlem11  27347  2sqblem  27349  addsqn2reu  27359  addsqrexnreu  27360  addsqnreup  27361  chtppilimlem2  27392  chebbnd2  27395  chto1lb  27396  rplogsumlem1  27402  rpvmasumlem  27405  dchrmusumlema  27411  dchrmusum2  27412  dchrisum0flblem1  27426  rpvmasum2  27430  mudivsum  27448  mulogsum  27450  vmalogdivsum2  27456  selberg2lem  27468  logdivbnd  27474  pntrmax  27482  pntrsumo1  27483  pntrsumbnd2  27485  pntrlog2bndlem5  27499  pntpbnd1a  27503  pntpbnd2  27505  pntibndlem2  27509  pntlemd  27512  pntlemc  27513  pntlemr  27520  brbtwn2  28839  colinearalglem4  28843  ax5seglem1  28862  ax5seglem2  28863  ax5seglem3  28865  ax5seglem5  28867  ax5seglem7  28869  ax5seglem9  28871  axbtwnid  28873  axpaschlem  28874  axlowdimlem13  28888  axlowdimlem14  28889  axlowdimlem16  28891  axeuclidlem  28896  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  axcontlem8  28905  crctcshwlkn0lem6  29752  clwwlkf1  29985  clwwlknonex2lem2  30044  ex-fl  30383  ex-ind-dvds  30397  vc2OLD  30504  vc0  30510  vcm  30512  nvm1  30601  nvmtri  30607  nvge0  30609  ipval2lem3  30641  ipidsq  30646  lnoadd  30694  ip1ilem  30762  ip1i  30763  ip2i  30764  ipdirilem  30765  ipasslem1  30767  ipasslem2  30768  ipasslem10  30775  minvecolem2  30811  hvsubid  30962  hv2times  30997  hisubcomi  31040  normlem9  31054  normlem7tALT  31055  norm-ii-i  31073  normsubi  31077  hhssnv  31200  pjhthlem1  31327  h1de2bi  31490  homullid  31736  ho2times  31755  lnop0  31902  lnopaddi  31907  lnophmlem2  31953  lnfn0i  31978  lnfnaddi  31979  hst1h  32163  sto2i  32173  stadd3i  32184  addltmulALT  32382  sgnneg  32765  dpmul4  32841  psgnid  33061  cnmsgn0g  33110  altgnsg  33113  isarchi3  33148  archirngz  33150  1fldgenq  33279  ply1dg3rt0irred  33558  ccfldextdgrr  33674  constrsscn  33737  constrabscl  33775  cos9thpiminplylem1  33779  cos9thpiminplylem4  33782  cos9thpiminplylem5  33783  lmatfvlem  33812  qqhval2lem  33978  dya2ub  34268  omssubadd  34298  eulerpartlemgs2  34378  fib5  34403  fib6  34404  ballotlem2  34487  signswch  34559  signlem0  34585  itgexpif  34604  reprlt  34617  breprexp  34631  breprexpnat  34632  hgt750lem2  34650  subfacp1lem5  35178  subfacp1lem6  35179  subfacval2  35181  subfaclim  35182  subfacval3  35183  cvxsconn  35237  resconn  35240  cvmliftlem7  35285  cvmliftlem10  35288  problem4  35662  sinccvglem  35666  sqdivzi  35722  faclimlem1  35737  dnibndlem5  36477  dnibndlem10  36482  ltflcei  37609  sin2h  37611  cos2h  37612  tan2h  37613  poimirlem13  37634  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem31  37652  mblfinlem2  37659  mblfinlem3  37660  dvtan  37671  itg2addnclem3  37674  dvasin  37705  dvacos  37706  areacirc  37714  fdc  37746  mettrifi  37758  heiborlem4  37815  heiborlem6  37817  60gcd7e1  42000  lcmineqlem1  42024  lcmineqlem8  42031  lcmineqlem9  42032  lcmineqlem10  42033  lcmineqlem12  42035  3exp7  42048  3lexlogpow5ineq1  42049  3lexlogpow5ineq5  42055  aks4d1p1p4  42066  aks4d1p1p7  42069  aks4d1p1  42071  facp2  42138  1p3e4  42254  sn-1ne2  42260  sqdeccom12  42284  235t711  42300  sin2t3rdpi  42348  cos2t3rdpi  42349  re1m1e0m0  42392  ipiiie0  42433  sn-0tie0  42446  fltnltalem  42657  sum9cubes  42667  3cubeslem3l  42681  3cubeslem3r  42682  eldioph2lem1  42755  lzenom  42765  irrapxlem1  42817  rmspecsqrtnq  42901  rmxm1  42930  rmym1  42931  2nn0ind  42941  jm2.24nn  42955  jm2.17a  42956  jm2.17b  42957  jm2.17c  42958  jm2.24  42959  acongeq  42979  jm2.18  42984  jm2.27c  43003  jm3.1lem2  43014  rngunsnply  43165  flcidc  43166  inductionexd  44151  unitadd  44191  hashnzfzclim  44318  ofdivrec  44322  lhe4.4ex1a  44325  expgrowth  44331  dvradcnv2  44343  binomcxplemrat  44346  binomcxplemnotnn0  44352  isosctrlem1ALT  44930  monoord2xrv  45486  dvsinax  45918  dvnprodlem3  45953  itgsin0pilem1  45955  itgsbtaddcnst  45987  stoweidlem13  46018  stoweidlem26  46031  stoweidlem34  46039  stoweidlem38  46043  wallispilem2  46071  wallispilem4  46073  wallispi2lem1  46076  stirlinglem1  46079  stirlinglem5  46083  stirlinglem10  46088  dirkerper  46101  dirkertrigeqlem1  46103  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkercncflem4  46111  fourierdlem24  46136  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  lambert0  46895  lamberte  46896  1t10e1p1e11  47315  ceil5half3  47345  modm2nep1  47371  modm1nep2  47373  modm1nem2  47374  fmtnorec3  47553  fmtno5lem4  47561  fmtno5  47562  257prm  47566  fmtno4nprmfac193  47579  m3prm  47597  139prmALT  47601  127prm  47604  m7prm  47605  lighneallem3  47612  proththd  47619  3exp4mod41  47621  41prothprmlem2  47623  perfectALTVlem2  47727  perfectALTV  47728  11t31e341  47737  evengpop3  47803  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  bgoldbtbndlem1  47810  0nodd  48162  altgsumbcALT  48345  exple2lt6  48356  nn0sumshdiglemB  48613  ackval3  48676  ackval3012  48685  line2ylem  48744  onetansqsecsq  49754  cotsqcscsq  49755  5m4e1  49790