Axiom ax-1cn 11088

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

This axiom is referenced by:  0cn  11128  1cnd  11131  1ex  11132  mulrid  11134  mullid  11135  1re  11136  0re  11138  muladd11  11307  peano2cn  11309  mul02lem2  11314  addrid  11317  cnegex2  11319  peano2cnm  11451  0reALT  11482  ine0  11576  mulm1  11582  0lt1  11663  ixi  11770  muleqadd  11785  reccl  11807  recne0  11813  recid  11814  recid2  11815  diveq1  11830  div1  11835  1div1e1  11836  recdiv  11851  divdiv1  11856  divdiv2  11857  recdiv2  11858  conjmul  11862  eqneg  11865  div2neg  11868  recp1lt1  12044  recreclt  12045  recgt0ii  12052  neg1cn  12134  neg1ne0  12136  negneg1e1  12138  ofnegsub  12147  peano5nni  12152  nnsscn  12154  nn1m1nn  12170  nn1suc  12171  nnaddcl  12172  nnmulcl  12173  nnne0  12183  nnsub  12193  1m1e0  12221  2cn  12224  3cn  12230  4cn  12234  5cn  12237  6cn  12240  7cn  12243  8cn  12246  9cn  12249  1pneg1e0  12263  1m0e1  12265  0p1e1  12266  1p0e1  12268  2m1e1  12270  3m1e2  12272  4m1e3  12273  5m1e4  12274  6m1e5  12275  7m1e6  12276  8m1e7  12277  9m1e8  12278  2p2e4  12279  1p2e3  12287  1p2e3ALT  12288  3p2e5  12295  3p3e6  12296  4p2e6  12297  4p3e7  12298  4p4e8  12299  5p2e7  12300  5p3e8  12301  5p4e9  12302  6p2e8  12303  6p3e9  12304  7p2e9  12305  1t1e1  12306  3t3e9  12311  neg1mulneg1e1  12357  1mhlfehlf  12364  8th4div3  12365  halfthird  12366  halfpm6th  12367  addltmul  12381  elnn0nn  12447  elz2  12510  zlem1lt  12547  zltlem1  12548  nnaddm1cl  12553  zextlt  12570  zeo  12582  peano5uzi  12585  numsuc  12625  numltc  12637  numsucc  12651  numaddc  12659  6p5lem  12681  5p5e10  12682  6p4e10  12683  7p3e10  12686  8p2e10  12691  10m1e9  12707  4t3lem  12708  7t4e28  12722  9t11e99  12741  decbin2  12752  5recm6rec  12754  uzp1  12792  peano2uzr  12820  uzaddcl  12821  rebtwnz  12864  qbtwnre  13118  iccf1o  13416  fz01en  13472  fztp  13500  fzsuc2  13502  fztpval  13506  fseq1m1p1  13519  elfzp1b  13521  predfz  13573  fzoss2  13607  fzval3  13654  fzosplitsnm1  13660  fzo1to4tp  13674  fldiv4p1lem1div2  13759  ceim1l  13771  fldiv  13784  uzrdgxfr  13894  fzen2  13896  nn0ennn  13906  seqm1  13946  seqshft2  13955  monoord2  13960  sermono  13961  seqf1olem1  13968  seqf1olem2  13969  seqz  13977  ser1const  13985  expcl  14006  expclzlem  14010  m1expcl2  14012  expm1t  14017  1exp  14018  mulexpz  14029  expadd  14031  expaddz  14033  expmul  14034  expubnd  14105  sqrecii  14110  neg1sqe1  14123  irec  14128  i4  14131  binom21  14146  sq01  14152  crreczi  14155  bernneq  14156  bernneq2  14157  nn0opthlem1  14195  facndiv  14215  faclbnd4lem1  14220  faclbnd6  14226  bcnp1n  14241  bcm1k  14242  bcp1nk  14244  bcn2  14246  bcp1m1  14247  bcpasc  14248  hashgadd  14304  hashfz  14354  hashfzo  14356  hashxplem  14360  hashbclem  14379  hashf1  14384  seqcoll  14391  swrds1  14594  swrdlsw  14595  wrdind  14649  wrd2ind  14650  swrds2  14867  relexpaddg  14980  rei  15083  imi  15084  recan  15264  iserex  15584  isercoll2  15596  serf0  15608  iseraltlem2  15610  iseraltlem3  15611  iseralt  15612  sumrblem  15638  fsumm1  15678  telfsumo  15729  fsumparts  15733  hashiun  15749  binomlem  15756  binom  15757  binom1p  15758  binom11  15759  binom1dif  15760  bcxmas  15762  isumsplit  15767  isum1p  15768  climcndslem1  15776  supcvg  15783  harmonic  15786  arisum  15787  arisum2  15788  trireciplem  15789  geoserg  15793  geolim  15797  geolim2  15798  georeclim  15799  geo2sum  15800  geo2sum2  15801  geoisum1c  15807  0.999...  15808  geoihalfsum  15809  cvgrat  15810  mertenslem1  15811  mertenslem2  15812  mertens  15813  prodf1  15818  prodfclim1  15820  prodrblem  15856  fprodcvg  15857  prodmolem2a  15861  zprod  15864  fprodntriv  15869  prodss  15874  fprodss  15875  fprodsplit  15893  fprodn0f  15918  risefaccl  15942  fallfaccl  15943  risefacfac  15962  binomfallfac  15968  bpolycl  15979  bpolysum  15980  bpolydiflem  15981  fsumkthpow  15983  bpoly2  15984  bpoly3  15985  bpoly4  15986  fsumcube  15987  esum  16007  ege2le3  16017  efsub  16029  efexp  16030  efzval  16031  eftlub  16038  effsumlt  16040  ef4p  16042  tanval3  16063  efi4p  16066  tan0  16080  efival  16081  tanadd  16096  cos2t  16107  cos2tsin  16108  ef01bndlem  16113  cos1bnd  16116  cos2bnd  16117  demoivreALT  16130  eirrlem  16133  rpnnen2lem3  16145  rpnnen2lem11  16153  ruclem12  16170  3dvds  16262  3dvdsdec  16263  3dvds2dec  16264  odd2np1lem  16271  odd2np1  16272  opoe  16294  omoe  16295  opeo  16296  omeo  16297  n2dvdsm1  16300  m1exp1  16307  flodddiv4  16346  bitsfzo  16366  sqgcd  16493  expgcd  16494  nn0seqcvgd  16501  prmind2  16616  hashdvds  16706  phiprmpw  16707  phiprm  16708  eulerthlem2  16713  iserodd  16767  sumhash  16828  fldivp1  16829  prmpwdvds  16836  pockthlem  16837  pockthi  16839  prmreclem4  16851  prmreclem6  16853  4sqlem11  16887  4sqlem19  16895  vdwapun  16906  vdwapid1  16907  vdwlem3  16915  vdwlem5  16917  vdwlem6  16918  vdwlem8  16920  vdwlem9  16921  vdwnnlem2  16928  ramub1lem1  16958  ramub1lem2  16959  ramcl  16961  prmo1  16969  dec5nprm  16998  prmlem0  17037  43prm  17053  83prm  17054  139prm  17055  163prm  17056  317prm  17057  631prm  17058  1259lem2  17063  1259lem3  17064  1259lem4  17065  1259lem5  17066  1259prm  17067  2503lem1  17068  2503lem2  17069  2503lem3  17070  2503prm  17071  4001lem1  17072  4001lem2  17073  4001lem3  17074  4001lem4  17075  4001prm  17076  gsumsgrpccat  18769  mulgnndir  19037  mulgneg2  19042  m1expaddsub  19431  sylow1lem1  19531  sylow2a  19552  efgsval2  19666  efgsrel  19667  efgsres  19671  cncrng  21347  cnfld1  21352  cnfld1OLD  21353  zsssubrg  21384  cnmgpid  21388  zringcyg  21428  mulgrhm2  21437  pzriprng1ALT  21455  cnmsgnsubg  21536  cnmsgnbas  21537  cnmsgngrp  21538  psgninv  21541  evpmodpmf1o  21555  psdmplcl  22109  blcvx  24746  iihalf2  24888  icopnfcnv  24900  iccpnfhmeo  24903  xrhmeo  24904  icccvx  24908  lebnumii  24925  reparphti  24956  reparphtiOLD  24957  pcoass  24984  pcorevlem  24986  pcorev2  24988  pi1xfrcnv  25017  cnstrcvs  25101  cncvs  25105  ncvsm1  25114  pjthlem1  25397  divcncf  25408  ovolunlem1a  25457  ovolunlem1  25458  ovolicc2lem4  25481  uniioombllem3  25546  uniioombllem4  25547  dyadovol  25554  vitalilem4  25572  mbf0  25595  iblcnlem1  25749  itgcnlem  25751  dvid  25879  dvexp  25917  dvexp2  25918  dvexp3  25942  dveflem  25943  dvlipcn  25959  dvcvx  25985  dvfsumle  25986  dvfsumleOLD  25987  dvfsumlem1  25992  degltp1le  26038  ply1divex  26102  fta1glem1  26133  plyaddlem1  26178  plymullem1  26179  coeidp  26229  dgrid  26230  dvply1  26251  dvply2g  26252  dvply2gOLD  26253  plyremlem  26272  fta1lem  26275  vieta1lem1  26278  vieta1lem2  26279  qaa  26291  iaa  26293  aalioulem3  26302  geolim3  26307  aaliou3lem2  26311  aaliou3lem7  26317  taylply2  26335  taylply2OLD  26336  dvradcnv  26390  pserdvlem2  26398  pserdv2  26400  abelthlem1  26401  abelthlem2  26402  abelthlem6  26406  abelthlem7  26408  abelth  26411  reeff1olem  26416  reeff1o  26417  efcvx  26419  sinhalfpilem  26432  eulerid  26443  cos2pi  26445  sincosq3sgn  26469  sincosq4sgn  26470  tangtx  26474  sincos4thpi  26482  sincos6thpi  26485  pigt3  26487  pige3ALT  26489  abssinper  26490  coskpi  26492  coseq1  26494  efeq1  26497  tanregt0  26508  logneg2  26584  logdivlti  26589  logcnlem4  26614  dvlog2lem  26621  dvlog2  26622  advlog  26623  advlogexp  26624  logtayl  26629  logtayl2  26631  logccv  26632  cxpval  26633  1cxp  26641  cxpcl  26643  cxpp1  26649  cxpsqrt  26672  dvsqrt  26711  dvcnsqrt  26713  sqrtcn  26720  cxpaddlelem  26721  root1id  26724  root1cj  26726  logrec  26733  logb1  26739  logbmpt  26758  ang180lem1  26779  ang180lem2  26780  ang180lem3  26781  isosctrlem1  26788  isosctrlem2  26789  1cubrlem  26811  1cubr  26812  mcubic  26817  binom4  26820  dquartlem1  26821  quartlem1  26827  asinlem  26838  asinlem2  26839  asinlem3a  26840  asinlem3  26841  asinf  26842  atandm2  26847  atandm4  26849  atanf  26850  asinneg  26856  efiasin  26858  sinasin  26859  asinsin  26862  asin1  26864  acos1  26865  reasinsin  26866  asinbnd  26869  cosasin  26874  atanneg  26877  atancj  26880  efiatan  26882  atanlogaddlem  26883  atanlogadd  26884  atanlogsublem  26885  atanlogsub  26886  efiatan2  26887  2efiatan  26888  tanatan  26889  cosatan  26891  cosatanne0  26892  atantan  26893  atanbndlem  26895  bndatandm  26899  atans2  26901  dvatan  26905  atantayl  26907  atantayl2  26908  atantayl3  26909  leibpilem2  26911  leibpi  26912  log2cnv  26914  log2tlbnd  26915  log2ublem3  26918  log2ub  26919  birthdaylem2  26922  birthday  26924  efrlim  26939  efrlimOLD  26940  dfef2  26941  cvxcl  26955  scvxcvx  26956  emcllem2  26967  emcllem4  26969  emcllem7  26972  harmonicbnd4  26981  fsumharmonic  26982  zetacvg  26985  lgamcvg2  27025  lgam1  27034  gam1  27035  wilthlem1  27038  wilthlem2  27039  wilthlem3  27040  basellem2  27052  basellem5  27055  basellem6  27056  basellem7  27057  basellem8  27058  basellem9  27059  0sgm  27114  mule1  27118  ppiprm  27121  ppinprm  27122  chtprm  27123  chtnprm  27124  chpp1  27125  mumullem2  27150  1sgmprm  27170  1sgm2ppw  27171  ppiub  27175  chtublem  27182  chtub  27183  logfaclbnd  27193  logfacbnd3  27194  logfacrlim  27195  logexprlim  27196  mersenne  27198  perfect1  27199  perfectlem1  27200  perfectlem2  27201  perfect  27202  dchrelbasd  27210  dchrmullid  27223  dchrfi  27226  dchrsum2  27239  sumdchr2  27241  bcp1ctr  27250  bposlem8  27262  zabsle1  27267  lgslem1  27268  lgslem2  27269  lgsfcl2  27274  lgsvalmod  27287  lgsneg  27292  lgsdilem  27295  lgsdir2lem1  27296  lgsdir2lem2  27297  lgsdir2lem3  27298  lgsdir2lem5  27300  lgsdir2  27301  lgsdir  27303  lgsdi  27305  lgsne0  27306  lgseisenlem1  27346  lgseisenlem2  27347  lgseisen  27350  lgsquadlem1  27351  lgsquadlem2  27352  lgsquad2lem1  27355  lgsquad2  27357  m1lgs  27359  2lgslem3c  27369  2lgsoddprmlem3c  27383  2lgsoddprmlem3d  27384  2sqlem10  27399  2sqlem11  27400  2sqblem  27402  addsqn2reu  27412  addsqrexnreu  27413  addsqnreup  27414  chtppilimlem2  27445  chebbnd2  27448  chto1lb  27449  rplogsumlem1  27455  rpvmasumlem  27458  dchrmusumlema  27464  dchrmusum2  27465  dchrisum0flblem1  27479  rpvmasum2  27483  mudivsum  27501  mulogsum  27503  vmalogdivsum2  27509  selberg2lem  27521  logdivbnd  27527  pntrmax  27535  pntrsumo1  27536  pntrsumbnd2  27538  pntrlog2bndlem5  27552  pntpbnd1a  27556  pntpbnd2  27558  pntibndlem2  27562  pntlemd  27565  pntlemc  27566  pntlemr  27573  brbtwn2  28982  colinearalglem4  28986  ax5seglem1  29005  ax5seglem2  29006  ax5seglem3  29008  ax5seglem5  29010  ax5seglem7  29012  ax5seglem9  29014  axbtwnid  29016  axpaschlem  29017  axlowdimlem13  29031  axlowdimlem14  29032  axlowdimlem16  29034  axeuclidlem  29039  axcontlem2  29042  axcontlem4  29044  axcontlem7  29047  axcontlem8  29048  crctcshwlkn0lem6  29892  clwwlkf1  30128  clwwlknonex2lem2  30187  ex-fl  30526  ex-ind-dvds  30540  vc2OLD  30647  vc0  30653  vcm  30655  nvm1  30744  nvmtri  30750  nvge0  30752  ipval2lem3  30784  ipidsq  30789  lnoadd  30837  ip1ilem  30905  ip1i  30906  ip2i  30907  ipdirilem  30908  ipasslem1  30910  ipasslem2  30911  ipasslem10  30918  minvecolem2  30954  hvsubid  31105  hv2times  31140  hisubcomi  31183  normlem9  31197  normlem7tALT  31198  norm-ii-i  31216  normsubi  31220  hhssnv  31343  pjhthlem1  31470  h1de2bi  31633  homullid  31879  ho2times  31898  lnop0  32045  lnopaddi  32050  lnophmlem2  32096  lnfn0i  32121  lnfnaddi  32122  hst1h  32306  sto2i  32316  stadd3i  32327  addltmulALT  32525  sgnneg  32916  dpmul4  32997  psgnid  33181  cnmsgn0g  33230  altgnsg  33233  isarchi3  33271  archirngz  33273  1fldgenq  33406  ply1dg3rt0irred  33667  ccfldextdgrr  33831  constrsscn  33899  constrabscl  33937  cos9thpiminplylem1  33941  cos9thpiminplylem4  33944  cos9thpiminplylem5  33945  lmatfvlem  33974  qqhval2lem  34140  dya2ub  34429  omssubadd  34459  eulerpartlemgs2  34539  fib5  34564  fib6  34565  ballotlem2  34648  signswch  34720  signlem0  34746  itgexpif  34765  reprlt  34778  breprexp  34792  breprexpnat  34793  hgt750lem2  34811  subfacp1lem5  35380  subfacp1lem6  35381  subfacval2  35383  subfaclim  35384  subfacval3  35385  cvxsconn  35439  resconn  35442  cvmliftlem7  35487  cvmliftlem10  35490  problem4  35864  sinccvglem  35868  sqdivzi  35924  faclimlem1  35939  dnibndlem5  36684  dnibndlem10  36689  ltflcei  37811  sin2h  37813  cos2h  37814  tan2h  37815  poimirlem13  37836  poimirlem16  37839  poimirlem17  37840  poimirlem19  37842  poimirlem20  37843  poimirlem31  37854  mblfinlem2  37861  mblfinlem3  37862  dvtan  37873  itg2addnclem3  37876  dvasin  37907  dvacos  37908  areacirc  37916  fdc  37948  mettrifi  37960  heiborlem4  38017  heiborlem6  38019  60gcd7e1  42327  lcmineqlem1  42351  lcmineqlem8  42358  lcmineqlem9  42359  lcmineqlem10  42360  lcmineqlem12  42362  3exp7  42375  3lexlogpow5ineq1  42376  3lexlogpow5ineq5  42382  aks4d1p1p4  42393  aks4d1p1p7  42396  aks4d1p1  42398  facp2  42465  1p3e4  42581  sn-1ne2  42587  sqdeccom12  42611  235t711  42627  sin2t3rdpi  42675  cos2t3rdpi  42676  re1m1e0m0  42719  ipiiie0  42760  sn-0tie0  42773  fltnltalem  42972  sum9cubes  42982  3cubeslem3l  42995  3cubeslem3r  42996  eldioph2lem1  43069  lzenom  43079  irrapxlem1  43131  rmspecsqrtnq  43215  rmxm1  43243  rmym1  43244  2nn0ind  43254  jm2.24nn  43268  jm2.17a  43269  jm2.17b  43270  jm2.17c  43271  jm2.24  43272  acongeq  43292  jm2.18  43297  jm2.27c  43316  jm3.1lem2  43327  rngunsnply  43478  flcidc  43479  inductionexd  44463  unitadd  44503  hashnzfzclim  44630  ofdivrec  44634  lhe4.4ex1a  44637  expgrowth  44643  dvradcnv2  44655  binomcxplemrat  44658  binomcxplemnotnn0  44664  isosctrlem1ALT  45241  monoord2xrv  45794  dvsinax  46224  dvnprodlem3  46259  itgsin0pilem1  46261  itgsbtaddcnst  46293  stoweidlem13  46324  stoweidlem26  46337  stoweidlem34  46345  stoweidlem38  46349  wallispilem2  46377  wallispilem4  46379  wallispi2lem1  46382  stirlinglem1  46385  stirlinglem5  46389  stirlinglem10  46394  dirkerper  46407  dirkertrigeqlem1  46409  dirkertrigeqlem3  46411  dirkertrigeq  46412  dirkercncflem4  46417  fourierdlem24  46442  sqwvfoura  46539  sqwvfourb  46540  fourierswlem  46541  lambert0  47200  lamberte  47201  cjnpoly  47202  1t10e1p1e11  47623  ceil5half3  47653  modm2nep1  47679  modm1nep2  47681  modm1nem2  47682  fmtnorec3  47861  fmtno5lem4  47869  fmtno5  47870  257prm  47874  fmtno4nprmfac193  47887  m3prm  47905  139prmALT  47909  127prm  47912  m7prm  47913  lighneallem3  47920  proththd  47927  3exp4mod41  47929  41prothprmlem2  47931  perfectALTVlem2  48035  perfectALTV  48036  11t31e341  48045  evengpop3  48111  nnsum4primeseven  48113  nnsum4primesevenALTV  48114  bgoldbtbndlem1  48118  0nodd  48483  altgsumbcALT  48666  exple2lt6  48677  nn0sumshdiglemB  48933  ackval3  48996  ackval3012  49005  line2ylem  49064  onetansqsecsq  50073  cotsqcscsq  50074  5m4e1  50109