Axiom ax-1cn 11164

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

This axiom is used by:  0cn  11204  1cnd  11208  1ex  11209  mulrid  11212  mullid  11213  1re  11214  0re  11216  muladd11  11386  peano2cn  11388  mul02lem2  11393  addrid  11396  cnegex2  11398  peano2cnm  11530  0reALT  11561  ine0  11655  mulm1  11661  0lt1  11742  ixi  11849  muleqadd  11864  reccl  11885  recne0  11891  recid  11892  recid2  11893  diveq1  11907  div1  11910  1div1e1  11911  recdiv  11927  divdiv1  11932  divdiv2  11933  recdiv2  11934  conjmul  11938  eqneg  11941  div2neg  11944  recp1lt1  12119  recreclt  12120  recgt0ii  12127  neg1cn  12209  neg1ne0  12211  negneg1e1  12213  ofnegsub  12222  peano5nni  12242  nnsscn  12244  nn1m1nn  12260  nn1suc  12261  nnaddcl  12262  nnmulcl  12263  nnne0  12276  nnsub  12286  1m1e0  12319  2cn  12322  3cn  12328  4cn  12332  5cn  12335  6cn  12338  7cn  12341  8cn  12344  9cn  12347  1pneg1e0  12364  1m0e1  12366  0p1e1  12367  1p0e1  12369  2m1e1  12371  2m1e1OLD  12372  3m1e2  12374  4m1e3  12375  5m1e4  12376  6m1e5  12377  7m1e6  12378  8m1e7  12379  9m1e8  12380  2p2e4  12381  1p2e3  12389  1p2e3ALT  12390  3p2e5  12397  3p3e6  12398  4p2e6  12399  4p3e7  12400  4p4e8  12401  5p2e7  12402  5p3e8  12403  5p4e9  12404  6p2e8  12405  6p3e9  12406  7p2e9  12407  1t1e1  12408  3t3e9  12414  neg1mulneg1e1  12462  1mhlfehlf  12469  8th4div3  12470  halfthird  12471  halfpm6th  12472  addltmul  12486  elnn0nn  12552  elz2  12615  zlem1lt  12652  zltlem1  12653  nnaddm1cl  12659  zextlt  12676  zeo  12688  peano5uzi  12691  numsuc  12731  numltc  12748  numsucc  12762  numaddc  12770  6p5lem  12792  5p5e10  12793  6p4e10  12794  7p3e10  12797  8p2e10  12802  10m1e9  12818  4t3lem  12819  7t4e28  12833  9t11e99OLD  12853  decbin2  12865  5recm6rec  12867  uzp1  12905  peano2uzr  12933  uzaddcl  12934  rebtwnz  12977  qbtwnre  13231  iccf1o  13529  fz01en  13587  fztp  13615  fzsuc2  13617  fztpval  13621  fseq1m1p1  13634  elfzp1b  13636  predfz  13688  fzoss2  13723  fzval3  13770  fzosplitsnm1  13776  fzo1to4tp  13790  fldiv4p1lem1div2  13875  ceim1l  13887  fldiv  13900  uzrdgxfr  14010  fzen2  14012  nn0ennn  14022  seqm1  14062  seqshft2  14071  monoord2  14076  sermono  14077  seqf1olem1  14084  seqf1olem2  14085  seqz  14093  ser1const  14101  expcl  14122  expclzlem  14126  m1expcl2  14128  expm1t  14133  1exp  14134  mulexpz  14145  expadd  14147  expaddz  14149  expmul  14150  expubnd  14221  sqrecii  14226  neg1sqe1  14239  irec  14244  i4  14247  binom21  14262  sq01  14268  crreczi  14271  bernneq  14272  bernneq2  14273  nn0opthlem1  14311  facndiv  14331  faclbnd4lem1  14336  faclbnd6  14342  bcnp1n  14357  bcm1k  14358  bcp1nk  14360  bcn2  14362  bcp1m1  14363  bcpasc  14364  hashgadd  14420  hashfz  14471  hashfzo  14473  hashxplem  14477  hashbclem  14496  hashf1  14501  seqcoll  14508  swrds1  14711  swrdlsw  14712  wrdind  14766  wrd2ind  14767  swrds2  14984  relexpaddg  15097  sgnneg  15144  rei  15214  imi  15215  recan  15395  iserex  15715  isercoll2  15727  serf0  15739  iseraltlem2  15741  iseraltlem3  15742  iseralt  15743  sumrblem  15769  fsumm1  15809  telfsumo  15861  fsumparts  15865  hashiun  15881  binomlem  15890  binom  15891  binom1p  15892  binom11  15893  binom1dif  15894  bcxmas  15896  isumsplit  15901  isum1p  15902  climcndslem1  15910  supcvg  15917  harmonic  15920  arisum  15921  arisum2  15922  trireciplem  15923  geoserg  15927  geolim  15931  geolim2  15932  georeclim  15933  geo2sum  15934  geo2sum2  15935  geoisum1c  15941  0.999...  15942  geoihalfsum  15943  cvgrat  15944  mertenslem1  15945  mertenslem2  15946  mertens  15947  prodf1  15952  prodfclim1  15954  prodrblem  15990  fprodcvg  15991  prodmolem2a  15995  zprod  15998  fprodntriv  16003  prodss  16008  fprodss  16009  fprodsplit  16027  fprodn0f  16052  risefaccl  16076  fallfaccl  16077  risefacfac  16095  binomfallfac  16101  bpolycl  16112  bpolysum  16113  bpolydiflem  16114  fsumkthpow  16116  bpoly2  16117  bpoly3  16118  bpoly4  16119  fsumcube  16120  esum  16140  ege2le3  16150  efsub  16162  efexp  16163  efzval  16164  eftlub  16171  effsumlt  16173  ef4p  16175  tanval3  16196  efi4p  16199  tan0  16213  efival  16214  tanadd  16229  cos2t  16240  cos2tsin  16241  ef01bndlem  16246  cos1bnd  16249  cos2bnd  16250  demoivreALT  16263  eirrlem  16266  rpnnen2lem3  16278  rpnnen2lem11  16286  ruclem12  16303  3dvds  16395  3dvdsdec  16396  3dvds2dec  16397  odd2np1lem  16404  odd2np1  16405  opoe  16427  omoe  16428  opeo  16429  omeo  16430  n2dvdsm1  16433  m1exp1  16440  flodddiv4  16479  bitsfzo  16499  sqgcd  16626  expgcd  16627  nn0seqcvgd  16634  prmind2  16749  hashdvds  16840  phiprmpw  16841  phiprm  16842  eulerthlem2  16847  iserodd  16901  sumhash  16962  fldivp1  16963  prmpwdvds  16970  pockthlem  16971  pockthi  16973  prmreclem4  16985  prmreclem6  16987  4sqlem11  17021  4sqlem19  17029  vdwapun  17040  vdwapid1  17041  vdwlem3  17049  vdwlem5  17051  vdwlem6  17052  vdwlem8  17054  vdwlem9  17055  vdwnnlem2  17062  ramub1lem1  17092  ramub1lem2  17093  ramcl  17095  prmo1  17103  dec5nprm  17132  prmlem0  17171  43prm  17188  83prm  17189  139prm  17190  163prm  17191  317prm  17192  631prm  17193  1259lem2  17198  1259lem3  17199  1259lem4  17200  1259lem5  17201  1259prm  17202  2503lem1  17203  2503lem2  17204  2503lem3  17205  2503prm  17206  4001lem1  17207  4001lem2  17208  4001lem3  17209  4001lem4  17210  4001prm  17211  gsumsgrpccat  18905  mulgnndir  19175  mulgneg2  19180  m1expaddsub  19574  sylow1lem1  19674  sylow2a  19695  efgsval2  19809  efgsrel  19810  efgsres  19814  cncrng  21554  cnfld1  21558  zsssubrg  21586  cnmgpid  21590  zringcyg  21630  mulgrhm2  21639  pzriprng1ALT  21657  cnmsgnsubg  21738  cnmsgnbas  21739  cnmsgngrp  21740  psgninv  21743  evpmodpmf1o  21757  psdmplcl  22336  blcvx  24966  iihalf2  25103  icopnfcnv  25112  iccpnfhmeo  25115  xrhmeo  25116  icccvx  25120  lebnumii  25136  reparphti  25167  pcoass  25194  pcorevlem  25196  pcorev2  25198  pi1xfrcnv  25227  cnstrcvs  25311  cncvs  25315  ncvsm1  25324  pjthlem1  25607  divcncf  25617  ovolunlem1a  25666  ovolunlem1  25667  ovolicc2lem4  25690  uniioombllem3  25755  uniioombllem4  25756  dyadovol  25763  vitalilem4  25781  mbf0  25804  iblcnlem1  25958  itgcnlem  25960  dvid  26088  dvexp  26123  dvexp2  26124  dvexp3  26148  dveflem  26149  dvlipcn  26164  dvcvx  26190  dvfsumle  26191  dvfsumlem1  26196  degltp1le  26241  ply1divex  26305  fta1glem1  26336  plyaddlem1  26381  plymullem1  26382  coeidp  26431  dgrid  26432  dvply1  26456  dvply2g  26457  plyremlem  26476  fta1lem  26479  vieta1lem1  26482  vieta1lem2  26483  qaa  26495  iaa  26499  aalioulem3  26508  geolim3  26513  aaliou3lem2  26517  aaliou3lem7  26523  taylply2  26542  dvradcnv  26595  pserdvlem2  26602  pserdv2  26604  abelthlem1  26605  abelthlem2  26606  abelthlem6  26610  abelthlem7  26612  abelth  26615  reeff1olem  26620  reeff1o  26621  efcvx  26623  sinhalfpilem  26639  eulerid  26650  cos2pi  26652  sincosq3sgn  26676  sincosq4sgn  26677  tangtx  26681  sincos4thpi  26689  sincos6thpi  26692  pigt3  26694  pige3ALT  26696  abssinper  26697  coskpi  26699  coseq1  26701  efeq1  26704  tanregt0  26715  logneg2  26791  logdivlti  26796  logcnlem4  26821  dvlog2lem  26828  dvlog2  26829  advlog  26830  advlogexp  26831  logtayl  26836  logtayl2  26838  logccv  26839  cxpval  26840  1cxp  26848  cxpcl  26850  cxpp1  26856  cxpsqrt  26879  dvsqrt  26918  dvcnsqrt  26920  sqrtcn  26926  cxpaddlelem  26927  root1id  26930  root1cj  26932  logrec  26939  logb1  26945  logbmpt  26964  ang180lem1  26985  ang180lem2  26986  ang180lem3  26987  isosctrlem1  26994  isosctrlem2  26995  1cubrlem  27017  1cubr  27018  mcubic  27023  binom4  27026  dquartlem1  27027  quartlem1  27033  asinlem  27044  asinlem2  27045  asinlem3a  27046  asinlem3  27047  asinf  27048  atandm2  27053  atandm4  27055  atanf  27056  asinneg  27062  efiasin  27064  sinasin  27065  asinsin  27068  asin1  27070  acos1  27071  reasinsin  27072  asinbnd  27075  cosasin  27080  atanneg  27083  atancj  27086  efiatan  27088  atanlogaddlem  27089  atanlogadd  27090  atanlogsublem  27091  atanlogsub  27092  efiatan2  27093  2efiatan  27094  tanatan  27095  cosatan  27097  cosatanne0  27098  atantan  27099  atanbndlem  27101  bndatandm  27105  atans2  27107  dvatan  27111  atantayl  27113  atantayl2  27114  atantayl3  27115  leibpilem2  27117  leibpi  27118  log2cnv  27120  log2tlbnd  27121  log2ublem3  27124  log2ub  27125  birthdaylem2  27128  birthday  27130  efrlim  27145  dfef2  27146  cvxcl  27160  scvxcvx  27161  emcllem2  27172  emcllem4  27174  emcllem7  27177  harmonicbnd4  27186  fsumharmonic  27187  zetacvg  27190  lgamcvg2  27230  lgam1  27239  gam1  27240  wilthlem1  27243  wilthlem2  27244  wilthlem3  27245  basellem2  27257  basellem5  27260  basellem6  27261  basellem7  27262  basellem8  27263  basellem9  27264  0sgm  27319  mule1  27323  ppiprm  27326  ppinprm  27327  chtprm  27328  chtnprm  27329  chpp1  27330  mumullem2  27355  1sgmprm  27374  1sgm2ppw  27375  ppiub  27379  chtublem  27386  chtub  27387  logfaclbnd  27397  logfacbnd3  27398  logfacrlim  27399  logexprlim  27400  mersenne  27402  perfect1  27403  perfectlem1  27404  perfectlem2  27405  perfect  27406  dchrelbasd  27414  dchrmullid  27427  dchrfi  27430  dchrsum2  27443  sumdchr2  27445  bcp1ctr  27454  bposlem8  27466  zabsle1  27471  lgslem1  27472  lgslem2  27473  lgsfcl2  27478  lgsvalmod  27491  lgsneg  27496  lgsdilem  27499  lgsdir2lem1  27500  lgsdir2lem2  27501  lgsdir2lem3  27502  lgsdir2lem5  27504  lgsdir2  27505  lgsdir  27507  lgsdi  27509  lgsne0  27510  lgseisenlem1  27550  lgseisenlem2  27551  lgseisen  27554  lgsquadlem1  27555  lgsquadlem2  27556  lgsquad2lem1  27559  lgsquad2  27561  m1lgs  27563  2lgslem3c  27573  2lgsoddprmlem3c  27587  2lgsoddprmlem3d  27588  2sqlem10  27603  2sqlem11  27604  2sqblem  27606  addsqn2reu  27616  addsqrexnreu  27617  addsqnreup  27618  chtppilimlem2  27649  chebbnd2  27652  chto1lb  27653  rplogsumlem1  27659  rpvmasumlem  27662  dchrmusumlema  27668  dchrmusum2  27669  dchrisum0flblem1  27683  rpvmasum2  27687  mudivsum  27705  mulogsum  27707  vmalogdivsum2  27713  selberg2lem  27725  logdivbnd  27731  pntrmax  27739  pntrsumo1  27740  pntrsumbnd2  27742  pntrlog2bndlem5  27756  pntpbnd1a  27760  pntpbnd2  27762  pntibndlem2  27766  pntlemd  27769  pntlemc  27770  pntlemr  27777  brbtwn2  29266  colinearalglem4  29270  ax5seglem1  29289  ax5seglem2  29290  ax5seglem3  29292  ax5seglem5  29294  ax5seglem7  29296  ax5seglem9  29298  axbtwnid  29300  axpaschlem  29301  axlowdimlem13  29315  axlowdimlem14  29316  axlowdimlem16  29318  axeuclidlem  29323  axcontlem2  29326  axcontlem4  29328  axcontlem7  29331  axcontlem8  29332  crctcshwlkn0lem6  30175  clwwlkf1  30411  clwwlknonex2lem2  30470  ex-fl  30809  ex-ind-dvds  30823  vc2OLD  30931  vc0  30937  vcm  30939  nvm1  31028  nvmtri  31034  nvge0  31036  ipval2lem3  31068  ipidsq  31073  lnoadd  31121  ip1ilem  31189  ip1i  31190  ip2i  31191  ipdirilem  31192  ipasslem1  31194  ipasslem2  31195  ipasslem10  31202  minvecolem2  31238  hvsubid  31389  hv2times  31424  hisubcomi  31467  normlem9  31481  normlem7tALT  31482  norm-ii-i  31500  normsubi  31504  hhssnv  31627  pjhthlem1  31754  h1de2bi  31917  homullid  32163  ho2times  32182  lnop0  32329  lnopaddi  32334  lnophmlem2  32380  lnfn0i  32405  lnfnaddi  32406  hst1h  32590  sto2i  32600  stadd3i  32611  addltmulALT  32809  dpmul4  33244  psgnid  33426  cnmsgn0g  33475  altgnsg  33478  isarchi3  33516  archirngz  33518  1fldgenq  33652  ply1dg3rt0irred  33883  esplyfvaln  33973  ccfldextdgrr  34071  constrsscn  34139  constrabscl  34177  cos9thpiminplylem1  34181  cos9thpiminplylem4  34184  cos9thpiminplylem5  34185  lmatfvlem  34214  qqhval2lem  34380  dya2ub  34669  omssubadd  34699  eulerpartlemgs2  34779  fib5  34804  fib6  34805  ballotlem2  34888  signswch  34957  signlem0  34983  itgexpif  35002  reprlt  35015  breprexp  35029  breprexpnat  35030  hgt750lem2  35048  subfacp1lem5  35684  subfacp1lem6  35685  subfacval2  35687  subfaclim  35688  subfacval3  35689  cvxsconn  35743  resconn  35746  cvmliftlem7  35791  cvmliftlem10  35794  problem4  36168  sinccvglem  36172  sqdivzi  36228  faclimlem1  36243  dnibndlem5  37099  dnibndlem10  37104  ltflcei  38287  sin2h  38289  cos2h  38290  tan2h  38291  poimirlem13  38312  poimirlem16  38315  poimirlem17  38316  poimirlem19  38318  poimirlem20  38319  poimirlem31  38330  mblfinlem2  38337  mblfinlem3  38338  dvtan  38349  itg2addnclem3  38352  dvasin  38383  dvacos  38384  areacirc  38392  fdc  38424  mettrifi  38436  heiborlem4  38493  heiborlem6  38495  60gcd7e1  42800  lcmineqlem1  42824  lcmineqlem8  42831  lcmineqlem9  42832  lcmineqlem10  42833  lcmineqlem12  42835  3exp7  42848  3lexlogpow5ineq1  42849  3lexlogpow5ineq5  42855  aks4d1p1p4  42866  aks4d1p1p7  42869  aks4d1p1  42871  facp2  42938  25or6to4  43001  1p3e4  43054  sn-1ne2  43060  sqdeccom12  43078  235t711  43094  sin2t3rdpi  43142  cos2t3rdpi  43143  re1m1e0m0  43186  ipiiie0  43227  sn-0tie0  43253  fltnltalem  43422  sum9cubes  43432  3cubeslem3l  43445  3cubeslem3r  43446  eldioph2lem1  43519  lzenom  43529  irrapxlem1  43577  rmspecsqrtnq  43661  rmxm1  43689  rmym1  43690  2nn0ind  43700  jm2.24nn  43714  jm2.17a  43715  jm2.17b  43716  jm2.17c  43717  jm2.24  43718  acongeq  43738  jm2.18  43743  jm2.27c  43762  jm3.1lem2  43773  rngunsnply  43924  flcidc  43925  inductionexd  44909  unitadd  44949  hashnzfzclim  45060  ofdivrec  45064  lhe4.4ex1a  45067  expgrowth  45073  dvradcnv2  45085  binomcxplemrat  45088  binomcxplemnotnn0  45094  isosctrlem1ALT  45670  monoord2xrv  46225  dvsinax  46655  dvnprodlem3  46690  itgsin0pilem1  46692  itgsbtaddcnst  46724  stoweidlem13  46755  stoweidlem26  46768  stoweidlem34  46776  stoweidlem38  46780  wallispilem2  46808  wallispilem4  46810  wallispi2lem1  46813  stirlinglem1  46816  stirlinglem5  46820  stirlinglem10  46825  dirkerper  46838  dirkertrigeqlem1  46840  dirkertrigeqlem3  46842  dirkertrigeq  46843  dirkercncflem4  46848  fourierdlem24  46873  sqwvfoura  46970  sqwvfourb  46971  fourierswlem  46972  cos5t  47644  goldratmolem2  47651  lambert0  47652  lamberte  47653  cjnpoly  47654  1t10e1p1e11  48075  ceil5half3  48111  modm2nep1  48137  modm1nep2  48139  modm1nem2  48140  fmtnorec3  48328  fmtno5lem4  48336  fmtno5  48337  257prm  48341  fmtno4nprmfac193  48354  m3prm  48372  139prmALT  48376  127prm  48379  m7prm  48380  lighneallem3  48387  proththd  48394  3exp4mod41  48396  41prothprmlem2  48398  perfectALTVlem2  48515  perfectALTV  48516  11t31e341  48525  evengpop3  48591  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  bgoldbtbndlem1  48598  0nodd  48963  altgsumbcALT  49161  exple2lt6  49172  nn0sumshdiglemB  49428  ackval3  49491  ackval3012  49500  line2ylem  49559  onetansqsecsq  50567  cotsqcscsq  50568  5m4e1  50645