Axiom ax-1cn 11229

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

This axiom is used by:  0cn  11269  1cnd  11273  1ex  11274  mulrid  11277  mullid  11278  1re  11279  0re  11281  muladd11  11451  peano2cn  11453  mul02lem2  11458  addrid  11461  cnegex2  11463  peano2cnm  11595  0reALT  11626  ine0  11720  mulm1  11726  0lt1  11807  ixi  11914  muleqadd  11929  reccl  11950  recne0  11956  recid  11957  recid2  11958  diveq1  11972  div1  11975  1div1e1  11976  recdiv  11992  divdiv1  11997  divdiv2  11998  recdiv2  11999  conjmul  12003  eqneg  12006  div2neg  12009  recp1lt1  12184  recreclt  12185  recgt0ii  12192  neg1cn  12274  neg1ne0  12276  negneg1e1  12278  ofnegsub  12287  peano5nni  12307  nnsscn  12309  nn1m1nn  12325  nn1suc  12326  nnaddcl  12327  nnmulcl  12328  nnne0  12341  nnsub  12351  1m1e0  12384  2cn  12387  3cn  12393  4cn  12397  5cn  12400  6cn  12403  7cn  12406  8cn  12409  9cn  12412  1pneg1e0  12429  1m0e1  12431  0p1e1  12432  1p0e1  12434  2m1e1  12436  2m1e1OLD  12437  3m1e2  12439  4m1e3  12440  5m1e4  12441  6m1e5  12442  7m1e6  12443  8m1e7  12444  9m1e8  12445  2p2e4  12446  1p2e3  12454  1p2e3ALT  12455  3p2e5  12462  3p3e6  12463  4p2e6  12464  4p3e7  12465  4p4e8  12466  5p2e7  12467  5p3e8  12468  5p4e9  12469  6p2e8  12470  6p3e9  12471  7p2e9  12472  1t1e1  12473  3t3e9  12479  neg1mulneg1e1  12527  1mhlfehlf  12534  8th4div3  12535  halfthird  12536  halfpm6th  12537  addltmul  12551  elnn0nn  12617  elz2  12680  zlem1lt  12717  zltlem1  12718  nnaddm1cl  12725  zextlt  12742  zeo  12754  peano5uzi  12757  numsuc  12797  numltc  12814  numsucc  12828  numaddc  12836  6p5lem  12858  5p5e10  12859  6p4e10  12860  7p3e10  12863  8p2e10  12868  10m1e9  12884  4t3lem  12885  7t4e28  12899  9t11e99OLD  12919  decbin2  12931  5recm6rec  12933  uzp1  12971  peano2uzr  12999  uzaddcl  13000  rebtwnz  13043  qbtwnre  13298  iccf1o  13596  fz01en  13654  fztp  13682  fzsuc2  13684  fztpval  13688  fseq1m1p1  13701  elfzp1b  13703  predfz  13755  fzoss2  13790  fzval3  13837  fzosplitsnm1  13843  fzo1to4tp  13857  fldiv4p1lem1div2  13943  ceim1l  13955  fldiv  13968  uzrdgxfr  14078  fzen2  14080  nn0ennn  14090  seqm1  14130  seqshft2  14139  monoord2  14144  sermono  14145  seqf1olem1  14152  seqf1olem2  14153  seqz  14161  ser1const  14169  expcl  14190  expclzlem  14194  m1expcl2  14196  expm1t  14201  1exp  14202  mulexpz  14213  expadd  14215  expaddz  14217  expmul  14218  expubnd  14289  sqrecii  14294  neg1sqe1  14307  irec  14312  i4  14315  binom21  14330  sq01  14336  crreczi  14339  bernneq  14340  bernneq2  14341  nn0opthlem1  14379  facndiv  14399  faclbnd4lem1  14404  faclbnd6  14410  bcnp1n  14425  bcm1k  14426  bcp1nk  14428  bcn2  14430  bcp1m1  14431  bcpasc  14432  hashgadd  14488  hashfz  14539  hashfzo  14541  hashxplem  14545  hashbclem  14564  hashf1  14569  seqcoll  14576  swrds1  14783  swrdlsw  14784  wrdind  14838  wrd2ind  14839  swrds2  15058  relexpaddg  15173  sgnneg  15220  rei  15290  imi  15291  recan  15471  iserex  15791  isercoll2  15803  serf0  15815  iseraltlem2  15817  iseraltlem3  15818  iseralt  15819  sumrblem  15844  fsumm1  15884  telfsumo  15936  fsumparts  15940  hashiun  15956  binomlem  15965  binom  15966  binom1p  15967  binom11  15968  binom1dif  15969  bcxmas  15971  isumsplit  15976  isum1p  15977  climcndslem1  15985  supcvg  15992  harmonic  15995  arisum  15996  arisum2  15997  trireciplem  15998  geoserg  16002  geolim  16006  geolim2  16007  georeclim  16008  geo2sum  16009  geo2sum2  16010  geoisum1c  16016  0.999...  16017  geoihalfsum  16018  cvgrat  16019  mertenslem1  16020  mertenslem2  16021  mertens  16022  prodf1  16027  prodfclim1  16029  prodrblem  16063  fprodcvg  16064  prodmolem2a  16068  zprod  16071  fprodntriv  16076  prodss  16081  fprodss  16082  fprodsplit  16100  fprodn0f  16125  risefaccl  16149  fallfaccl  16150  risefacfac  16168  binomfallfac  16174  bpolycl  16185  bpolysum  16186  bpolydiflem  16187  fsumkthpow  16189  bpoly2  16190  bpoly3  16191  bpoly4  16192  fsumcube  16193  esum  16213  ege2le3  16223  efsub  16235  efexp  16236  efzval  16237  eftlub  16244  effsumlt  16246  ef4p  16248  tanval3  16269  efi4p  16272  tan0  16286  efival  16287  tanadd  16302  cos2t  16313  cos2tsin  16314  ef01bndlem  16319  cos1bnd  16322  cos2bnd  16323  demoivreALT  16336  eirrlem  16339  rpnnen2lem3  16351  rpnnen2lem11  16359  ruclem12  16376  3dvds  16468  3dvdsdec  16469  3dvds2dec  16470  odd2np1lem  16477  odd2np1  16478  opoe  16500  omoe  16501  opeo  16502  omeo  16503  n2dvdsm1  16506  m1exp1  16513  flodddiv4  16552  bitsfzo  16572  sqgcd  16699  expgcd  16700  nn0seqcvgd  16707  prmind2  16822  hashdvds  16913  phiprmpw  16914  phiprm  16915  eulerthlem2  16920  iserodd  16974  sumhash  17035  fldivp1  17036  prmpwdvds  17043  pockthlem  17044  pockthi  17046  prmreclem4  17058  prmreclem6  17060  4sqlem11  17094  4sqlem19  17102  vdwapun  17113  vdwapid1  17114  vdwlem3  17122  vdwlem5  17124  vdwlem6  17125  vdwlem8  17127  vdwlem9  17128  vdwnnlem2  17135  ramub1lem1  17165  ramub1lem2  17166  ramcl  17168  prmo1  17176  dec5nprm  17205  prmlem0  17244  43prm  17261  83prm  17262  139prm  17263  163prm  17264  317prm  17265  631prm  17266  1259lem2  17271  1259lem3  17272  1259lem4  17273  1259lem5  17274  1259prm  17275  2503lem1  17276  2503lem2  17277  2503lem3  17278  2503prm  17279  4001lem1  17280  4001lem2  17281  4001lem3  17282  4001lem4  17283  4001prm  17284  gsumsgrpccat  18997  mulgnndir  19274  mulgneg2  19279  m1expaddsub  19673  sylow1lem1  19773  sylow2a  19794  efgsval2  19908  efgsrel  19909  efgsres  19913  cncrng  21660  cnfld1  21664  zsssubrg  21692  cnmgpid  21696  zringcyg  21736  mulgrhm2  21745  pzriprng1ALT  21763  cnmsgnsubg  21844  cnmsgnbas  21845  cnmsgngrp  21846  psgninv  21849  evpmodpmf1o  21863  psdmplcl  22444  blcvx  25078  iihalf2  25215  icopnfcnv  25224  iccpnfhmeo  25227  xrhmeo  25228  icccvx  25232  lebnumii  25248  reparphti  25279  pcoass  25306  pcorevlem  25308  pcorev2  25310  pi1xfrcnv  25339  cnstrcvs  25423  cncvs  25427  ncvsm1  25436  pjthlem1  25719  divcncf  25729  ovolunlem1a  25778  ovolunlem1  25779  ovolicc2lem4  25802  uniioombllem3  25867  uniioombllem4  25868  dyadovol  25875  vitalilem4  25893  mbf0  25916  iblcnlem1  26069  itgcnlem  26071  dvid  26199  dvexp  26234  dvexp2  26235  dvexp3  26259  dveflem  26260  dvlipcn  26275  dvcvx  26301  dvfsumle  26302  dvfsumlem1  26307  degltp1le  26352  ply1divex  26416  fta1glem1  26447  plyaddlem1  26493  plymullem1  26494  coeidp  26543  dgrid  26544  dvply1  26568  dvply2g  26569  plyremlem  26588  fta1lem  26591  vieta1lem1  26596  vieta1lem2  26597  qaa  26610  iaa  26614  iaaOLD  26615  aalioulem3  26624  geolim3  26629  aaliou3lem2  26633  aaliou3lem7  26639  taylply2  26658  dvradcnv  26711  pserdvlem2  26718  pserdv2  26720  abelthlem1  26721  abelthlem2  26722  abelthlem6  26726  abelthlem7  26728  abelth  26731  reeff1olem  26736  reeff1o  26737  efcvx  26739  sinhalfpilem  26755  eulerid  26766  cos2pi  26768  sincosq3sgn  26792  sincosq4sgn  26793  tangtx  26797  sincos4thpi  26805  sincos6thpi  26807  pigt3  26809  pige3ALT  26811  abssinper  26812  coskpi  26814  coseq1  26816  efeq1  26819  tanregt0  26830  logneg2  26906  logdivlti  26911  logcnlem4  26936  dvlog2lem  26943  dvlog2  26944  advlog  26945  advlogexp  26946  logtayl  26951  logtayl2  26953  logccv  26954  cxpval  26955  1cxp  26963  cxpcl  26965  cxpp1  26971  cxpsqrt  26994  dvsqrt  27033  dvcnsqrt  27035  sqrtcn  27041  cxpaddlelem  27042  root1id  27045  root1cj  27047  logrec  27054  logb1  27060  logbmpt  27079  ang180lem1  27100  ang180lem2  27101  ang180lem3  27102  isosctrlem1  27109  isosctrlem2  27110  1cubrlem  27132  1cubr  27133  mcubic  27138  binom4  27141  dquartlem1  27142  quartlem1  27148  asinlem  27159  asinlem2  27160  asinlem3a  27161  asinlem3  27162  asinf  27163  atandm2  27168  atandm4  27170  atanf  27171  asinneg  27177  efiasin  27179  sinasin  27180  asinsin  27183  asin1  27185  acos1  27186  reasinsin  27187  asinbnd  27190  cosasin  27195  atanneg  27198  atancj  27201  efiatan  27203  atanlogaddlem  27204  atanlogadd  27205  atanlogsublem  27206  atanlogsub  27207  efiatan2  27208  2efiatan  27209  tanatan  27210  cosatan  27212  cosatanne0  27213  atantan  27214  atanbndlem  27216  bndatandm  27220  atans2  27222  dvatan  27226  atantayl  27228  atantayl2  27229  atantayl3  27230  leibpilem2  27232  leibpi  27233  log2cnv  27235  log2tlbnd  27236  log2ublem3  27239  log2ub  27240  birthdaylem2  27243  birthday  27245  efrlim  27260  dfef2  27261  cvxcl  27275  scvxcvx  27276  emcllem2  27287  emcllem4  27289  emcllem7  27292  harmonicbnd4  27301  fsumharmonic  27302  zetacvg  27305  lgamcvg2  27345  lgam1  27354  gam1  27355  wilthlem1  27358  wilthlem2  27359  wilthlem3  27360  basellem2  27372  basellem5  27375  basellem6  27376  basellem7  27377  basellem8  27378  basellem9  27379  0sgm  27434  mule1  27438  ppiprm  27441  ppinprm  27442  chtprm  27443  chtnprm  27444  chpp1  27445  mumullem2  27470  1sgmprm  27489  1sgm2ppw  27490  ppiub  27494  chtublem  27501  chtub  27502  logfaclbnd  27512  logfacbnd3  27513  logfacrlim  27514  logexprlim  27515  mersenne  27517  perfect1  27518  perfectlem1  27519  perfectlem2  27520  perfect  27521  dchrelbasd  27529  dchrmullid  27542  dchrfi  27545  dchrsum2  27558  sumdchr2  27560  bcp1ctr  27569  bposlem8  27581  zabsle1  27586  lgslem1  27587  lgslem2  27588  lgsfcl2  27593  lgsvalmod  27606  lgsneg  27611  lgsdilem  27614  lgsdir2lem1  27615  lgsdir2lem2  27616  lgsdir2lem3  27617  lgsdir2lem5  27619  lgsdir2  27620  lgsdir  27622  lgsdi  27624  lgsne0  27625  lgseisenlem1  27665  lgseisenlem2  27666  lgseisen  27669  lgsquadlem1  27670  lgsquadlem2  27671  lgsquad2lem1  27674  lgsquad2  27676  m1lgs  27678  2lgslem3c  27688  2lgsoddprmlem3c  27702  2lgsoddprmlem3d  27703  2sqlem10  27718  2sqlem11  27719  2sqblem  27721  addsqn2reu  27731  addsqrexnreu  27732  addsqnreup  27733  chtppilimlem2  27764  chebbnd2  27767  chto1lb  27768  rplogsumlem1  27774  rpvmasumlem  27777  dchrmusumlema  27783  dchrmusum2  27784  dchrisum0flblem1  27798  rpvmasum2  27802  mudivsum  27820  mulogsum  27822  vmalogdivsum2  27828  selberg2lem  27840  logdivbnd  27846  pntrmax  27854  pntrsumo1  27855  pntrsumbnd2  27857  pntrlog2bndlem5  27871  pntpbnd1a  27875  pntpbnd2  27877  pntibndlem2  27881  pntlemd  27884  pntlemc  27885  pntlemr  27892  brbtwn2  29416  colinearalglem4  29420  ax5seglem1  29439  ax5seglem2  29440  ax5seglem3  29442  ax5seglem5  29444  ax5seglem7  29446  ax5seglem9  29448  axbtwnid  29450  axpaschlem  29451  axlowdimlem13  29465  axlowdimlem14  29466  axlowdimlem16  29468  axeuclidlem  29473  axcontlem2  29476  axcontlem4  29478  axcontlem7  29481  axcontlem8  29482  crctcshwlkn0lem6  30337  clwwlkf1  30573  clwwlknonex2lem2  30632  ex-fl  30981  ex-ind-dvds  30995  vc2OLD  31103  vc0  31109  vcm  31111  nvm1  31200  nvmtri  31206  nvge0  31208  ipval2lem3  31240  ipidsq  31245  lnoadd  31293  ip1ilem  31361  ip1i  31362  ip2i  31363  ipdirilem  31364  ipasslem1  31366  ipasslem2  31367  ipasslem10  31374  minvecolem2  31410  hvsubid  31561  hv2times  31596  hisubcomi  31639  normlem9  31653  normlem7tALT  31654  norm-ii-i  31672  normsubi  31676  hhssnv  31799  pjhthlem1  31926  h1de2bi  32089  homullid  32335  ho2times  32354  lnop0  32501  lnopaddi  32506  lnophmlem2  32552  lnfn0i  32577  lnfnaddi  32578  hst1h  32762  sto2i  32772  stadd3i  32783  addltmulALT  32981  dpmul4  33413  psgnid  33591  cnmsgn0g  33640  altgnsg  33643  isarchi3  33681  archirngz  33683  1fldgenq  33817  ply1dg3rt0irred  34049  esplyfvaln  34139  ccfldextdgrr  34237  constrsscn  34305  constrabscl  34343  cos9thpiminplylem1  34347  cos9thpiminplylem4  34350  cos9thpiminplylem5  34351  lmatfvlem  34380  qqhval2lem  34546  dya2ub  34836  omssubadd  34866  eulerpartlemgs2  34946  fib5  34971  fib6  34972  ballotlem2  35055  signswch  35124  signlem0  35150  itgexpif  35169  reprlt  35182  breprexp  35196  breprexpnat  35197  hgt750lem2  35215  subfacp1lem5  35870  subfacp1lem6  35871  subfacval2  35873  subfaclim  35874  subfacval3  35875  cvxsconn  35929  resconn  35932  cvmliftlem7  35977  cvmliftlem10  35980  problem4  36354  sinccvglem  36358  sqdivzi  36414  faclimlem1  36429  dnibndlem5  37270  dnibndlem10  37275  ltflcei  38451  sin2h  38453  cos2h  38454  tan2h  38455  poimirlem13  38471  poimirlem16  38474  poimirlem17  38475  poimirlem19  38477  poimirlem20  38478  poimirlem31  38489  mblfinlem2  38496  mblfinlem3  38497  dvtan  38508  itg2addnclem3  38511  dvasin  38542  dvacos  38543  areacirc  38551  fdc  38599  mettrifi  38611  heiborlem4  38668  heiborlem6  38670  60gcd7e1  42975  lcmineqlem1  42999  lcmineqlem8  43006  lcmineqlem9  43007  lcmineqlem10  43008  lcmineqlem12  43010  3exp7  43023  3lexlogpow5ineq1  43024  3lexlogpow5ineq5  43030  aks4d1p1p4  43041  aks4d1p1p7  43044  aks4d1p1  43046  facp2  43113  25or6to4  43176  1p3e4  43230  1p4e5  43231  1p5e6  43232  1p6e7  43233  1p7e8  43234  1p8e9  43235  2p3e5  43236  4p5e9  43244  sn-1ne2  43250  sqdeccom12  43268  235t711  43284  sin2t3rdpi  43332  cos2t3rdpi  43333  re1m1e0m0  43376  ipiiie0  43417  sn-0tie0  43443  fltnltalem  43612  sum9cubes  43622  3cubeslem3l  43635  3cubeslem3r  43636  eldioph2lem1  43709  lzenom  43719  irrapxlem1  43767  rmspecsqrtnq  43851  rmxm1  43879  rmym1  43880  2nn0ind  43890  jm2.24nn  43904  jm2.17a  43905  jm2.17b  43906  jm2.17c  43907  jm2.24  43908  acongeq  43928  jm2.18  43933  jm2.27c  43952  jm3.1lem2  43963  rngunsnply  44114  flcidc  44115  inductionexd  45099  unitadd  45139  hashnzfzclim  45250  ofdivrec  45254  lhe4.4ex1a  45257  expgrowth  45263  dvradcnv2  45275  binomcxplemrat  45278  binomcxplemnotnn0  45284  isosctrlem1ALT  45860  monoord2xrv  46415  dvsinax  46845  dvnprodlem3  46880  itgsin0pilem1  46882  itgsbtaddcnst  46914  stoweidlem13  46945  stoweidlem26  46958  stoweidlem34  46966  stoweidlem38  46970  wallispilem2  46998  wallispilem4  47000  wallispi2lem1  47003  stirlinglem1  47006  stirlinglem5  47010  stirlinglem10  47015  dirkerper  47028  dirkertrigeqlem1  47030  dirkertrigeqlem3  47032  dirkertrigeq  47033  dirkercncflem4  47038  fourierdlem24  47063  sqwvfoura  47160  sqwvfourb  47161  fourierswlem  47162  cos5t  47847  goldpolyfactor  47849  goldratmolem2  47855  goldratmolem4  47857  goldratval  47858  lambert0  47859  lamberte  47860  cjnpoly  47861  sqrtnpoly  47865  1t10e1p1e11  48302  ceil5half3  48338  modm2nep1  48364  modm1nep2  48366  modm1nem2  48367  fmtnorec3  48555  fmtno5lem4  48563  fmtno5  48564  257prm  48568  fmtno4nprmfac193  48581  m3prm  48599  139prmALT  48603  127prm  48606  m7prm  48607  lighneallem3  48614  proththd  48621  3exp4mod41  48623  41prothprmlem2  48625  perfectALTVlem2  48742  perfectALTV  48743  11t31e341  48752  evengpop3  48818  nnsum4primeseven  48820  nnsum4primesevenALTV  48821  bgoldbtbndlem1  48825  0nodd  49189  altgsumbcALT  49387  exple2lt6  49398  nn0sumshdiglemB  49654  ackval3  49717  ackval3012  49726  line2ylem  49785  onetansqsecsq  50776  cotsqcscsq  50777  dvsec  50778  dvcsc  50779  dvcot  50780  5m4e1  50857