Axiom ax-1cn 11185

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

This axiom is used by:  0cn  11225  1cnd  11229  1ex  11230  mulrid  11233  mullid  11234  1re  11235  0re  11237  muladd11  11407  peano2cn  11409  mul02lem2  11414  addrid  11417  cnegex2  11419  peano2cnm  11551  0reALT  11582  ine0  11676  mulm1  11682  0lt1  11763  ixi  11870  muleqadd  11885  reccl  11906  recne0  11912  recid  11913  recid2  11914  diveq1  11928  div1  11931  1div1e1  11932  recdiv  11948  divdiv1  11953  divdiv2  11954  recdiv2  11955  conjmul  11959  eqneg  11962  div2neg  11965  recp1lt1  12140  recreclt  12141  recgt0ii  12148  neg1cn  12230  neg1ne0  12232  negneg1e1  12234  ofnegsub  12243  peano5nni  12263  nnsscn  12265  nn1m1nn  12281  nn1suc  12282  nnaddcl  12283  nnmulcl  12284  nnne0  12297  nnsub  12307  1m1e0  12340  2cn  12343  3cn  12349  4cn  12353  5cn  12356  6cn  12359  7cn  12362  8cn  12365  9cn  12368  1pneg1e0  12385  1m0e1  12387  0p1e1  12388  1p0e1  12390  2m1e1  12392  2m1e1OLD  12393  3m1e2  12395  4m1e3  12396  5m1e4  12397  6m1e5  12398  7m1e6  12399  8m1e7  12400  9m1e8  12401  2p2e4  12402  1p2e3  12410  1p2e3ALT  12411  3p2e5  12418  3p3e6  12419  4p2e6  12420  4p3e7  12421  4p4e8  12422  5p2e7  12423  5p3e8  12424  5p4e9  12425  6p2e8  12426  6p3e9  12427  7p2e9  12428  1t1e1  12429  3t3e9  12435  neg1mulneg1e1  12483  1mhlfehlf  12490  8th4div3  12491  halfthird  12492  halfpm6th  12493  addltmul  12507  elnn0nn  12573  elz2  12636  zlem1lt  12673  zltlem1  12674  nnaddm1cl  12681  zextlt  12698  zeo  12710  peano5uzi  12713  numsuc  12753  numltc  12770  numsucc  12784  numaddc  12792  6p5lem  12814  5p5e10  12815  6p4e10  12816  7p3e10  12819  8p2e10  12824  10m1e9  12840  4t3lem  12841  7t4e28  12855  9t11e99OLD  12875  decbin2  12887  5recm6rec  12889  uzp1  12927  peano2uzr  12955  uzaddcl  12956  rebtwnz  12999  qbtwnre  13253  iccf1o  13551  fz01en  13609  fztp  13637  fzsuc2  13639  fztpval  13643  fseq1m1p1  13656  elfzp1b  13658  predfz  13710  fzoss2  13745  fzval3  13792  fzosplitsnm1  13798  fzo1to4tp  13812  fldiv4p1lem1div2  13898  ceim1l  13910  fldiv  13923  uzrdgxfr  14033  fzen2  14035  nn0ennn  14045  seqm1  14085  seqshft2  14094  monoord2  14099  sermono  14100  seqf1olem1  14107  seqf1olem2  14108  seqz  14116  ser1const  14124  expcl  14145  expclzlem  14149  m1expcl2  14151  expm1t  14156  1exp  14157  mulexpz  14168  expadd  14170  expaddz  14172  expmul  14173  expubnd  14244  sqrecii  14249  neg1sqe1  14262  irec  14267  i4  14270  binom21  14285  sq01  14291  crreczi  14294  bernneq  14295  bernneq2  14296  nn0opthlem1  14334  facndiv  14354  faclbnd4lem1  14359  faclbnd6  14365  bcnp1n  14380  bcm1k  14381  bcp1nk  14383  bcn2  14385  bcp1m1  14386  bcpasc  14387  hashgadd  14443  hashfz  14494  hashfzo  14496  hashxplem  14500  hashbclem  14519  hashf1  14524  seqcoll  14531  swrds1  14738  swrdlsw  14739  wrdind  14793  wrd2ind  14794  swrds2  15013  relexpaddg  15128  sgnneg  15175  rei  15245  imi  15246  recan  15426  iserex  15746  isercoll2  15758  serf0  15770  iseraltlem2  15772  iseraltlem3  15773  iseralt  15774  sumrblem  15799  fsumm1  15839  telfsumo  15891  fsumparts  15895  hashiun  15911  binomlem  15920  binom  15921  binom1p  15922  binom11  15923  binom1dif  15924  bcxmas  15926  isumsplit  15931  isum1p  15932  climcndslem1  15940  supcvg  15947  harmonic  15950  arisum  15951  arisum2  15952  trireciplem  15953  geoserg  15957  geolim  15961  geolim2  15962  georeclim  15963  geo2sum  15964  geo2sum2  15965  geoisum1c  15971  0.999...  15972  geoihalfsum  15973  cvgrat  15974  mertenslem1  15975  mertenslem2  15976  mertens  15977  prodf1  15982  prodfclim1  15984  prodrblem  16020  fprodcvg  16021  prodmolem2a  16025  zprod  16028  fprodntriv  16033  prodss  16038  fprodss  16039  fprodsplit  16057  fprodn0f  16082  risefaccl  16106  fallfaccl  16107  risefacfac  16125  binomfallfac  16131  bpolycl  16142  bpolysum  16143  bpolydiflem  16144  fsumkthpow  16146  bpoly2  16147  bpoly3  16148  bpoly4  16149  fsumcube  16150  esum  16170  ege2le3  16180  efsub  16192  efexp  16193  efzval  16194  eftlub  16201  effsumlt  16203  ef4p  16205  tanval3  16226  efi4p  16229  tan0  16243  efival  16244  tanadd  16259  cos2t  16270  cos2tsin  16271  ef01bndlem  16276  cos1bnd  16279  cos2bnd  16280  demoivreALT  16293  eirrlem  16296  rpnnen2lem3  16308  rpnnen2lem11  16316  ruclem12  16333  3dvds  16425  3dvdsdec  16426  3dvds2dec  16427  odd2np1lem  16434  odd2np1  16435  opoe  16457  omoe  16458  opeo  16459  omeo  16460  n2dvdsm1  16463  m1exp1  16470  flodddiv4  16509  bitsfzo  16529  sqgcd  16656  expgcd  16657  nn0seqcvgd  16664  prmind2  16779  hashdvds  16870  phiprmpw  16871  phiprm  16872  eulerthlem2  16877  iserodd  16931  sumhash  16992  fldivp1  16993  prmpwdvds  17000  pockthlem  17001  pockthi  17003  prmreclem4  17015  prmreclem6  17017  4sqlem11  17051  4sqlem19  17059  vdwapun  17070  vdwapid1  17071  vdwlem3  17079  vdwlem5  17081  vdwlem6  17082  vdwlem8  17084  vdwlem9  17085  vdwnnlem2  17092  ramub1lem1  17122  ramub1lem2  17123  ramcl  17125  prmo1  17133  dec5nprm  17162  prmlem0  17201  43prm  17218  83prm  17219  139prm  17220  163prm  17221  317prm  17222  631prm  17223  1259lem2  17228  1259lem3  17229  1259lem4  17230  1259lem5  17231  1259prm  17232  2503lem1  17233  2503lem2  17234  2503lem3  17235  2503prm  17236  4001lem1  17237  4001lem2  17238  4001lem3  17239  4001lem4  17240  4001prm  17241  gsumsgrpccat  18950  mulgnndir  19227  mulgneg2  19232  m1expaddsub  19626  sylow1lem1  19726  sylow2a  19747  efgsval2  19861  efgsrel  19862  efgsres  19866  cncrng  21607  cnfld1  21611  zsssubrg  21639  cnmgpid  21643  zringcyg  21683  mulgrhm2  21692  pzriprng1ALT  21710  cnmsgnsubg  21791  cnmsgnbas  21792  cnmsgngrp  21793  psgninv  21796  evpmodpmf1o  21810  psdmplcl  22391  blcvx  25025  iihalf2  25162  icopnfcnv  25171  iccpnfhmeo  25174  xrhmeo  25175  icccvx  25179  lebnumii  25195  reparphti  25226  pcoass  25253  pcorevlem  25255  pcorev2  25257  pi1xfrcnv  25286  cnstrcvs  25370  cncvs  25374  ncvsm1  25383  pjthlem1  25666  divcncf  25676  ovolunlem1a  25725  ovolunlem1  25726  ovolicc2lem4  25749  uniioombllem3  25814  uniioombllem4  25815  dyadovol  25822  vitalilem4  25840  mbf0  25863  iblcnlem1  26017  itgcnlem  26019  dvid  26147  dvexp  26182  dvexp2  26183  dvexp3  26207  dveflem  26208  dvlipcn  26223  dvcvx  26249  dvfsumle  26250  dvfsumlem1  26255  degltp1le  26300  ply1divex  26364  fta1glem1  26395  plyaddlem1  26440  plymullem1  26441  coeidp  26490  dgrid  26491  dvply1  26515  dvply2g  26516  plyremlem  26535  fta1lem  26538  vieta1lem1  26541  vieta1lem2  26542  qaa  26554  iaa  26558  aalioulem3  26567  geolim3  26572  aaliou3lem2  26576  aaliou3lem7  26582  taylply2  26601  dvradcnv  26654  pserdvlem2  26661  pserdv2  26663  abelthlem1  26664  abelthlem2  26665  abelthlem6  26669  abelthlem7  26671  abelth  26674  reeff1olem  26679  reeff1o  26680  efcvx  26682  sinhalfpilem  26698  eulerid  26709  cos2pi  26711  sincosq3sgn  26735  sincosq4sgn  26736  tangtx  26740  sincos4thpi  26748  sincos6thpi  26751  pigt3  26753  pige3ALT  26755  abssinper  26756  coskpi  26758  coseq1  26760  efeq1  26763  tanregt0  26774  logneg2  26850  logdivlti  26855  logcnlem4  26880  dvlog2lem  26887  dvlog2  26888  advlog  26889  advlogexp  26890  logtayl  26895  logtayl2  26897  logccv  26898  cxpval  26899  1cxp  26907  cxpcl  26909  cxpp1  26915  cxpsqrt  26938  dvsqrt  26977  dvcnsqrt  26979  sqrtcn  26985  cxpaddlelem  26986  root1id  26989  root1cj  26991  logrec  26998  logb1  27004  logbmpt  27023  ang180lem1  27044  ang180lem2  27045  ang180lem3  27046  isosctrlem1  27053  isosctrlem2  27054  1cubrlem  27076  1cubr  27077  mcubic  27082  binom4  27085  dquartlem1  27086  quartlem1  27092  asinlem  27103  asinlem2  27104  asinlem3a  27105  asinlem3  27106  asinf  27107  atandm2  27112  atandm4  27114  atanf  27115  asinneg  27121  efiasin  27123  sinasin  27124  asinsin  27127  asin1  27129  acos1  27130  reasinsin  27131  asinbnd  27134  cosasin  27139  atanneg  27142  atancj  27145  efiatan  27147  atanlogaddlem  27148  atanlogadd  27149  atanlogsublem  27150  atanlogsub  27151  efiatan2  27152  2efiatan  27153  tanatan  27154  cosatan  27156  cosatanne0  27157  atantan  27158  atanbndlem  27160  bndatandm  27164  atans2  27166  dvatan  27170  atantayl  27172  atantayl2  27173  atantayl3  27174  leibpilem2  27176  leibpi  27177  log2cnv  27179  log2tlbnd  27180  log2ublem3  27183  log2ub  27184  birthdaylem2  27187  birthday  27189  efrlim  27204  dfef2  27205  cvxcl  27219  scvxcvx  27220  emcllem2  27231  emcllem4  27233  emcllem7  27236  harmonicbnd4  27245  fsumharmonic  27246  zetacvg  27249  lgamcvg2  27289  lgam1  27298  gam1  27299  wilthlem1  27302  wilthlem2  27303  wilthlem3  27304  basellem2  27316  basellem5  27319  basellem6  27320  basellem7  27321  basellem8  27322  basellem9  27323  0sgm  27378  mule1  27382  ppiprm  27385  ppinprm  27386  chtprm  27387  chtnprm  27388  chpp1  27389  mumullem2  27414  1sgmprm  27433  1sgm2ppw  27434  ppiub  27438  chtublem  27445  chtub  27446  logfaclbnd  27456  logfacbnd3  27457  logfacrlim  27458  logexprlim  27459  mersenne  27461  perfect1  27462  perfectlem1  27463  perfectlem2  27464  perfect  27465  dchrelbasd  27473  dchrmullid  27486  dchrfi  27489  dchrsum2  27502  sumdchr2  27504  bcp1ctr  27513  bposlem8  27525  zabsle1  27530  lgslem1  27531  lgslem2  27532  lgsfcl2  27537  lgsvalmod  27550  lgsneg  27555  lgsdilem  27558  lgsdir2lem1  27559  lgsdir2lem2  27560  lgsdir2lem3  27561  lgsdir2lem5  27563  lgsdir2  27564  lgsdir  27566  lgsdi  27568  lgsne0  27569  lgseisenlem1  27609  lgseisenlem2  27610  lgseisen  27613  lgsquadlem1  27614  lgsquadlem2  27615  lgsquad2lem1  27618  lgsquad2  27620  m1lgs  27622  2lgslem3c  27632  2lgsoddprmlem3c  27646  2lgsoddprmlem3d  27647  2sqlem10  27662  2sqlem11  27663  2sqblem  27665  addsqn2reu  27675  addsqrexnreu  27676  addsqnreup  27677  chtppilimlem2  27708  chebbnd2  27711  chto1lb  27712  rplogsumlem1  27718  rpvmasumlem  27721  dchrmusumlema  27727  dchrmusum2  27728  dchrisum0flblem1  27742  rpvmasum2  27746  mudivsum  27764  mulogsum  27766  vmalogdivsum2  27772  selberg2lem  27784  logdivbnd  27790  pntrmax  27798  pntrsumo1  27799  pntrsumbnd2  27801  pntrlog2bndlem5  27815  pntpbnd1a  27819  pntpbnd2  27821  pntibndlem2  27825  pntlemd  27828  pntlemc  27829  pntlemr  27836  brbtwn2  29348  colinearalglem4  29352  ax5seglem1  29371  ax5seglem2  29372  ax5seglem3  29374  ax5seglem5  29376  ax5seglem7  29378  ax5seglem9  29380  axbtwnid  29382  axpaschlem  29383  axlowdimlem13  29397  axlowdimlem14  29398  axlowdimlem16  29400  axeuclidlem  29405  axcontlem2  29408  axcontlem4  29410  axcontlem7  29413  axcontlem8  29414  crctcshwlkn0lem6  30269  clwwlkf1  30505  clwwlknonex2lem2  30564  ex-fl  30913  ex-ind-dvds  30927  vc2OLD  31035  vc0  31041  vcm  31043  nvm1  31132  nvmtri  31138  nvge0  31140  ipval2lem3  31172  ipidsq  31177  lnoadd  31225  ip1ilem  31293  ip1i  31294  ip2i  31295  ipdirilem  31296  ipasslem1  31298  ipasslem2  31299  ipasslem10  31306  minvecolem2  31342  hvsubid  31493  hv2times  31528  hisubcomi  31571  normlem9  31585  normlem7tALT  31586  norm-ii-i  31604  normsubi  31608  hhssnv  31731  pjhthlem1  31858  h1de2bi  32021  homullid  32267  ho2times  32286  lnop0  32433  lnopaddi  32438  lnophmlem2  32484  lnfn0i  32509  lnfnaddi  32510  hst1h  32694  sto2i  32704  stadd3i  32715  addltmulALT  32913  dpmul4  33346  psgnid  33524  cnmsgn0g  33573  altgnsg  33576  isarchi3  33614  archirngz  33616  1fldgenq  33750  ply1dg3rt0irred  33981  esplyfvaln  34071  ccfldextdgrr  34169  constrsscn  34237  constrabscl  34275  cos9thpiminplylem1  34279  cos9thpiminplylem4  34282  cos9thpiminplylem5  34283  lmatfvlem  34312  qqhval2lem  34478  dya2ub  34768  omssubadd  34798  eulerpartlemgs2  34878  fib5  34903  fib6  34904  ballotlem2  34987  signswch  35056  signlem0  35082  itgexpif  35101  reprlt  35114  breprexp  35128  breprexpnat  35129  hgt750lem2  35147  subfacp1lem5  35750  subfacp1lem6  35751  subfacval2  35753  subfaclim  35754  subfacval3  35755  cvxsconn  35809  resconn  35812  cvmliftlem7  35857  cvmliftlem10  35860  problem4  36234  sinccvglem  36238  sqdivzi  36294  faclimlem1  36309  dnibndlem5  37166  dnibndlem10  37171  ltflcei  38349  sin2h  38351  cos2h  38352  tan2h  38353  poimirlem13  38369  poimirlem16  38372  poimirlem17  38373  poimirlem19  38375  poimirlem20  38376  poimirlem31  38387  mblfinlem2  38394  mblfinlem3  38395  dvtan  38406  itg2addnclem3  38409  dvasin  38440  dvacos  38441  areacirc  38449  fdc  38482  mettrifi  38494  heiborlem4  38551  heiborlem6  38553  60gcd7e1  42858  lcmineqlem1  42882  lcmineqlem8  42889  lcmineqlem9  42890  lcmineqlem10  42891  lcmineqlem12  42893  3exp7  42906  3lexlogpow5ineq1  42907  3lexlogpow5ineq5  42913  aks4d1p1p4  42924  aks4d1p1p7  42927  aks4d1p1  42929  facp2  42996  25or6to4  43059  1p3e4  43113  1p4e5  43114  1p5e6  43115  1p6e7  43116  1p7e8  43117  1p8e9  43118  2p3e5  43119  4p5e9  43127  sn-1ne2  43133  sqdeccom12  43151  235t711  43167  sin2t3rdpi  43215  cos2t3rdpi  43216  re1m1e0m0  43259  ipiiie0  43300  sn-0tie0  43326  fltnltalem  43495  sum9cubes  43505  3cubeslem3l  43518  3cubeslem3r  43519  eldioph2lem1  43592  lzenom  43602  irrapxlem1  43650  rmspecsqrtnq  43734  rmxm1  43762  rmym1  43763  2nn0ind  43773  jm2.24nn  43787  jm2.17a  43788  jm2.17b  43789  jm2.17c  43790  jm2.24  43791  acongeq  43811  jm2.18  43816  jm2.27c  43835  jm3.1lem2  43846  rngunsnply  43997  flcidc  43998  inductionexd  44982  unitadd  45022  hashnzfzclim  45133  ofdivrec  45137  lhe4.4ex1a  45140  expgrowth  45146  dvradcnv2  45158  binomcxplemrat  45161  binomcxplemnotnn0  45167  isosctrlem1ALT  45743  monoord2xrv  46298  dvsinax  46728  dvnprodlem3  46763  itgsin0pilem1  46765  itgsbtaddcnst  46797  stoweidlem13  46828  stoweidlem26  46841  stoweidlem34  46849  stoweidlem38  46853  wallispilem2  46881  wallispilem4  46883  wallispi2lem1  46886  stirlinglem1  46889  stirlinglem5  46893  stirlinglem10  46898  dirkerper  46911  dirkertrigeqlem1  46913  dirkertrigeqlem3  46915  dirkertrigeq  46916  dirkercncflem4  46921  fourierdlem24  46946  sqwvfoura  47043  sqwvfourb  47044  fourierswlem  47045  cos5t  47730  goldpolyfactor  47732  goldratmolem2  47738  goldratmolem4  47740  goldratval  47741  lambert0  47742  lamberte  47743  cjnpoly  47744  sqrtnpoly  47748  1t10e1p1e11  48185  ceil5half3  48221  modm2nep1  48247  modm1nep2  48249  modm1nem2  48250  fmtnorec3  48438  fmtno5lem4  48446  fmtno5  48447  257prm  48451  fmtno4nprmfac193  48464  m3prm  48482  139prmALT  48486  127prm  48489  m7prm  48490  lighneallem3  48497  proththd  48504  3exp4mod41  48506  41prothprmlem2  48508  perfectALTVlem2  48625  perfectALTV  48626  11t31e341  48635  evengpop3  48701  nnsum4primeseven  48703  nnsum4primesevenALTV  48704  bgoldbtbndlem1  48708  0nodd  49072  altgsumbcALT  49270  exple2lt6  49281  nn0sumshdiglemB  49537  ackval3  49600  ackval3012  49609  line2ylem  49668  onetansqsecsq  50674  cotsqcscsq  50675  dvsec  50676  dvcsc  50677  dvcot  50678  5m4e1  50755