Axiom ax-1cn 11197

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

This axiom is referenced by:  0cn  11237  1cnd  11240  1ex  11241  mulrid  11243  mullid  11244  1re  11245  0re  11247  muladd11  11415  peano2cn  11417  mul02lem2  11422  addrid  11425  cnegex2  11427  peano2cnm  11557  0reALT  11588  ine0  11680  mulm1  11686  0lt1  11767  ixi  11874  muleqadd  11889  reccl  11910  recne0  11916  recid  11917  recid2  11918  div1  11934  1div1e1  11935  diveq1  11936  recdiv  11951  divdiv1  11956  divdiv2  11957  recdiv2  11958  conjmul  11962  eqneg  11965  div2neg  11968  recp1lt1  12143  recreclt  12144  recgt0ii  12151  inelr  12233  ofnegsub  12241  peano5nni  12246  nnsscn  12248  nn1m1nn  12264  nn1suc  12265  nnaddcl  12266  nnmulcl  12267  nnne0  12277  nnsub  12287  1m1e0  12315  2cn  12318  3cn  12324  4cn  12328  5cn  12331  6cn  12334  7cn  12337  8cn  12340  9cn  12343  neg1cn  12357  neg1ne0  12359  negneg1e1  12361  1pneg1e0  12362  1m0e1  12364  0p1e1  12365  1p0e1  12367  2m1e1  12369  3m1e2  12371  4m1e3  12372  5m1e4  12373  6m1e5  12374  7m1e6  12375  8m1e7  12376  9m1e8  12377  2p2e4  12378  1p2e3  12386  1p2e3ALT  12387  3p2e5  12394  3p3e6  12395  4p2e6  12396  4p3e7  12397  4p4e8  12398  5p2e7  12399  5p3e8  12400  5p4e9  12401  6p2e8  12402  6p3e9  12403  7p2e9  12404  1t1e1  12405  3t3e9  12410  neg1mulneg1e1  12456  1mhlfehlf  12462  8th4div3  12463  halfpm6th  12464  addltmul  12479  elnn0nn  12545  elz2  12607  zlem1lt  12645  zltlem1  12646  nnaddm1cl  12650  zextlt  12667  zeo  12679  peano5uzi  12682  numsuc  12722  numltc  12734  numsucc  12748  numaddc  12756  6p5lem  12778  5p5e10  12779  6p4e10  12780  7p3e10  12783  8p2e10  12788  10m1e9  12804  4t3lem  12805  7t4e28  12819  9t11e99  12838  decbin2  12849  halfthird  12851  5recm6rec  12852  uzp1  12894  peano2uzr  12918  uzaddcl  12919  rebtwnz  12962  qbtwnre  13211  iccf1o  13506  fz01en  13562  fztp  13590  fzsuc2  13592  fztpval  13596  fseq1m1p1  13609  elfzp1b  13611  fz0to4untppr  13637  predfz  13659  fzoss2  13693  fzval3  13734  fzosplitsnm1  13740  fzo1to4tp  13753  fldiv4p1lem1div2  13833  ceim1l  13845  fldiv  13858  uzrdgxfr  13965  fzen2  13967  nn0ennn  13977  seqm1  14017  seqshft2  14026  monoord2  14031  sermono  14032  seqf1olem1  14039  seqf1olem2  14040  seqz  14048  ser1const  14056  expcl  14077  expclzlem  14081  m1expcl2  14083  expm1t  14088  1exp  14089  mulexpz  14100  expadd  14102  expaddz  14104  expmul  14105  expubnd  14174  sqrecii  14179  neg1sqe1  14192  irec  14197  i4  14200  binom21  14214  sq01  14220  crreczi  14223  bernneq  14224  bernneq2  14225  nn0opthlem1  14260  facndiv  14280  faclbnd4lem1  14285  faclbnd6  14291  bcnp1n  14306  bcm1k  14307  bcp1nk  14309  bcn2  14311  bcp1m1  14312  bcpasc  14313  hashgadd  14369  hashfz  14419  hashfzo  14421  hashxplem  14425  hashbclem  14444  hashf1  14451  seqcoll  14458  swrds1  14649  swrdlsw  14650  wrdind  14705  wrd2ind  14706  swrds2  14924  relexpaddg  15033  rei  15136  imi  15137  recan  15316  iserex  15636  isercoll2  15648  serf0  15660  iseraltlem2  15662  iseraltlem3  15663  iseralt  15664  sumrblem  15690  fsumm1  15730  telfsumo  15781  fsumparts  15785  hashiun  15801  binomlem  15808  binom  15809  binom1p  15810  binom11  15811  binom1dif  15812  bcxmas  15814  isumsplit  15819  isum1p  15820  climcndslem1  15828  supcvg  15835  harmonic  15838  arisum  15839  arisum2  15840  trireciplem  15841  geoserg  15845  geolim  15849  geolim2  15850  georeclim  15851  geo2sum  15852  geo2sum2  15853  geoisum1c  15859  0.999...  15860  geoihalfsum  15861  cvgrat  15862  mertenslem1  15863  mertenslem2  15864  mertens  15865  prodf1  15870  prodfclim1  15872  prodrblem  15906  fprodcvg  15907  prodmolem2a  15911  zprod  15914  fprodntriv  15919  prodss  15924  fprodss  15925  fprodsplit  15943  fprodn0f  15968  risefaccl  15992  fallfaccl  15993  risefacfac  16012  binomfallfac  16018  bpolycl  16029  bpolysum  16030  bpolydiflem  16031  fsumkthpow  16033  bpoly2  16034  bpoly3  16035  bpoly4  16036  fsumcube  16037  esum  16057  ege2le3  16067  efsub  16077  efexp  16078  efzval  16079  eftlub  16086  effsumlt  16088  ef4p  16090  tanval3  16111  efi4p  16114  tan0  16128  efival  16129  tanadd  16144  cos2t  16155  cos2tsin  16156  ef01bndlem  16161  cos1bnd  16164  cos2bnd  16165  demoivreALT  16178  eirrlem  16181  rpnnen2lem3  16193  rpnnen2lem11  16201  ruclem12  16218  3dvds  16308  3dvdsdec  16309  3dvds2dec  16310  odd2np1lem  16317  odd2np1  16318  opoe  16340  omoe  16341  opeo  16342  omeo  16343  n2dvdsm1  16346  m1exp1  16353  flodddiv4  16390  bitsfzo  16410  sqgcd  16536  nn0seqcvgd  16541  prmind2  16656  hashdvds  16744  phiprmpw  16745  phiprm  16746  eulerthlem2  16751  iserodd  16804  sumhash  16865  fldivp1  16866  prmpwdvds  16873  pockthlem  16874  pockthi  16876  prmreclem4  16888  prmreclem6  16890  4sqlem11  16924  4sqlem19  16932  vdwapun  16943  vdwapid1  16944  vdwlem3  16952  vdwlem5  16954  vdwlem6  16955  vdwlem8  16957  vdwlem9  16958  vdwnnlem2  16965  ramub1lem1  16995  ramub1lem2  16996  ramcl  16998  prmo1  17006  dec5nprm  17035  decexp2  17044  prmlem0  17075  43prm  17091  83prm  17092  139prm  17093  163prm  17094  317prm  17095  631prm  17096  1259lem2  17101  1259lem3  17102  1259lem4  17103  1259lem5  17104  1259prm  17105  2503lem1  17106  2503lem2  17107  2503lem3  17108  2503prm  17109  4001lem1  17110  4001lem2  17111  4001lem3  17112  4001lem4  17113  4001prm  17114  gsumsgrpccat  18792  mulgnndir  19058  mulgneg2  19063  m1expaddsub  19453  sylow1lem1  19553  sylow2a  19574  efgsval2  19688  efgsrel  19689  efgsres  19693  cncrng  21316  cnfld1  21321  cnfld1OLD  21322  zsssubrg  21358  cnmgpid  21362  zringcyg  21395  mulgrhm2  21404  pzriprng1ALT  21422  cnmsgnsubg  21509  cnmsgnbas  21510  cnmsgngrp  21511  psgninv  21514  evpmodpmf1o  21528  psdmplcl  22086  blcvx  24727  iihalf2  24868  icopnfcnv  24880  iccpnfhmeo  24883  xrhmeo  24884  icccvx  24888  lebnumii  24905  reparphti  24936  reparphtiOLD  24937  pcoass  24964  pcorevlem  24966  pcorev2  24968  pi1xfrcnv  24997  cnstrcvs  25081  cncvs  25085  ncvsm1  25095  pjthlem1  25378  divcncf  25389  ovolunlem1a  25438  ovolunlem1  25439  ovolicc2lem4  25462  uniioombllem3  25527  uniioombllem4  25528  dyadovol  25535  vitalilem4  25553  mbf0  25576  iblcnlem1  25730  itgcnlem  25732  dvid  25860  dvexp  25898  dvexp2  25899  dvexp3  25923  dveflem  25924  dvlipcn  25940  dvcvx  25966  dvfsumle  25967  dvfsumleOLD  25968  dvfsumlem1  25973  degltp1le  26022  ply1divex  26085  fta1glem1  26115  plyaddlem1  26160  plymullem1  26161  coeidp  26211  dgrid  26212  dvply1  26231  dvply2g  26232  dvply2gOLD  26233  plyremlem  26252  fta1lem  26255  vieta1lem1  26258  vieta1lem2  26259  qaa  26271  iaa  26273  aalioulem3  26282  geolim3  26287  aaliou3lem2  26291  aaliou3lem7  26297  taylply2  26315  taylply2OLD  26316  dvradcnv  26370  pserdvlem2  26378  pserdv2  26380  abelthlem1  26381  abelthlem2  26382  abelthlem6  26386  abelthlem7  26388  abelth  26391  reeff1olem  26396  reeff1o  26397  efcvx  26399  sinhalfpilem  26411  eulerid  26422  cos2pi  26424  sincosq3sgn  26448  sincosq4sgn  26449  tangtx  26453  sincos4thpi  26461  sincos6thpi  26463  pigt3  26465  pige3ALT  26467  abssinper  26468  coskpi  26470  coseq1  26472  efeq1  26475  tanregt0  26486  logneg2  26562  logdivlti  26567  logcnlem4  26592  dvlog2lem  26599  dvlog2  26600  advlog  26601  advlogexp  26602  logtayl  26607  logtayl2  26609  logccv  26610  cxpval  26611  1cxp  26619  cxpcl  26621  cxpp1  26627  cxpsqrt  26650  dvsqrt  26689  dvcnsqrt  26691  sqrtcn  26698  cxpaddlelem  26699  root1id  26702  root1cj  26704  logrec  26708  logb1  26714  logbmpt  26733  ang180lem1  26754  ang180lem2  26755  ang180lem3  26756  isosctrlem1  26763  isosctrlem2  26764  1cubrlem  26786  1cubr  26787  mcubic  26792  binom4  26795  dquartlem1  26796  quartlem1  26802  asinlem  26813  asinlem2  26814  asinlem3a  26815  asinlem3  26816  asinf  26817  atandm2  26822  atandm4  26824  atanf  26825  asinneg  26831  efiasin  26833  sinasin  26834  asinsin  26837  asin1  26839  acos1  26840  reasinsin  26841  asinbnd  26844  cosasin  26849  atanneg  26852  atancj  26855  efiatan  26857  atanlogaddlem  26858  atanlogadd  26859  atanlogsublem  26860  atanlogsub  26861  efiatan2  26862  2efiatan  26863  tanatan  26864  cosatan  26866  cosatanne0  26867  atantan  26868  atanbndlem  26870  bndatandm  26874  atans2  26876  dvatan  26880  atantayl  26882  atantayl2  26883  atantayl3  26884  leibpilem2  26886  leibpi  26887  log2cnv  26889  log2tlbnd  26890  log2ublem3  26893  log2ub  26894  birthdaylem2  26897  birthday  26899  efrlim  26914  efrlimOLD  26915  dfef2  26916  cvxcl  26930  scvxcvx  26931  emcllem2  26942  emcllem4  26944  emcllem7  26947  harmonicbnd4  26956  fsumharmonic  26957  zetacvg  26960  lgamcvg2  27000  lgam1  27009  gam1  27010  wilthlem1  27013  wilthlem2  27014  wilthlem3  27015  basellem2  27027  basellem5  27030  basellem6  27031  basellem7  27032  basellem8  27033  basellem9  27034  0sgm  27089  mule1  27093  ppiprm  27096  ppinprm  27097  chtprm  27098  chtnprm  27099  chpp1  27100  mumullem2  27125  1sgmprm  27145  1sgm2ppw  27146  ppiub  27150  chtublem  27157  chtub  27158  logfaclbnd  27168  logfacbnd3  27169  logfacrlim  27170  logexprlim  27171  mersenne  27173  perfect1  27174  perfectlem1  27175  perfectlem2  27176  perfect  27177  dchrelbasd  27185  dchrmullid  27198  dchrfi  27201  dchrsum2  27214  sumdchr2  27216  bcp1ctr  27225  bposlem8  27237  zabsle1  27242  lgslem1  27243  lgslem2  27244  lgsfcl2  27249  lgsvalmod  27262  lgsneg  27267  lgsdilem  27270  lgsdir2lem1  27271  lgsdir2lem2  27272  lgsdir2lem3  27273  lgsdir2lem5  27275  lgsdir2  27276  lgsdir  27278  lgsdi  27280  lgsne0  27281  lgseisenlem1  27321  lgseisenlem2  27322  lgseisen  27325  lgsquadlem1  27326  lgsquadlem2  27327  lgsquad2lem1  27330  lgsquad2  27332  m1lgs  27334  2lgslem3c  27344  2lgsoddprmlem3c  27358  2lgsoddprmlem3d  27359  2sqlem10  27374  2sqlem11  27375  2sqblem  27377  addsqn2reu  27387  addsqrexnreu  27388  addsqnreup  27389  chtppilimlem2  27420  chebbnd2  27423  chto1lb  27424  rplogsumlem1  27430  rpvmasumlem  27433  dchrmusumlema  27439  dchrmusum2  27440  dchrisum0flblem1  27454  rpvmasum2  27458  mudivsum  27476  mulogsum  27478  vmalogdivsum2  27484  selberg2lem  27496  logdivbnd  27502  pntrmax  27510  pntrsumo1  27511  pntrsumbnd2  27513  pntrlog2bndlem5  27527  pntpbnd1a  27531  pntpbnd2  27533  pntibndlem2  27537  pntlemd  27540  pntlemc  27541  pntlemr  27548  brbtwn2  28729  colinearalglem4  28733  ax5seglem1  28752  ax5seglem2  28753  ax5seglem3  28755  ax5seglem5  28757  ax5seglem7  28759  ax5seglem9  28761  axbtwnid  28763  axpaschlem  28764  axlowdimlem13  28778  axlowdimlem14  28779  axlowdimlem16  28781  axeuclidlem  28786  axcontlem2  28789  axcontlem4  28791  axcontlem7  28794  axcontlem8  28795  crctcshwlkn0lem6  29639  clwwlkf1  29872  clwwlknonex2lem2  29931  ex-fl  30270  ex-ind-dvds  30284  vc2OLD  30391  vc0  30397  vcm  30399  nvm1  30488  nvmtri  30494  nvge0  30496  ipval2lem3  30528  ipidsq  30533  lnoadd  30581  ip1ilem  30649  ip1i  30650  ip2i  30651  ipdirilem  30652  ipasslem1  30654  ipasslem2  30655  ipasslem10  30662  minvecolem2  30698  hvsubid  30849  hv2times  30884  hisubcomi  30927  normlem9  30941  normlem7tALT  30942  norm-ii-i  30960  normsubi  30964  hhssnv  31087  pjhthlem1  31214  h1de2bi  31377  homullid  31623  ho2times  31642  lnop0  31789  lnopaddi  31794  lnophmlem2  31840  lnfn0i  31865  lnfnaddi  31866  hst1h  32050  sto2i  32060  stadd3i  32071  addltmulALT  32269  dpmul4  32650  psgnid  32831  cnmsgn0g  32880  altgnsg  32883  isarchi3  32908  archirngz  32910  1fldgenq  33022  ccfldextdgrr  33360  lmatfvlem  33416  qqhval2lem  33582  dya2ub  33890  omssubadd  33920  eulerpartlemgs2  34000  fib5  34025  fib6  34026  ballotlem2  34108  sgnneg  34160  signswch  34193  signlem0  34219  itgexpif  34238  reprlt  34251  breprexp  34265  breprexpnat  34266  hgt750lem2  34284  subfacp1lem5  34794  subfacp1lem6  34795  subfacval2  34797  subfaclim  34798  subfacval3  34799  cvxsconn  34853  resconn  34856  cvmliftlem7  34901  cvmliftlem10  34904  problem4  35272  sinccvglem  35276  sqdivzi  35322  faclimlem1  35337  dnibndlem5  35957  dnibndlem10  35962  ltflcei  37081  sin2h  37083  cos2h  37084  tan2h  37085  poimirlem13  37106  poimirlem16  37109  poimirlem17  37110  poimirlem19  37112  poimirlem20  37113  poimirlem31  37124  mblfinlem2  37131  mblfinlem3  37132  dvtan  37143  itg2addnclem3  37146  dvasin  37177  dvacos  37178  areacirc  37186  fdc  37218  mettrifi  37230  heiborlem4  37287  heiborlem6  37289  60gcd7e1  41476  lcmineqlem1  41500  lcmineqlem8  41507  lcmineqlem9  41508  lcmineqlem10  41509  lcmineqlem12  41511  3exp7  41524  3lexlogpow5ineq1  41525  3lexlogpow5ineq5  41531  aks4d1p1p4  41542  aks4d1p1p7  41545  aks4d1p1  41547  facp2  41615  fac2xp3  41691  2xp3dxp2ge1d  41693  factwoffsmonot  41694  sn-1ne2  41840  sqdeccom12  41863  235t711  41867  expgcd  41894  re1m1e0m0  41952  ipiiie0  41992  sn-0tie0  41994  fltnltalem  42086  sum9cubes  42096  3cubeslem3l  42106  3cubeslem3r  42107  eldioph2lem1  42180  lzenom  42190  irrapxlem1  42242  rmspecsqrtnq  42326  rmxm1  42355  rmym1  42356  2nn0ind  42366  jm2.24nn  42380  jm2.17a  42381  jm2.17b  42382  jm2.17c  42383  jm2.24  42384  acongeq  42404  jm2.18  42409  jm2.27c  42428  jm3.1lem2  42439  rngunsnply  42597  flcidc  42598  inductionexd  43585  unitadd  43625  hashnzfzclim  43759  ofdivrec  43763  lhe4.4ex1a  43766  expgrowth  43772  dvradcnv2  43784  binomcxplemrat  43787  binomcxplemnotnn0  43793  isosctrlem1ALT  44373  monoord2xrv  44866  dvsinax  45301  dvnprodlem3  45336  itgsin0pilem1  45338  itgsbtaddcnst  45370  stoweidlem13  45401  stoweidlem26  45414  stoweidlem34  45422  stoweidlem38  45426  wallispilem2  45454  wallispilem4  45456  wallispi2lem1  45459  stirlinglem1  45462  stirlinglem5  45466  stirlinglem10  45471  dirkerper  45484  dirkertrigeqlem1  45486  dirkertrigeqlem3  45488  dirkertrigeq  45489  dirkercncflem4  45494  fourierdlem24  45519  sqwvfoura  45616  sqwvfourb  45617  fourierswlem  45618  1t10e1p1e11  46690  fmtnorec3  46888  fmtno5lem4  46896  fmtno5  46897  257prm  46901  fmtno4nprmfac193  46914  m3prm  46932  139prmALT  46936  127prm  46939  m7prm  46940  lighneallem3  46947  proththd  46954  3exp4mod41  46956  41prothprmlem2  46958  perfectALTVlem2  47062  perfectALTV  47063  11t31e341  47072  evengpop3  47138  nnsum4primeseven  47140  nnsum4primesevenALTV  47141  bgoldbtbndlem1  47145  0nodd  47232  altgsumbcALT  47417  exple2lt6  47428  nn0sumshdiglemB  47693  ackval3  47756  ackval3012  47765  line2ylem  47824  onetansqsecsq  48192  cotsqcscsq  48193  5m4e1  48230