Axiom ax-1cn 11084

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

This axiom is referenced by:  0cn  11124  1cnd  11127  1ex  11128  mulrid  11130  mullid  11131  1re  11132  0re  11134  muladd11  11303  peano2cn  11305  mul02lem2  11310  addrid  11313  cnegex2  11315  peano2cnm  11447  0reALT  11478  ine0  11572  mulm1  11578  0lt1  11659  ixi  11766  muleqadd  11781  reccl  11803  recne0  11809  recid  11810  recid2  11811  diveq1  11826  div1  11831  1div1e1  11832  recdiv  11847  divdiv1  11852  divdiv2  11853  recdiv2  11854  conjmul  11858  eqneg  11861  div2neg  11864  recp1lt1  12040  recreclt  12041  recgt0ii  12048  neg1cn  12130  neg1ne0  12132  negneg1e1  12134  ofnegsub  12143  peano5nni  12148  nnsscn  12150  nn1m1nn  12166  nn1suc  12167  nnaddcl  12168  nnmulcl  12169  nnne0  12179  nnsub  12189  1m1e0  12217  2cn  12220  3cn  12226  4cn  12230  5cn  12233  6cn  12236  7cn  12239  8cn  12242  9cn  12245  1pneg1e0  12259  1m0e1  12261  0p1e1  12262  1p0e1  12264  2m1e1  12266  3m1e2  12268  4m1e3  12269  5m1e4  12270  6m1e5  12271  7m1e6  12272  8m1e7  12273  9m1e8  12274  2p2e4  12275  1p2e3  12283  1p2e3ALT  12284  3p2e5  12291  3p3e6  12292  4p2e6  12293  4p3e7  12294  4p4e8  12295  5p2e7  12296  5p3e8  12297  5p4e9  12298  6p2e8  12299  6p3e9  12300  7p2e9  12301  1t1e1  12302  3t3e9  12307  neg1mulneg1e1  12353  1mhlfehlf  12360  8th4div3  12361  halfthird  12362  halfpm6th  12363  addltmul  12377  elnn0nn  12443  elz2  12506  zlem1lt  12543  zltlem1  12544  nnaddm1cl  12549  zextlt  12566  zeo  12578  peano5uzi  12581  numsuc  12621  numltc  12633  numsucc  12647  numaddc  12655  6p5lem  12677  5p5e10  12678  6p4e10  12679  7p3e10  12682  8p2e10  12687  10m1e9  12703  4t3lem  12704  7t4e28  12718  9t11e99  12737  decbin2  12748  5recm6rec  12750  uzp1  12788  peano2uzr  12816  uzaddcl  12817  rebtwnz  12860  qbtwnre  13114  iccf1o  13412  fz01en  13468  fztp  13496  fzsuc2  13498  fztpval  13502  fseq1m1p1  13515  elfzp1b  13517  predfz  13569  fzoss2  13603  fzval3  13650  fzosplitsnm1  13656  fzo1to4tp  13670  fldiv4p1lem1div2  13755  ceim1l  13767  fldiv  13780  uzrdgxfr  13890  fzen2  13892  nn0ennn  13902  seqm1  13942  seqshft2  13951  monoord2  13956  sermono  13957  seqf1olem1  13964  seqf1olem2  13965  seqz  13973  ser1const  13981  expcl  14002  expclzlem  14006  m1expcl2  14008  expm1t  14013  1exp  14014  mulexpz  14025  expadd  14027  expaddz  14029  expmul  14030  expubnd  14101  sqrecii  14106  neg1sqe1  14119  irec  14124  i4  14127  binom21  14142  sq01  14148  crreczi  14151  bernneq  14152  bernneq2  14153  nn0opthlem1  14191  facndiv  14211  faclbnd4lem1  14216  faclbnd6  14222  bcnp1n  14237  bcm1k  14238  bcp1nk  14240  bcn2  14242  bcp1m1  14243  bcpasc  14244  hashgadd  14300  hashfz  14350  hashfzo  14352  hashxplem  14356  hashbclem  14375  hashf1  14380  seqcoll  14387  swrds1  14590  swrdlsw  14591  wrdind  14645  wrd2ind  14646  swrds2  14863  relexpaddg  14976  rei  15079  imi  15080  recan  15260  iserex  15580  isercoll2  15592  serf0  15604  iseraltlem2  15606  iseraltlem3  15607  iseralt  15608  sumrblem  15634  fsumm1  15674  telfsumo  15725  fsumparts  15729  hashiun  15745  binomlem  15752  binom  15753  binom1p  15754  binom11  15755  binom1dif  15756  bcxmas  15758  isumsplit  15763  isum1p  15764  climcndslem1  15772  supcvg  15779  harmonic  15782  arisum  15783  arisum2  15784  trireciplem  15785  geoserg  15789  geolim  15793  geolim2  15794  georeclim  15795  geo2sum  15796  geo2sum2  15797  geoisum1c  15803  0.999...  15804  geoihalfsum  15805  cvgrat  15806  mertenslem1  15807  mertenslem2  15808  mertens  15809  prodf1  15814  prodfclim1  15816  prodrblem  15852  fprodcvg  15853  prodmolem2a  15857  zprod  15860  fprodntriv  15865  prodss  15870  fprodss  15871  fprodsplit  15889  fprodn0f  15914  risefaccl  15938  fallfaccl  15939  risefacfac  15958  binomfallfac  15964  bpolycl  15975  bpolysum  15976  bpolydiflem  15977  fsumkthpow  15979  bpoly2  15980  bpoly3  15981  bpoly4  15982  fsumcube  15983  esum  16003  ege2le3  16013  efsub  16025  efexp  16026  efzval  16027  eftlub  16034  effsumlt  16036  ef4p  16038  tanval3  16059  efi4p  16062  tan0  16076  efival  16077  tanadd  16092  cos2t  16103  cos2tsin  16104  ef01bndlem  16109  cos1bnd  16112  cos2bnd  16113  demoivreALT  16126  eirrlem  16129  rpnnen2lem3  16141  rpnnen2lem11  16149  ruclem12  16166  3dvds  16258  3dvdsdec  16259  3dvds2dec  16260  odd2np1lem  16267  odd2np1  16268  opoe  16290  omoe  16291  opeo  16292  omeo  16293  n2dvdsm1  16296  m1exp1  16303  flodddiv4  16342  bitsfzo  16362  sqgcd  16489  expgcd  16490  nn0seqcvgd  16497  prmind2  16612  hashdvds  16702  phiprmpw  16703  phiprm  16704  eulerthlem2  16709  iserodd  16763  sumhash  16824  fldivp1  16825  prmpwdvds  16832  pockthlem  16833  pockthi  16835  prmreclem4  16847  prmreclem6  16849  4sqlem11  16883  4sqlem19  16891  vdwapun  16902  vdwapid1  16903  vdwlem3  16911  vdwlem5  16913  vdwlem6  16914  vdwlem8  16916  vdwlem9  16917  vdwnnlem2  16924  ramub1lem1  16954  ramub1lem2  16955  ramcl  16957  prmo1  16965  dec5nprm  16994  prmlem0  17033  43prm  17049  83prm  17050  139prm  17051  163prm  17052  317prm  17053  631prm  17054  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  1259prm  17063  2503lem1  17064  2503lem2  17065  2503lem3  17066  2503prm  17067  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  4001prm  17072  gsumsgrpccat  18765  mulgnndir  19033  mulgneg2  19038  m1expaddsub  19427  sylow1lem1  19527  sylow2a  19548  efgsval2  19662  efgsrel  19663  efgsres  19667  cncrng  21343  cnfld1  21348  cnfld1OLD  21349  zsssubrg  21380  cnmgpid  21384  zringcyg  21424  mulgrhm2  21433  pzriprng1ALT  21451  cnmsgnsubg  21532  cnmsgnbas  21533  cnmsgngrp  21534  psgninv  21537  evpmodpmf1o  21551  psdmplcl  22105  blcvx  24742  iihalf2  24884  icopnfcnv  24896  iccpnfhmeo  24899  xrhmeo  24900  icccvx  24904  lebnumii  24921  reparphti  24952  reparphtiOLD  24953  pcoass  24980  pcorevlem  24982  pcorev2  24984  pi1xfrcnv  25013  cnstrcvs  25097  cncvs  25101  ncvsm1  25110  pjthlem1  25393  divcncf  25404  ovolunlem1a  25453  ovolunlem1  25454  ovolicc2lem4  25477  uniioombllem3  25542  uniioombllem4  25543  dyadovol  25550  vitalilem4  25568  mbf0  25591  iblcnlem1  25745  itgcnlem  25747  dvid  25875  dvexp  25913  dvexp2  25914  dvexp3  25938  dveflem  25939  dvlipcn  25955  dvcvx  25981  dvfsumle  25982  dvfsumleOLD  25983  dvfsumlem1  25988  degltp1le  26034  ply1divex  26098  fta1glem1  26129  plyaddlem1  26174  plymullem1  26175  coeidp  26225  dgrid  26226  dvply1  26247  dvply2g  26248  dvply2gOLD  26249  plyremlem  26268  fta1lem  26271  vieta1lem1  26274  vieta1lem2  26275  qaa  26287  iaa  26289  aalioulem3  26298  geolim3  26303  aaliou3lem2  26307  aaliou3lem7  26313  taylply2  26331  taylply2OLD  26332  dvradcnv  26386  pserdvlem2  26394  pserdv2  26396  abelthlem1  26397  abelthlem2  26398  abelthlem6  26402  abelthlem7  26404  abelth  26407  reeff1olem  26412  reeff1o  26413  efcvx  26415  sinhalfpilem  26428  eulerid  26439  cos2pi  26441  sincosq3sgn  26465  sincosq4sgn  26466  tangtx  26470  sincos4thpi  26478  sincos6thpi  26481  pigt3  26483  pige3ALT  26485  abssinper  26486  coskpi  26488  coseq1  26490  efeq1  26493  tanregt0  26504  logneg2  26580  logdivlti  26585  logcnlem4  26610  dvlog2lem  26617  dvlog2  26618  advlog  26619  advlogexp  26620  logtayl  26625  logtayl2  26627  logccv  26628  cxpval  26629  1cxp  26637  cxpcl  26639  cxpp1  26645  cxpsqrt  26668  dvsqrt  26707  dvcnsqrt  26709  sqrtcn  26716  cxpaddlelem  26717  root1id  26720  root1cj  26722  logrec  26729  logb1  26735  logbmpt  26754  ang180lem1  26775  ang180lem2  26776  ang180lem3  26777  isosctrlem1  26784  isosctrlem2  26785  1cubrlem  26807  1cubr  26808  mcubic  26813  binom4  26816  dquartlem1  26817  quartlem1  26823  asinlem  26834  asinlem2  26835  asinlem3a  26836  asinlem3  26837  asinf  26838  atandm2  26843  atandm4  26845  atanf  26846  asinneg  26852  efiasin  26854  sinasin  26855  asinsin  26858  asin1  26860  acos1  26861  reasinsin  26862  asinbnd  26865  cosasin  26870  atanneg  26873  atancj  26876  efiatan  26878  atanlogaddlem  26879  atanlogadd  26880  atanlogsublem  26881  atanlogsub  26882  efiatan2  26883  2efiatan  26884  tanatan  26885  cosatan  26887  cosatanne0  26888  atantan  26889  atanbndlem  26891  bndatandm  26895  atans2  26897  dvatan  26901  atantayl  26903  atantayl2  26904  atantayl3  26905  leibpilem2  26907  leibpi  26908  log2cnv  26910  log2tlbnd  26911  log2ublem3  26914  log2ub  26915  birthdaylem2  26918  birthday  26920  efrlim  26935  efrlimOLD  26936  dfef2  26937  cvxcl  26951  scvxcvx  26952  emcllem2  26963  emcllem4  26965  emcllem7  26968  harmonicbnd4  26977  fsumharmonic  26978  zetacvg  26981  lgamcvg2  27021  lgam1  27030  gam1  27031  wilthlem1  27034  wilthlem2  27035  wilthlem3  27036  basellem2  27048  basellem5  27051  basellem6  27052  basellem7  27053  basellem8  27054  basellem9  27055  0sgm  27110  mule1  27114  ppiprm  27117  ppinprm  27118  chtprm  27119  chtnprm  27120  chpp1  27121  mumullem2  27146  1sgmprm  27166  1sgm2ppw  27167  ppiub  27171  chtublem  27178  chtub  27179  logfaclbnd  27189  logfacbnd3  27190  logfacrlim  27191  logexprlim  27192  mersenne  27194  perfect1  27195  perfectlem1  27196  perfectlem2  27197  perfect  27198  dchrelbasd  27206  dchrmullid  27219  dchrfi  27222  dchrsum2  27235  sumdchr2  27237  bcp1ctr  27246  bposlem8  27258  zabsle1  27263  lgslem1  27264  lgslem2  27265  lgsfcl2  27270  lgsvalmod  27283  lgsneg  27288  lgsdilem  27291  lgsdir2lem1  27292  lgsdir2lem2  27293  lgsdir2lem3  27294  lgsdir2lem5  27296  lgsdir2  27297  lgsdir  27299  lgsdi  27301  lgsne0  27302  lgseisenlem1  27342  lgseisenlem2  27343  lgseisen  27346  lgsquadlem1  27347  lgsquadlem2  27348  lgsquad2lem1  27351  lgsquad2  27353  m1lgs  27355  2lgslem3c  27365  2lgsoddprmlem3c  27379  2lgsoddprmlem3d  27380  2sqlem10  27395  2sqlem11  27396  2sqblem  27398  addsqn2reu  27408  addsqrexnreu  27409  addsqnreup  27410  chtppilimlem2  27441  chebbnd2  27444  chto1lb  27445  rplogsumlem1  27451  rpvmasumlem  27454  dchrmusumlema  27460  dchrmusum2  27461  dchrisum0flblem1  27475  rpvmasum2  27479  mudivsum  27497  mulogsum  27499  vmalogdivsum2  27505  selberg2lem  27517  logdivbnd  27523  pntrmax  27531  pntrsumo1  27532  pntrsumbnd2  27534  pntrlog2bndlem5  27548  pntpbnd1a  27552  pntpbnd2  27554  pntibndlem2  27558  pntlemd  27561  pntlemc  27562  pntlemr  27569  brbtwn2  28978  colinearalglem4  28982  ax5seglem1  29001  ax5seglem2  29002  ax5seglem3  29004  ax5seglem5  29006  ax5seglem7  29008  ax5seglem9  29010  axbtwnid  29012  axpaschlem  29013  axlowdimlem13  29027  axlowdimlem14  29028  axlowdimlem16  29030  axeuclidlem  29035  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  axcontlem8  29044  crctcshwlkn0lem6  29888  clwwlkf1  30124  clwwlknonex2lem2  30183  ex-fl  30522  ex-ind-dvds  30536  vc2OLD  30643  vc0  30649  vcm  30651  nvm1  30740  nvmtri  30746  nvge0  30748  ipval2lem3  30780  ipidsq  30785  lnoadd  30833  ip1ilem  30901  ip1i  30902  ip2i  30903  ipdirilem  30904  ipasslem1  30906  ipasslem2  30907  ipasslem10  30914  minvecolem2  30950  hvsubid  31101  hv2times  31136  hisubcomi  31179  normlem9  31193  normlem7tALT  31194  norm-ii-i  31212  normsubi  31216  hhssnv  31339  pjhthlem1  31466  h1de2bi  31629  homullid  31875  ho2times  31894  lnop0  32041  lnopaddi  32046  lnophmlem2  32092  lnfn0i  32117  lnfnaddi  32118  hst1h  32302  sto2i  32312  stadd3i  32323  addltmulALT  32521  sgnneg  32914  dpmul4  32995  psgnid  33179  cnmsgn0g  33228  altgnsg  33231  isarchi3  33269  archirngz  33271  1fldgenq  33404  ply1dg3rt0irred  33665  ccfldextdgrr  33829  constrsscn  33897  constrabscl  33935  cos9thpiminplylem1  33939  cos9thpiminplylem4  33942  cos9thpiminplylem5  33943  lmatfvlem  33972  qqhval2lem  34138  dya2ub  34427  omssubadd  34457  eulerpartlemgs2  34537  fib5  34562  fib6  34563  ballotlem2  34646  signswch  34718  signlem0  34744  itgexpif  34763  reprlt  34776  breprexp  34790  breprexpnat  34791  hgt750lem2  34809  subfacp1lem5  35378  subfacp1lem6  35379  subfacval2  35381  subfaclim  35382  subfacval3  35383  cvxsconn  35437  resconn  35440  cvmliftlem7  35485  cvmliftlem10  35488  problem4  35862  sinccvglem  35866  sqdivzi  35922  faclimlem1  35937  dnibndlem5  36682  dnibndlem10  36687  ltflcei  37805  sin2h  37807  cos2h  37808  tan2h  37809  poimirlem13  37830  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem20  37837  poimirlem31  37848  mblfinlem2  37855  mblfinlem3  37856  dvtan  37867  itg2addnclem3  37870  dvasin  37901  dvacos  37902  areacirc  37910  fdc  37942  mettrifi  37954  heiborlem4  38011  heiborlem6  38013  60gcd7e1  42255  lcmineqlem1  42279  lcmineqlem8  42286  lcmineqlem9  42287  lcmineqlem10  42288  lcmineqlem12  42290  3exp7  42303  3lexlogpow5ineq1  42304  3lexlogpow5ineq5  42310  aks4d1p1p4  42321  aks4d1p1p7  42324  aks4d1p1  42326  facp2  42393  1p3e4  42510  sn-1ne2  42516  sqdeccom12  42540  235t711  42556  sin2t3rdpi  42604  cos2t3rdpi  42605  re1m1e0m0  42648  ipiiie0  42689  sn-0tie0  42702  fltnltalem  42901  sum9cubes  42911  3cubeslem3l  42924  3cubeslem3r  42925  eldioph2lem1  42998  lzenom  43008  irrapxlem1  43060  rmspecsqrtnq  43144  rmxm1  43172  rmym1  43173  2nn0ind  43183  jm2.24nn  43197  jm2.17a  43198  jm2.17b  43199  jm2.17c  43200  jm2.24  43201  acongeq  43221  jm2.18  43226  jm2.27c  43245  jm3.1lem2  43256  rngunsnply  43407  flcidc  43408  inductionexd  44392  unitadd  44432  hashnzfzclim  44559  ofdivrec  44563  lhe4.4ex1a  44566  expgrowth  44572  dvradcnv2  44584  binomcxplemrat  44587  binomcxplemnotnn0  44593  isosctrlem1ALT  45170  monoord2xrv  45723  dvsinax  46153  dvnprodlem3  46188  itgsin0pilem1  46190  itgsbtaddcnst  46222  stoweidlem13  46253  stoweidlem26  46266  stoweidlem34  46274  stoweidlem38  46278  wallispilem2  46306  wallispilem4  46308  wallispi2lem1  46311  stirlinglem1  46314  stirlinglem5  46318  stirlinglem10  46323  dirkerper  46336  dirkertrigeqlem1  46338  dirkertrigeqlem3  46340  dirkertrigeq  46341  dirkercncflem4  46346  fourierdlem24  46371  sqwvfoura  46468  sqwvfourb  46469  fourierswlem  46470  lambert0  47129  lamberte  47130  cjnpoly  47131  1t10e1p1e11  47552  ceil5half3  47582  modm2nep1  47608  modm1nep2  47610  modm1nem2  47611  fmtnorec3  47790  fmtno5lem4  47798  fmtno5  47799  257prm  47803  fmtno4nprmfac193  47816  m3prm  47834  139prmALT  47838  127prm  47841  m7prm  47842  lighneallem3  47849  proththd  47856  3exp4mod41  47858  41prothprmlem2  47860  perfectALTVlem2  47964  perfectALTV  47965  11t31e341  47974  evengpop3  48040  nnsum4primeseven  48042  nnsum4primesevenALTV  48043  bgoldbtbndlem1  48047  0nodd  48412  altgsumbcALT  48595  exple2lt6  48606  nn0sumshdiglemB  48862  ackval3  48925  ackval3012  48934  line2ylem  48993  onetansqsecsq  50002  cotsqcscsq  50003  5m4e1  50038