Axiom ax-1cn 11126

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

This axiom is referenced by:  0cn  11166  1cnd  11169  1ex  11170  mulrid  11172  mullid  11173  1re  11174  0re  11176  muladd11  11344  peano2cn  11346  mul02lem2  11351  addrid  11354  cnegex2  11356  peano2cnm  11488  0reALT  11519  ine0  11613  mulm1  11619  0lt1  11700  ixi  11807  muleqadd  11822  reccl  11844  recne0  11850  recid  11851  recid2  11852  diveq1  11867  div1  11872  1div1e1  11873  recdiv  11888  divdiv1  11893  divdiv2  11894  recdiv2  11895  conjmul  11899  eqneg  11902  div2neg  11905  recp1lt1  12081  recreclt  12082  recgt0ii  12089  neg1cn  12171  neg1ne0  12173  negneg1e1  12175  ofnegsub  12184  peano5nni  12189  nnsscn  12191  nn1m1nn  12207  nn1suc  12208  nnaddcl  12209  nnmulcl  12210  nnne0  12220  nnsub  12230  1m1e0  12258  2cn  12261  3cn  12267  4cn  12271  5cn  12274  6cn  12277  7cn  12280  8cn  12283  9cn  12286  1pneg1e0  12300  1m0e1  12302  0p1e1  12303  1p0e1  12305  2m1e1  12307  3m1e2  12309  4m1e3  12310  5m1e4  12311  6m1e5  12312  7m1e6  12313  8m1e7  12314  9m1e8  12315  2p2e4  12316  1p2e3  12324  1p2e3ALT  12325  3p2e5  12332  3p3e6  12333  4p2e6  12334  4p3e7  12335  4p4e8  12336  5p2e7  12337  5p3e8  12338  5p4e9  12339  6p2e8  12340  6p3e9  12341  7p2e9  12342  1t1e1  12343  3t3e9  12348  neg1mulneg1e1  12394  1mhlfehlf  12401  8th4div3  12402  halfthird  12403  halfpm6th  12404  addltmul  12418  elnn0nn  12484  elz2  12547  zlem1lt  12585  zltlem1  12586  nnaddm1cl  12591  zextlt  12608  zeo  12620  peano5uzi  12623  numsuc  12663  numltc  12675  numsucc  12689  numaddc  12697  6p5lem  12719  5p5e10  12720  6p4e10  12721  7p3e10  12724  8p2e10  12729  10m1e9  12745  4t3lem  12746  7t4e28  12760  9t11e99  12779  decbin2  12790  5recm6rec  12792  uzp1  12834  peano2uzr  12862  uzaddcl  12863  rebtwnz  12906  qbtwnre  13159  iccf1o  13457  fz01en  13513  fztp  13541  fzsuc2  13543  fztpval  13547  fseq1m1p1  13560  elfzp1b  13562  predfz  13614  fzoss2  13648  fzval3  13695  fzosplitsnm1  13701  fzo1to4tp  13715  fldiv4p1lem1div2  13797  ceim1l  13809  fldiv  13822  uzrdgxfr  13932  fzen2  13934  nn0ennn  13944  seqm1  13984  seqshft2  13993  monoord2  13998  sermono  13999  seqf1olem1  14006  seqf1olem2  14007  seqz  14015  ser1const  14023  expcl  14044  expclzlem  14048  m1expcl2  14050  expm1t  14055  1exp  14056  mulexpz  14067  expadd  14069  expaddz  14071  expmul  14072  expubnd  14143  sqrecii  14148  neg1sqe1  14161  irec  14166  i4  14169  binom21  14184  sq01  14190  crreczi  14193  bernneq  14194  bernneq2  14195  nn0opthlem1  14233  facndiv  14253  faclbnd4lem1  14258  faclbnd6  14264  bcnp1n  14279  bcm1k  14280  bcp1nk  14282  bcn2  14284  bcp1m1  14285  bcpasc  14286  hashgadd  14342  hashfz  14392  hashfzo  14394  hashxplem  14398  hashbclem  14417  hashf1  14422  seqcoll  14429  swrds1  14631  swrdlsw  14632  wrdind  14687  wrd2ind  14688  swrds2  14906  relexpaddg  15019  rei  15122  imi  15123  recan  15303  iserex  15623  isercoll2  15635  serf0  15647  iseraltlem2  15649  iseraltlem3  15650  iseralt  15651  sumrblem  15677  fsumm1  15717  telfsumo  15768  fsumparts  15772  hashiun  15788  binomlem  15795  binom  15796  binom1p  15797  binom11  15798  binom1dif  15799  bcxmas  15801  isumsplit  15806  isum1p  15807  climcndslem1  15815  supcvg  15822  harmonic  15825  arisum  15826  arisum2  15827  trireciplem  15828  geoserg  15832  geolim  15836  geolim2  15837  georeclim  15838  geo2sum  15839  geo2sum2  15840  geoisum1c  15846  0.999...  15847  geoihalfsum  15848  cvgrat  15849  mertenslem1  15850  mertenslem2  15851  mertens  15852  prodf1  15857  prodfclim1  15859  prodrblem  15895  fprodcvg  15896  prodmolem2a  15900  zprod  15903  fprodntriv  15908  prodss  15913  fprodss  15914  fprodsplit  15932  fprodn0f  15957  risefaccl  15981  fallfaccl  15982  risefacfac  16001  binomfallfac  16007  bpolycl  16018  bpolysum  16019  bpolydiflem  16020  fsumkthpow  16022  bpoly2  16023  bpoly3  16024  bpoly4  16025  fsumcube  16026  esum  16046  ege2le3  16056  efsub  16068  efexp  16069  efzval  16070  eftlub  16077  effsumlt  16079  ef4p  16081  tanval3  16102  efi4p  16105  tan0  16119  efival  16120  tanadd  16135  cos2t  16146  cos2tsin  16147  ef01bndlem  16152  cos1bnd  16155  cos2bnd  16156  demoivreALT  16169  eirrlem  16172  rpnnen2lem3  16184  rpnnen2lem11  16192  ruclem12  16209  3dvds  16301  3dvdsdec  16302  3dvds2dec  16303  odd2np1lem  16310  odd2np1  16311  opoe  16333  omoe  16334  opeo  16335  omeo  16336  n2dvdsm1  16339  m1exp1  16346  flodddiv4  16385  bitsfzo  16405  sqgcd  16532  expgcd  16533  nn0seqcvgd  16540  prmind2  16655  hashdvds  16745  phiprmpw  16746  phiprm  16747  eulerthlem2  16752  iserodd  16806  sumhash  16867  fldivp1  16868  prmpwdvds  16875  pockthlem  16876  pockthi  16878  prmreclem4  16890  prmreclem6  16892  4sqlem11  16926  4sqlem19  16934  vdwapun  16945  vdwapid1  16946  vdwlem3  16954  vdwlem5  16956  vdwlem6  16957  vdwlem8  16959  vdwlem9  16960  vdwnnlem2  16967  ramub1lem1  16997  ramub1lem2  16998  ramcl  17000  prmo1  17008  dec5nprm  17037  prmlem0  17076  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  gsumsgrpccat  18767  mulgnndir  19035  mulgneg2  19040  m1expaddsub  19428  sylow1lem1  19528  sylow2a  19549  efgsval2  19663  efgsrel  19664  efgsres  19668  cncrng  21300  cnfld1  21305  cnfld1OLD  21306  zsssubrg  21342  cnmgpid  21346  zringcyg  21379  mulgrhm2  21388  pzriprng1ALT  21406  cnmsgnsubg  21486  cnmsgnbas  21487  cnmsgngrp  21488  psgninv  21491  evpmodpmf1o  21505  psdmplcl  22049  blcvx  24686  iihalf2  24828  icopnfcnv  24840  iccpnfhmeo  24843  xrhmeo  24844  icccvx  24848  lebnumii  24865  reparphti  24896  reparphtiOLD  24897  pcoass  24924  pcorevlem  24926  pcorev2  24928  pi1xfrcnv  24957  cnstrcvs  25041  cncvs  25045  ncvsm1  25054  pjthlem1  25337  divcncf  25348  ovolunlem1a  25397  ovolunlem1  25398  ovolicc2lem4  25421  uniioombllem3  25486  uniioombllem4  25487  dyadovol  25494  vitalilem4  25512  mbf0  25535  iblcnlem1  25689  itgcnlem  25691  dvid  25819  dvexp  25857  dvexp2  25858  dvexp3  25882  dveflem  25883  dvlipcn  25899  dvcvx  25925  dvfsumle  25926  dvfsumleOLD  25927  dvfsumlem1  25932  degltp1le  25978  ply1divex  26042  fta1glem1  26073  plyaddlem1  26118  plymullem1  26119  coeidp  26169  dgrid  26170  dvply1  26191  dvply2g  26192  dvply2gOLD  26193  plyremlem  26212  fta1lem  26215  vieta1lem1  26218  vieta1lem2  26219  qaa  26231  iaa  26233  aalioulem3  26242  geolim3  26247  aaliou3lem2  26251  aaliou3lem7  26257  taylply2  26275  taylply2OLD  26276  dvradcnv  26330  pserdvlem2  26338  pserdv2  26340  abelthlem1  26341  abelthlem2  26342  abelthlem6  26346  abelthlem7  26348  abelth  26351  reeff1olem  26356  reeff1o  26357  efcvx  26359  sinhalfpilem  26372  eulerid  26383  cos2pi  26385  sincosq3sgn  26409  sincosq4sgn  26410  tangtx  26414  sincos4thpi  26422  sincos6thpi  26425  pigt3  26427  pige3ALT  26429  abssinper  26430  coskpi  26432  coseq1  26434  efeq1  26437  tanregt0  26448  logneg2  26524  logdivlti  26529  logcnlem4  26554  dvlog2lem  26561  dvlog2  26562  advlog  26563  advlogexp  26564  logtayl  26569  logtayl2  26571  logccv  26572  cxpval  26573  1cxp  26581  cxpcl  26583  cxpp1  26589  cxpsqrt  26612  dvsqrt  26651  dvcnsqrt  26653  sqrtcn  26660  cxpaddlelem  26661  root1id  26664  root1cj  26666  logrec  26673  logb1  26679  logbmpt  26698  ang180lem1  26719  ang180lem2  26720  ang180lem3  26721  isosctrlem1  26728  isosctrlem2  26729  1cubrlem  26751  1cubr  26752  mcubic  26757  binom4  26760  dquartlem1  26761  quartlem1  26767  asinlem  26778  asinlem2  26779  asinlem3a  26780  asinlem3  26781  asinf  26782  atandm2  26787  atandm4  26789  atanf  26790  asinneg  26796  efiasin  26798  sinasin  26799  asinsin  26802  asin1  26804  acos1  26805  reasinsin  26806  asinbnd  26809  cosasin  26814  atanneg  26817  atancj  26820  efiatan  26822  atanlogaddlem  26823  atanlogadd  26824  atanlogsublem  26825  atanlogsub  26826  efiatan2  26827  2efiatan  26828  tanatan  26829  cosatan  26831  cosatanne0  26832  atantan  26833  atanbndlem  26835  bndatandm  26839  atans2  26841  dvatan  26845  atantayl  26847  atantayl2  26848  atantayl3  26849  leibpilem2  26851  leibpi  26852  log2cnv  26854  log2tlbnd  26855  log2ublem3  26858  log2ub  26859  birthdaylem2  26862  birthday  26864  efrlim  26879  efrlimOLD  26880  dfef2  26881  cvxcl  26895  scvxcvx  26896  emcllem2  26907  emcllem4  26909  emcllem7  26912  harmonicbnd4  26921  fsumharmonic  26922  zetacvg  26925  lgamcvg2  26965  lgam1  26974  gam1  26975  wilthlem1  26978  wilthlem2  26979  wilthlem3  26980  basellem2  26992  basellem5  26995  basellem6  26996  basellem7  26997  basellem8  26998  basellem9  26999  0sgm  27054  mule1  27058  ppiprm  27061  ppinprm  27062  chtprm  27063  chtnprm  27064  chpp1  27065  mumullem2  27090  1sgmprm  27110  1sgm2ppw  27111  ppiub  27115  chtublem  27122  chtub  27123  logfaclbnd  27133  logfacbnd3  27134  logfacrlim  27135  logexprlim  27136  mersenne  27138  perfect1  27139  perfectlem1  27140  perfectlem2  27141  perfect  27142  dchrelbasd  27150  dchrmullid  27163  dchrfi  27166  dchrsum2  27179  sumdchr2  27181  bcp1ctr  27190  bposlem8  27202  zabsle1  27207  lgslem1  27208  lgslem2  27209  lgsfcl2  27214  lgsvalmod  27227  lgsneg  27232  lgsdilem  27235  lgsdir2lem1  27236  lgsdir2lem2  27237  lgsdir2lem3  27238  lgsdir2lem5  27240  lgsdir2  27241  lgsdir  27243  lgsdi  27245  lgsne0  27246  lgseisenlem1  27286  lgseisenlem2  27287  lgseisen  27290  lgsquadlem1  27291  lgsquadlem2  27292  lgsquad2lem1  27295  lgsquad2  27297  m1lgs  27299  2lgslem3c  27309  2lgsoddprmlem3c  27323  2lgsoddprmlem3d  27324  2sqlem10  27339  2sqlem11  27340  2sqblem  27342  addsqn2reu  27352  addsqrexnreu  27353  addsqnreup  27354  chtppilimlem2  27385  chebbnd2  27388  chto1lb  27389  rplogsumlem1  27395  rpvmasumlem  27398  dchrmusumlema  27404  dchrmusum2  27405  dchrisum0flblem1  27419  rpvmasum2  27423  mudivsum  27441  mulogsum  27443  vmalogdivsum2  27449  selberg2lem  27461  logdivbnd  27467  pntrmax  27475  pntrsumo1  27476  pntrsumbnd2  27478  pntrlog2bndlem5  27492  pntpbnd1a  27496  pntpbnd2  27498  pntibndlem2  27502  pntlemd  27505  pntlemc  27506  pntlemr  27513  brbtwn2  28832  colinearalglem4  28836  ax5seglem1  28855  ax5seglem2  28856  ax5seglem3  28858  ax5seglem5  28860  ax5seglem7  28862  ax5seglem9  28864  axbtwnid  28866  axpaschlem  28867  axlowdimlem13  28881  axlowdimlem14  28882  axlowdimlem16  28884  axeuclidlem  28889  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  axcontlem8  28898  crctcshwlkn0lem6  29745  clwwlkf1  29978  clwwlknonex2lem2  30037  ex-fl  30376  ex-ind-dvds  30390  vc2OLD  30497  vc0  30503  vcm  30505  nvm1  30594  nvmtri  30600  nvge0  30602  ipval2lem3  30634  ipidsq  30639  lnoadd  30687  ip1ilem  30755  ip1i  30756  ip2i  30757  ipdirilem  30758  ipasslem1  30760  ipasslem2  30761  ipasslem10  30768  minvecolem2  30804  hvsubid  30955  hv2times  30990  hisubcomi  31033  normlem9  31047  normlem7tALT  31048  norm-ii-i  31066  normsubi  31070  hhssnv  31193  pjhthlem1  31320  h1de2bi  31483  homullid  31729  ho2times  31748  lnop0  31895  lnopaddi  31900  lnophmlem2  31946  lnfn0i  31971  lnfnaddi  31972  hst1h  32156  sto2i  32166  stadd3i  32177  addltmulALT  32375  sgnneg  32758  dpmul4  32834  psgnid  33054  cnmsgn0g  33103  altgnsg  33106  isarchi3  33141  archirngz  33143  1fldgenq  33272  ply1dg3rt0irred  33551  ccfldextdgrr  33667  constrsscn  33730  constrabscl  33768  cos9thpiminplylem1  33772  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  lmatfvlem  33805  qqhval2lem  33971  dya2ub  34261  omssubadd  34291  eulerpartlemgs2  34371  fib5  34396  fib6  34397  ballotlem2  34480  signswch  34552  signlem0  34578  itgexpif  34597  reprlt  34610  breprexp  34624  breprexpnat  34625  hgt750lem2  34643  subfacp1lem5  35171  subfacp1lem6  35172  subfacval2  35174  subfaclim  35175  subfacval3  35176  cvxsconn  35230  resconn  35233  cvmliftlem7  35278  cvmliftlem10  35281  problem4  35655  sinccvglem  35659  sqdivzi  35715  faclimlem1  35730  dnibndlem5  36470  dnibndlem10  36475  ltflcei  37602  sin2h  37604  cos2h  37605  tan2h  37606  poimirlem13  37627  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem31  37645  mblfinlem2  37652  mblfinlem3  37653  dvtan  37664  itg2addnclem3  37667  dvasin  37698  dvacos  37699  areacirc  37707  fdc  37739  mettrifi  37751  heiborlem4  37808  heiborlem6  37810  60gcd7e1  41993  lcmineqlem1  42017  lcmineqlem8  42024  lcmineqlem9  42025  lcmineqlem10  42026  lcmineqlem12  42028  3exp7  42041  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  aks4d1p1p4  42059  aks4d1p1p7  42062  aks4d1p1  42064  facp2  42131  1p3e4  42247  sn-1ne2  42253  sqdeccom12  42277  235t711  42293  sin2t3rdpi  42341  cos2t3rdpi  42342  re1m1e0m0  42385  ipiiie0  42426  sn-0tie0  42439  fltnltalem  42650  sum9cubes  42660  3cubeslem3l  42674  3cubeslem3r  42675  eldioph2lem1  42748  lzenom  42758  irrapxlem1  42810  rmspecsqrtnq  42894  rmxm1  42923  rmym1  42924  2nn0ind  42934  jm2.24nn  42948  jm2.17a  42949  jm2.17b  42950  jm2.17c  42951  jm2.24  42952  acongeq  42972  jm2.18  42977  jm2.27c  42996  jm3.1lem2  43007  rngunsnply  43158  flcidc  43159  inductionexd  44144  unitadd  44184  hashnzfzclim  44311  ofdivrec  44315  lhe4.4ex1a  44318  expgrowth  44324  dvradcnv2  44336  binomcxplemrat  44339  binomcxplemnotnn0  44345  isosctrlem1ALT  44923  monoord2xrv  45479  dvsinax  45911  dvnprodlem3  45946  itgsin0pilem1  45948  itgsbtaddcnst  45980  stoweidlem13  46011  stoweidlem26  46024  stoweidlem34  46032  stoweidlem38  46036  wallispilem2  46064  wallispilem4  46066  wallispi2lem1  46069  stirlinglem1  46072  stirlinglem5  46076  stirlinglem10  46081  dirkerper  46094  dirkertrigeqlem1  46096  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncflem4  46104  fourierdlem24  46129  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  lambert0  46888  lamberte  46889  cjnpoly  46890  1t10e1p1e11  47311  ceil5half3  47341  modm2nep1  47367  modm1nep2  47369  modm1nem2  47370  fmtnorec3  47549  fmtno5lem4  47557  fmtno5  47558  257prm  47562  fmtno4nprmfac193  47575  m3prm  47593  139prmALT  47597  127prm  47600  m7prm  47601  lighneallem3  47608  proththd  47615  3exp4mod41  47617  41prothprmlem2  47619  perfectALTVlem2  47723  perfectALTV  47724  11t31e341  47733  evengpop3  47799  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  bgoldbtbndlem1  47806  0nodd  48158  altgsumbcALT  48341  exple2lt6  48352  nn0sumshdiglemB  48609  ackval3  48672  ackval3012  48681  line2ylem  48740  onetansqsecsq  49750  cotsqcscsq  49751  5m4e1  49786