Axiom ax-1cn 11157

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

This axiom is referenced by:  0cn  11197  1cnd  11201  1ex  11202  mulrid  11205  mullid  11206  1re  11207  0re  11209  muladd11  11379  peano2cn  11381  mul02lem2  11386  addrid  11389  cnegex2  11391  peano2cnm  11523  0reALT  11554  ine0  11648  mulm1  11654  0lt1  11735  ixi  11842  muleqadd  11857  reccl  11878  recne0  11884  recid  11885  recid2  11886  diveq1  11900  div1  11903  1div1e1  11904  recdiv  11920  divdiv1  11925  divdiv2  11926  recdiv2  11927  conjmul  11931  eqneg  11934  div2neg  11937  recp1lt1  12112  recreclt  12113  recgt0ii  12120  neg1cn  12202  neg1ne0  12204  negneg1e1  12206  ofnegsub  12215  peano5nni  12235  nnsscn  12237  nn1m1nn  12253  nn1suc  12254  nnaddcl  12255  nnmulcl  12256  nnne0  12269  nnsub  12279  1m1e0  12312  2cn  12315  3cn  12321  4cn  12325  5cn  12328  6cn  12331  7cn  12334  8cn  12337  9cn  12340  1pneg1e0  12357  1m0e1  12359  0p1e1  12360  1p0e1  12362  2m1e1  12364  2m1e1OLD  12365  3m1e2  12367  4m1e3  12368  5m1e4  12369  6m1e5  12370  7m1e6  12371  8m1e7  12372  9m1e8  12373  2p2e4  12374  1p2e3  12382  1p2e3ALT  12383  3p2e5  12390  3p3e6  12391  4p2e6  12392  4p3e7  12393  4p4e8  12394  5p2e7  12395  5p3e8  12396  5p4e9  12397  6p2e8  12398  6p3e9  12399  7p2e9  12400  1t1e1  12401  3t3e9  12407  neg1mulneg1e1  12455  1mhlfehlf  12462  8th4div3  12463  halfthird  12464  halfpm6th  12465  addltmul  12479  elnn0nn  12545  elz2  12608  zlem1lt  12645  zltlem1  12646  nnaddm1cl  12652  zextlt  12669  zeo  12681  peano5uzi  12684  numsuc  12724  numltc  12741  numsucc  12755  numaddc  12763  6p5lem  12785  5p5e10  12786  6p4e10  12787  7p3e10  12790  8p2e10  12795  10m1e9  12811  4t3lem  12812  7t4e28  12826  9t11e99OLD  12846  decbin2  12858  5recm6rec  12860  uzp1  12898  peano2uzr  12926  uzaddcl  12927  rebtwnz  12970  qbtwnre  13224  iccf1o  13522  fz01en  13579  fztp  13607  fzsuc2  13609  fztpval  13613  fseq1m1p1  13626  elfzp1b  13628  predfz  13680  fzoss2  13715  fzval3  13762  fzosplitsnm1  13768  fzo1to4tp  13782  fldiv4p1lem1div2  13867  ceim1l  13879  fldiv  13892  uzrdgxfr  14002  fzen2  14004  nn0ennn  14014  seqm1  14054  seqshft2  14063  monoord2  14068  sermono  14069  seqf1olem1  14076  seqf1olem2  14077  seqz  14085  ser1const  14093  expcl  14114  expclzlem  14118  m1expcl2  14120  expm1t  14125  1exp  14126  mulexpz  14137  expadd  14139  expaddz  14141  expmul  14142  expubnd  14213  sqrecii  14218  neg1sqe1  14231  irec  14236  i4  14239  binom21  14254  sq01  14260  crreczi  14263  bernneq  14264  bernneq2  14265  nn0opthlem1  14303  facndiv  14323  faclbnd4lem1  14328  faclbnd6  14334  bcnp1n  14349  bcm1k  14350  bcp1nk  14352  bcn2  14354  bcp1m1  14355  bcpasc  14356  hashgadd  14412  hashfz  14463  hashfzo  14465  hashxplem  14469  hashbclem  14488  hashf1  14493  seqcoll  14500  swrds1  14703  swrdlsw  14704  wrdind  14758  wrd2ind  14759  swrds2  14976  relexpaddg  15089  sgnneg  15136  rei  15206  imi  15207  recan  15387  iserex  15707  isercoll2  15719  serf0  15731  iseraltlem2  15733  iseraltlem3  15734  iseralt  15735  sumrblem  15761  fsumm1  15801  telfsumo  15853  fsumparts  15857  hashiun  15873  binomlem  15882  binom  15883  binom1p  15884  binom11  15885  binom1dif  15886  bcxmas  15888  isumsplit  15893  isum1p  15894  climcndslem1  15902  supcvg  15909  harmonic  15912  arisum  15913  arisum2  15914  trireciplem  15915  geoserg  15919  geolim  15923  geolim2  15924  georeclim  15925  geo2sum  15926  geo2sum2  15927  geoisum1c  15933  0.999...  15934  geoihalfsum  15935  cvgrat  15936  mertenslem1  15937  mertenslem2  15938  mertens  15939  prodf1  15944  prodfclim1  15946  prodrblem  15982  fprodcvg  15983  prodmolem2a  15987  zprod  15990  fprodntriv  15995  prodss  16000  fprodss  16001  fprodsplit  16019  fprodn0f  16044  risefaccl  16068  fallfaccl  16069  risefacfac  16088  binomfallfac  16094  bpolycl  16105  bpolysum  16106  bpolydiflem  16107  fsumkthpow  16109  bpoly2  16110  bpoly3  16111  bpoly4  16112  fsumcube  16113  esum  16133  ege2le3  16143  efsub  16155  efexp  16156  efzval  16157  eftlub  16164  effsumlt  16166  ef4p  16168  tanval3  16189  efi4p  16192  tan0  16206  efival  16207  tanadd  16222  cos2t  16233  cos2tsin  16234  ef01bndlem  16239  cos1bnd  16242  cos2bnd  16243  demoivreALT  16256  eirrlem  16259  rpnnen2lem3  16271  rpnnen2lem11  16279  ruclem12  16296  3dvds  16388  3dvdsdec  16389  3dvds2dec  16390  odd2np1lem  16397  odd2np1  16398  opoe  16420  omoe  16421  opeo  16422  omeo  16423  n2dvdsm1  16426  m1exp1  16433  flodddiv4  16472  bitsfzo  16492  sqgcd  16619  expgcd  16620  nn0seqcvgd  16627  prmind2  16742  hashdvds  16833  phiprmpw  16834  phiprm  16835  eulerthlem2  16840  iserodd  16894  sumhash  16955  fldivp1  16956  prmpwdvds  16963  pockthlem  16964  pockthi  16966  prmreclem4  16978  prmreclem6  16980  4sqlem11  17014  4sqlem19  17022  vdwapun  17033  vdwapid1  17034  vdwlem3  17042  vdwlem5  17044  vdwlem6  17045  vdwlem8  17047  vdwlem9  17048  vdwnnlem2  17055  ramub1lem1  17085  ramub1lem2  17086  ramcl  17088  prmo1  17096  dec5nprm  17125  prmlem0  17164  43prm  17181  83prm  17182  139prm  17183  163prm  17184  317prm  17185  631prm  17186  1259lem2  17191  1259lem3  17192  1259lem4  17193  1259lem5  17194  1259prm  17195  2503lem1  17196  2503lem2  17197  2503lem3  17198  2503prm  17199  4001lem1  17200  4001lem2  17201  4001lem3  17202  4001lem4  17203  4001prm  17204  gsumsgrpccat  18898  mulgnndir  19168  mulgneg2  19173  m1expaddsub  19567  sylow1lem1  19667  sylow2a  19688  efgsval2  19802  efgsrel  19803  efgsres  19807  cncrng  21522  cnfld1  21526  zsssubrg  21554  cnmgpid  21558  zringcyg  21598  mulgrhm2  21607  pzriprng1ALT  21625  cnmsgnsubg  21706  cnmsgnbas  21707  cnmsgngrp  21708  psgninv  21711  evpmodpmf1o  21725  psdmplcl  22304  blcvx  24934  iihalf2  25071  icopnfcnv  25080  iccpnfhmeo  25083  xrhmeo  25084  icccvx  25088  lebnumii  25104  reparphti  25135  pcoass  25162  pcorevlem  25164  pcorev2  25166  pi1xfrcnv  25195  cnstrcvs  25279  cncvs  25283  ncvsm1  25292  pjthlem1  25575  divcncf  25585  ovolunlem1a  25634  ovolunlem1  25635  ovolicc2lem4  25658  uniioombllem3  25723  uniioombllem4  25724  dyadovol  25731  vitalilem4  25749  mbf0  25772  iblcnlem1  25926  itgcnlem  25928  dvid  26056  dvexp  26091  dvexp2  26092  dvexp3  26116  dveflem  26117  dvlipcn  26132  dvcvx  26158  dvfsumle  26159  dvfsumlem1  26164  degltp1le  26209  ply1divex  26273  fta1glem1  26304  plyaddlem1  26349  plymullem1  26350  coeidp  26399  dgrid  26400  dvply1  26424  dvply2g  26425  plyremlem  26444  fta1lem  26447  vieta1lem1  26450  vieta1lem2  26451  qaa  26463  iaa  26465  aalioulem3  26474  geolim3  26479  aaliou3lem2  26483  aaliou3lem7  26489  taylply2  26507  dvradcnv  26560  pserdvlem2  26567  pserdv2  26569  abelthlem1  26570  abelthlem2  26571  abelthlem6  26575  abelthlem7  26577  abelth  26580  reeff1olem  26585  reeff1o  26586  efcvx  26588  sinhalfpilem  26604  eulerid  26615  cos2pi  26617  sincosq3sgn  26641  sincosq4sgn  26642  tangtx  26646  sincos4thpi  26654  sincos6thpi  26657  pigt3  26659  pige3ALT  26661  abssinper  26662  coskpi  26664  coseq1  26666  efeq1  26669  tanregt0  26680  logneg2  26756  logdivlti  26761  logcnlem4  26786  dvlog2lem  26793  dvlog2  26794  advlog  26795  advlogexp  26796  logtayl  26801  logtayl2  26803  logccv  26804  cxpval  26805  1cxp  26813  cxpcl  26815  cxpp1  26821  cxpsqrt  26844  dvsqrt  26883  dvcnsqrt  26885  sqrtcn  26891  cxpaddlelem  26892  root1id  26895  root1cj  26897  logrec  26904  logb1  26910  logbmpt  26929  ang180lem1  26950  ang180lem2  26951  ang180lem3  26952  isosctrlem1  26959  isosctrlem2  26960  1cubrlem  26982  1cubr  26983  mcubic  26988  binom4  26991  dquartlem1  26992  quartlem1  26998  asinlem  27009  asinlem2  27010  asinlem3a  27011  asinlem3  27012  asinf  27013  atandm2  27018  atandm4  27020  atanf  27021  asinneg  27027  efiasin  27029  sinasin  27030  asinsin  27033  asin1  27035  acos1  27036  reasinsin  27037  asinbnd  27040  cosasin  27045  atanneg  27048  atancj  27051  efiatan  27053  atanlogaddlem  27054  atanlogadd  27055  atanlogsublem  27056  atanlogsub  27057  efiatan2  27058  2efiatan  27059  tanatan  27060  cosatan  27062  cosatanne0  27063  atantan  27064  atanbndlem  27066  bndatandm  27070  atans2  27072  dvatan  27076  atantayl  27078  atantayl2  27079  atantayl3  27080  leibpilem2  27082  leibpi  27083  log2cnv  27085  log2tlbnd  27086  log2ublem3  27089  log2ub  27090  birthdaylem2  27093  birthday  27095  efrlim  27110  dfef2  27111  cvxcl  27125  scvxcvx  27126  emcllem2  27137  emcllem4  27139  emcllem7  27142  harmonicbnd4  27151  fsumharmonic  27152  zetacvg  27155  lgamcvg2  27195  lgam1  27204  gam1  27205  wilthlem1  27208  wilthlem2  27209  wilthlem3  27210  basellem2  27222  basellem5  27225  basellem6  27226  basellem7  27227  basellem8  27228  basellem9  27229  0sgm  27284  mule1  27288  ppiprm  27291  ppinprm  27292  chtprm  27293  chtnprm  27294  chpp1  27295  mumullem2  27320  1sgmprm  27339  1sgm2ppw  27340  ppiub  27344  chtublem  27351  chtub  27352  logfaclbnd  27362  logfacbnd3  27363  logfacrlim  27364  logexprlim  27365  mersenne  27367  perfect1  27368  perfectlem1  27369  perfectlem2  27370  perfect  27371  dchrelbasd  27379  dchrmullid  27392  dchrfi  27395  dchrsum2  27408  sumdchr2  27410  bcp1ctr  27419  bposlem8  27431  zabsle1  27436  lgslem1  27437  lgslem2  27438  lgsfcl2  27443  lgsvalmod  27456  lgsneg  27461  lgsdilem  27464  lgsdir2lem1  27465  lgsdir2lem2  27466  lgsdir2lem3  27467  lgsdir2lem5  27469  lgsdir2  27470  lgsdir  27472  lgsdi  27474  lgsne0  27475  lgseisenlem1  27515  lgseisenlem2  27516  lgseisen  27519  lgsquadlem1  27520  lgsquadlem2  27521  lgsquad2lem1  27524  lgsquad2  27526  m1lgs  27528  2lgslem3c  27538  2lgsoddprmlem3c  27552  2lgsoddprmlem3d  27553  2sqlem10  27568  2sqlem11  27569  2sqblem  27571  addsqn2reu  27581  addsqrexnreu  27582  addsqnreup  27583  chtppilimlem2  27614  chebbnd2  27617  chto1lb  27618  rplogsumlem1  27624  rpvmasumlem  27627  dchrmusumlema  27633  dchrmusum2  27634  dchrisum0flblem1  27648  rpvmasum2  27652  mudivsum  27670  mulogsum  27672  vmalogdivsum2  27678  selberg2lem  27690  logdivbnd  27696  pntrmax  27704  pntrsumo1  27705  pntrsumbnd2  27707  pntrlog2bndlem5  27721  pntpbnd1a  27725  pntpbnd2  27727  pntibndlem2  27731  pntlemd  27734  pntlemc  27735  pntlemr  27742  brbtwn2  29221  colinearalglem4  29225  ax5seglem1  29244  ax5seglem2  29245  ax5seglem3  29247  ax5seglem5  29249  ax5seglem7  29251  ax5seglem9  29253  axbtwnid  29255  axpaschlem  29256  axlowdimlem13  29270  axlowdimlem14  29271  axlowdimlem16  29273  axeuclidlem  29278  axcontlem2  29281  axcontlem4  29283  axcontlem7  29286  axcontlem8  29287  crctcshwlkn0lem6  30130  clwwlkf1  30366  clwwlknonex2lem2  30425  ex-fl  30764  ex-ind-dvds  30778  vc2OLD  30886  vc0  30892  vcm  30894  nvm1  30983  nvmtri  30989  nvge0  30991  ipval2lem3  31023  ipidsq  31028  lnoadd  31076  ip1ilem  31144  ip1i  31145  ip2i  31146  ipdirilem  31147  ipasslem1  31149  ipasslem2  31150  ipasslem10  31157  minvecolem2  31193  hvsubid  31344  hv2times  31379  hisubcomi  31422  normlem9  31436  normlem7tALT  31437  norm-ii-i  31455  normsubi  31459  hhssnv  31582  pjhthlem1  31709  h1de2bi  31872  homullid  32118  ho2times  32137  lnop0  32284  lnopaddi  32289  lnophmlem2  32335  lnfn0i  32360  lnfnaddi  32361  hst1h  32545  sto2i  32555  stadd3i  32566  addltmulALT  32764  dpmul4  33199  psgnid  33383  cnmsgn0g  33432  altgnsg  33435  isarchi3  33473  archirngz  33475  1fldgenq  33609  ply1dg3rt0irred  33840  esplyfvaln  33930  ccfldextdgrr  34028  constrsscn  34096  constrabscl  34134  cos9thpiminplylem1  34138  cos9thpiminplylem4  34141  cos9thpiminplylem5  34142  lmatfvlem  34171  qqhval2lem  34337  dya2ub  34626  omssubadd  34656  eulerpartlemgs2  34736  fib5  34761  fib6  34762  ballotlem2  34845  signswch  34914  signlem0  34940  itgexpif  34959  reprlt  34972  breprexp  34986  breprexpnat  34987  hgt750lem2  35005  subfacp1lem5  35630  subfacp1lem6  35631  subfacval2  35633  subfaclim  35634  subfacval3  35635  cvxsconn  35689  resconn  35692  cvmliftlem7  35737  cvmliftlem10  35740  problem4  36114  sinccvglem  36118  sqdivzi  36174  faclimlem1  36189  dnibndlem5  37015  dnibndlem10  37020  ltflcei  38203  sin2h  38205  cos2h  38206  tan2h  38207  poimirlem13  38228  poimirlem16  38231  poimirlem17  38232  poimirlem19  38234  poimirlem20  38235  poimirlem31  38246  mblfinlem2  38253  mblfinlem3  38254  dvtan  38265  itg2addnclem3  38268  dvasin  38299  dvacos  38300  areacirc  38308  fdc  38340  mettrifi  38352  heiborlem4  38409  heiborlem6  38411  60gcd7e1  42718  lcmineqlem1  42742  lcmineqlem8  42749  lcmineqlem9  42750  lcmineqlem10  42751  lcmineqlem12  42753  3exp7  42766  3lexlogpow5ineq1  42767  3lexlogpow5ineq5  42773  aks4d1p1p4  42784  aks4d1p1p7  42787  aks4d1p1  42789  facp2  42856  25or6to4  42919  1p3e4  42972  sn-1ne2  42978  sqdeccom12  42996  235t711  43012  sin2t3rdpi  43060  cos2t3rdpi  43061  re1m1e0m0  43104  ipiiie0  43145  sn-0tie0  43171  fltnltalem  43342  sum9cubes  43352  3cubeslem3l  43365  3cubeslem3r  43366  eldioph2lem1  43439  lzenom  43449  irrapxlem1  43497  rmspecsqrtnq  43581  rmxm1  43609  rmym1  43610  2nn0ind  43620  jm2.24nn  43634  jm2.17a  43635  jm2.17b  43636  jm2.17c  43637  jm2.24  43638  acongeq  43658  jm2.18  43663  jm2.27c  43682  jm3.1lem2  43693  rngunsnply  43844  flcidc  43845  inductionexd  44829  unitadd  44869  hashnzfzclim  44980  ofdivrec  44984  lhe4.4ex1a  44987  expgrowth  44993  dvradcnv2  45005  binomcxplemrat  45008  binomcxplemnotnn0  45014  isosctrlem1ALT  45590  monoord2xrv  46145  dvsinax  46575  dvnprodlem3  46610  itgsin0pilem1  46612  itgsbtaddcnst  46644  stoweidlem13  46675  stoweidlem26  46688  stoweidlem34  46696  stoweidlem38  46700  wallispilem2  46728  wallispilem4  46730  wallispi2lem1  46733  stirlinglem1  46736  stirlinglem5  46740  stirlinglem10  46745  dirkerper  46758  dirkertrigeqlem1  46760  dirkertrigeqlem3  46762  dirkertrigeq  46763  dirkercncflem4  46768  fourierdlem24  46793  sqwvfoura  46890  sqwvfourb  46891  fourierswlem  46892  cos5t  47561  goldratmolem2  47568  lambert0  47569  lamberte  47570  cjnpoly  47571  1t10e1p1e11  47992  ceil5half3  48028  modm2nep1  48054  modm1nep2  48056  modm1nem2  48057  fmtnorec3  48245  fmtno5lem4  48253  fmtno5  48254  257prm  48258  fmtno4nprmfac193  48271  m3prm  48289  139prmALT  48293  127prm  48296  m7prm  48297  lighneallem3  48304  proththd  48311  3exp4mod41  48313  41prothprmlem2  48315  perfectALTVlem2  48432  perfectALTV  48433  11t31e341  48442  evengpop3  48508  nnsum4primeseven  48510  nnsum4primesevenALTV  48511  bgoldbtbndlem1  48515  0nodd  48880  altgsumbcALT  49078  exple2lt6  49089  nn0sumshdiglemB  49345  ackval3  49408  ackval3012  49417  line2ylem  49476  onetansqsecsq  50484  cotsqcscsq  50485  5m4e1  50542