Axiom ax-1cn 11085

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

This axiom is referenced by:  0cn  11125  1cnd  11128  1ex  11129  mulrid  11131  mullid  11132  1re  11133  0re  11135  muladd11  11304  peano2cn  11306  mul02lem2  11311  addrid  11314  cnegex2  11316  peano2cnm  11448  0reALT  11479  ine0  11573  mulm1  11579  0lt1  11660  ixi  11767  muleqadd  11782  reccl  11804  recne0  11810  recid  11811  recid2  11812  diveq1  11827  div1  11832  1div1e1  11833  recdiv  11848  divdiv1  11853  divdiv2  11854  recdiv2  11855  conjmul  11859  eqneg  11862  div2neg  11865  recp1lt1  12041  recreclt  12042  recgt0ii  12049  neg1cn  12131  neg1ne0  12133  negneg1e1  12135  ofnegsub  12144  peano5nni  12149  nnsscn  12151  nn1m1nn  12167  nn1suc  12168  nnaddcl  12169  nnmulcl  12170  nnne0  12180  nnsub  12190  1m1e0  12218  2cn  12221  3cn  12227  4cn  12231  5cn  12234  6cn  12237  7cn  12240  8cn  12243  9cn  12246  1pneg1e0  12260  1m0e1  12262  0p1e1  12263  1p0e1  12265  2m1e1  12267  3m1e2  12269  4m1e3  12270  5m1e4  12271  6m1e5  12272  7m1e6  12273  8m1e7  12274  9m1e8  12275  2p2e4  12276  1p2e3  12284  1p2e3ALT  12285  3p2e5  12292  3p3e6  12293  4p2e6  12294  4p3e7  12295  4p4e8  12296  5p2e7  12297  5p3e8  12298  5p4e9  12299  6p2e8  12300  6p3e9  12301  7p2e9  12302  1t1e1  12303  3t3e9  12308  neg1mulneg1e1  12354  1mhlfehlf  12361  8th4div3  12362  halfthird  12363  halfpm6th  12364  addltmul  12378  elnn0nn  12444  elz2  12507  zlem1lt  12544  zltlem1  12545  nnaddm1cl  12550  zextlt  12567  zeo  12579  peano5uzi  12582  numsuc  12622  numltc  12634  numsucc  12648  numaddc  12656  6p5lem  12678  5p5e10  12679  6p4e10  12680  7p3e10  12683  8p2e10  12688  10m1e9  12704  4t3lem  12705  7t4e28  12719  9t11e99  12738  decbin2  12749  5recm6rec  12751  uzp1  12789  peano2uzr  12817  uzaddcl  12818  rebtwnz  12861  qbtwnre  13115  iccf1o  13413  fz01en  13469  fztp  13497  fzsuc2  13499  fztpval  13503  fseq1m1p1  13516  elfzp1b  13518  predfz  13570  fzoss2  13604  fzval3  13651  fzosplitsnm1  13657  fzo1to4tp  13671  fldiv4p1lem1div2  13756  ceim1l  13768  fldiv  13781  uzrdgxfr  13891  fzen2  13893  nn0ennn  13903  seqm1  13943  seqshft2  13952  monoord2  13957  sermono  13958  seqf1olem1  13965  seqf1olem2  13966  seqz  13974  ser1const  13982  expcl  14003  expclzlem  14007  m1expcl2  14009  expm1t  14014  1exp  14015  mulexpz  14026  expadd  14028  expaddz  14030  expmul  14031  expubnd  14102  sqrecii  14107  neg1sqe1  14120  irec  14125  i4  14128  binom21  14143  sq01  14149  crreczi  14152  bernneq  14153  bernneq2  14154  nn0opthlem1  14192  facndiv  14212  faclbnd4lem1  14217  faclbnd6  14223  bcnp1n  14238  bcm1k  14239  bcp1nk  14241  bcn2  14243  bcp1m1  14244  bcpasc  14245  hashgadd  14301  hashfz  14351  hashfzo  14353  hashxplem  14357  hashbclem  14376  hashf1  14381  seqcoll  14388  swrds1  14591  swrdlsw  14592  wrdind  14646  wrd2ind  14647  swrds2  14864  relexpaddg  14977  rei  15080  imi  15081  recan  15261  iserex  15581  isercoll2  15593  serf0  15605  iseraltlem2  15607  iseraltlem3  15608  iseralt  15609  sumrblem  15635  fsumm1  15675  telfsumo  15726  fsumparts  15730  hashiun  15746  binomlem  15753  binom  15754  binom1p  15755  binom11  15756  binom1dif  15757  bcxmas  15759  isumsplit  15764  isum1p  15765  climcndslem1  15773  supcvg  15780  harmonic  15783  arisum  15784  arisum2  15785  trireciplem  15786  geoserg  15790  geolim  15794  geolim2  15795  georeclim  15796  geo2sum  15797  geo2sum2  15798  geoisum1c  15804  0.999...  15805  geoihalfsum  15806  cvgrat  15807  mertenslem1  15808  mertenslem2  15809  mertens  15810  prodf1  15815  prodfclim1  15817  prodrblem  15853  fprodcvg  15854  prodmolem2a  15858  zprod  15861  fprodntriv  15866  prodss  15871  fprodss  15872  fprodsplit  15890  fprodn0f  15915  risefaccl  15939  fallfaccl  15940  risefacfac  15959  binomfallfac  15965  bpolycl  15976  bpolysum  15977  bpolydiflem  15978  fsumkthpow  15980  bpoly2  15981  bpoly3  15982  bpoly4  15983  fsumcube  15984  esum  16004  ege2le3  16014  efsub  16026  efexp  16027  efzval  16028  eftlub  16035  effsumlt  16037  ef4p  16039  tanval3  16060  efi4p  16063  tan0  16077  efival  16078  tanadd  16093  cos2t  16104  cos2tsin  16105  ef01bndlem  16110  cos1bnd  16113  cos2bnd  16114  demoivreALT  16127  eirrlem  16130  rpnnen2lem3  16142  rpnnen2lem11  16150  ruclem12  16167  3dvds  16259  3dvdsdec  16260  3dvds2dec  16261  odd2np1lem  16268  odd2np1  16269  opoe  16291  omoe  16292  opeo  16293  omeo  16294  n2dvdsm1  16297  m1exp1  16304  flodddiv4  16343  bitsfzo  16363  sqgcd  16490  expgcd  16491  nn0seqcvgd  16498  prmind2  16613  hashdvds  16703  phiprmpw  16704  phiprm  16705  eulerthlem2  16710  iserodd  16764  sumhash  16825  fldivp1  16826  prmpwdvds  16833  pockthlem  16834  pockthi  16836  prmreclem4  16848  prmreclem6  16850  4sqlem11  16884  4sqlem19  16892  vdwapun  16903  vdwapid1  16904  vdwlem3  16912  vdwlem5  16914  vdwlem6  16915  vdwlem8  16917  vdwlem9  16918  vdwnnlem2  16925  ramub1lem1  16955  ramub1lem2  16956  ramcl  16958  prmo1  16966  dec5nprm  16995  prmlem0  17034  43prm  17050  83prm  17051  139prm  17052  163prm  17053  317prm  17054  631prm  17055  1259lem2  17060  1259lem3  17061  1259lem4  17062  1259lem5  17063  1259prm  17064  2503lem1  17065  2503lem2  17066  2503lem3  17067  2503prm  17068  4001lem1  17069  4001lem2  17070  4001lem3  17071  4001lem4  17072  4001prm  17073  gsumsgrpccat  18766  mulgnndir  19037  mulgneg2  19042  m1expaddsub  19431  sylow1lem1  19531  sylow2a  19552  efgsval2  19666  efgsrel  19667  efgsres  19671  cncrng  21345  cnfld1  21350  cnfld1OLD  21351  zsssubrg  21382  cnmgpid  21386  zringcyg  21426  mulgrhm2  21435  pzriprng1ALT  21453  cnmsgnsubg  21534  cnmsgnbas  21535  cnmsgngrp  21536  psgninv  21539  evpmodpmf1o  21553  psdmplcl  22106  blcvx  24741  iihalf2  24878  icopnfcnv  24887  iccpnfhmeo  24890  xrhmeo  24891  icccvx  24895  lebnumii  24911  reparphti  24942  pcoass  24969  pcorevlem  24971  pcorev2  24973  pi1xfrcnv  25002  cnstrcvs  25086  cncvs  25090  ncvsm1  25099  pjthlem1  25382  divcncf  25392  ovolunlem1a  25441  ovolunlem1  25442  ovolicc2lem4  25465  uniioombllem3  25530  uniioombllem4  25531  dyadovol  25538  vitalilem4  25556  mbf0  25579  iblcnlem1  25733  itgcnlem  25735  dvid  25863  dvexp  25898  dvexp2  25899  dvexp3  25923  dveflem  25924  dvlipcn  25940  dvcvx  25966  dvfsumle  25967  dvfsumleOLD  25968  dvfsumlem1  25973  degltp1le  26019  ply1divex  26083  fta1glem1  26114  plyaddlem1  26159  plymullem1  26160  coeidp  26209  dgrid  26210  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  26412  eulerid  26423  cos2pi  26425  sincosq3sgn  26449  sincosq4sgn  26450  tangtx  26454  sincos4thpi  26462  sincos6thpi  26465  pigt3  26467  pige3ALT  26469  abssinper  26470  coskpi  26472  coseq1  26474  efeq1  26477  tanregt0  26488  logneg2  26564  logdivlti  26569  logcnlem4  26594  dvlog2lem  26601  dvlog2  26602  advlog  26603  advlogexp  26604  logtayl  26609  logtayl2  26611  logccv  26612  cxpval  26613  1cxp  26621  cxpcl  26623  cxpp1  26629  cxpsqrt  26652  dvsqrt  26691  dvcnsqrt  26693  sqrtcn  26700  cxpaddlelem  26701  root1id  26704  root1cj  26706  logrec  26713  logb1  26719  logbmpt  26738  ang180lem1  26759  ang180lem2  26760  ang180lem3  26761  isosctrlem1  26768  isosctrlem2  26769  1cubrlem  26791  1cubr  26792  mcubic  26797  binom4  26800  dquartlem1  26801  quartlem1  26807  asinlem  26818  asinlem2  26819  asinlem3a  26820  asinlem3  26821  asinf  26822  atandm2  26827  atandm4  26829  atanf  26830  asinneg  26836  efiasin  26838  sinasin  26839  asinsin  26842  asin1  26844  acos1  26845  reasinsin  26846  asinbnd  26849  cosasin  26854  atanneg  26857  atancj  26860  efiatan  26862  atanlogaddlem  26863  atanlogadd  26864  atanlogsublem  26865  atanlogsub  26866  efiatan2  26867  2efiatan  26868  tanatan  26869  cosatan  26871  cosatanne0  26872  atantan  26873  atanbndlem  26875  bndatandm  26879  atans2  26881  dvatan  26885  atantayl  26887  atantayl2  26888  atantayl3  26889  leibpilem2  26891  leibpi  26892  log2cnv  26894  log2tlbnd  26895  log2ublem3  26898  log2ub  26899  birthdaylem2  26902  birthday  26904  efrlim  26919  efrlimOLD  26920  dfef2  26921  cvxcl  26935  scvxcvx  26936  emcllem2  26947  emcllem4  26949  emcllem7  26952  harmonicbnd4  26961  fsumharmonic  26962  zetacvg  26965  lgamcvg2  27005  lgam1  27014  gam1  27015  wilthlem1  27018  wilthlem2  27019  wilthlem3  27020  basellem2  27032  basellem5  27035  basellem6  27036  basellem7  27037  basellem8  27038  basellem9  27039  0sgm  27094  mule1  27098  ppiprm  27101  ppinprm  27102  chtprm  27103  chtnprm  27104  chpp1  27105  mumullem2  27130  1sgmprm  27150  1sgm2ppw  27151  ppiub  27155  chtublem  27162  chtub  27163  logfaclbnd  27173  logfacbnd3  27174  logfacrlim  27175  logexprlim  27176  mersenne  27178  perfect1  27179  perfectlem1  27180  perfectlem2  27181  perfect  27182  dchrelbasd  27190  dchrmullid  27203  dchrfi  27206  dchrsum2  27219  sumdchr2  27221  bcp1ctr  27230  bposlem8  27242  zabsle1  27247  lgslem1  27248  lgslem2  27249  lgsfcl2  27254  lgsvalmod  27267  lgsneg  27272  lgsdilem  27275  lgsdir2lem1  27276  lgsdir2lem2  27277  lgsdir2lem3  27278  lgsdir2lem5  27280  lgsdir2  27281  lgsdir  27283  lgsdi  27285  lgsne0  27286  lgseisenlem1  27326  lgseisenlem2  27327  lgseisen  27330  lgsquadlem1  27331  lgsquadlem2  27332  lgsquad2lem1  27335  lgsquad2  27337  m1lgs  27339  2lgslem3c  27349  2lgsoddprmlem3c  27363  2lgsoddprmlem3d  27364  2sqlem10  27379  2sqlem11  27380  2sqblem  27382  addsqn2reu  27392  addsqrexnreu  27393  addsqnreup  27394  chtppilimlem2  27425  chebbnd2  27428  chto1lb  27429  rplogsumlem1  27435  rpvmasumlem  27438  dchrmusumlema  27444  dchrmusum2  27445  dchrisum0flblem1  27459  rpvmasum2  27463  mudivsum  27481  mulogsum  27483  vmalogdivsum2  27489  selberg2lem  27501  logdivbnd  27507  pntrmax  27515  pntrsumo1  27516  pntrsumbnd2  27518  pntrlog2bndlem5  27532  pntpbnd1a  27536  pntpbnd2  27538  pntibndlem2  27542  pntlemd  27545  pntlemc  27546  pntlemr  27553  brbtwn2  28962  colinearalglem4  28966  ax5seglem1  28985  ax5seglem2  28986  ax5seglem3  28988  ax5seglem5  28990  ax5seglem7  28992  ax5seglem9  28994  axbtwnid  28996  axpaschlem  28997  axlowdimlem13  29011  axlowdimlem14  29012  axlowdimlem16  29014  axeuclidlem  29019  axcontlem2  29022  axcontlem4  29024  axcontlem7  29027  axcontlem8  29028  crctcshwlkn0lem6  29872  clwwlkf1  30108  clwwlknonex2lem2  30167  ex-fl  30506  ex-ind-dvds  30520  vc2OLD  30628  vc0  30634  vcm  30636  nvm1  30725  nvmtri  30731  nvge0  30733  ipval2lem3  30765  ipidsq  30770  lnoadd  30818  ip1ilem  30886  ip1i  30887  ip2i  30888  ipdirilem  30889  ipasslem1  30891  ipasslem2  30892  ipasslem10  30899  minvecolem2  30935  hvsubid  31086  hv2times  31121  hisubcomi  31164  normlem9  31178  normlem7tALT  31179  norm-ii-i  31197  normsubi  31201  hhssnv  31324  pjhthlem1  31451  h1de2bi  31614  homullid  31860  ho2times  31879  lnop0  32026  lnopaddi  32031  lnophmlem2  32077  lnfn0i  32102  lnfnaddi  32103  hst1h  32287  sto2i  32297  stadd3i  32308  addltmulALT  32506  sgnneg  32897  dpmul4  32978  psgnid  33163  cnmsgn0g  33212  altgnsg  33215  isarchi3  33253  archirngz  33255  1fldgenq  33388  ply1dg3rt0irred  33649  esplyfvaln  33723  ccfldextdgrr  33822  constrsscn  33890  constrabscl  33928  cos9thpiminplylem1  33932  cos9thpiminplylem4  33935  cos9thpiminplylem5  33936  lmatfvlem  33965  qqhval2lem  34131  dya2ub  34420  omssubadd  34450  eulerpartlemgs2  34530  fib5  34555  fib6  34556  ballotlem2  34639  signswch  34711  signlem0  34737  itgexpif  34756  reprlt  34769  breprexp  34783  breprexpnat  34784  hgt750lem2  34802  subfacp1lem5  35372  subfacp1lem6  35373  subfacval2  35375  subfaclim  35376  subfacval3  35377  cvxsconn  35431  resconn  35434  cvmliftlem7  35479  cvmliftlem10  35482  problem4  35856  sinccvglem  35860  sqdivzi  35916  faclimlem1  35931  dnibndlem5  36740  dnibndlem10  36745  ltflcei  37920  sin2h  37922  cos2h  37923  tan2h  37924  poimirlem13  37945  poimirlem16  37948  poimirlem17  37949  poimirlem19  37951  poimirlem20  37952  poimirlem31  37963  mblfinlem2  37970  mblfinlem3  37971  dvtan  37982  itg2addnclem3  37985  dvasin  38016  dvacos  38017  areacirc  38025  fdc  38057  mettrifi  38069  heiborlem4  38126  heiborlem6  38128  60gcd7e1  42436  lcmineqlem1  42460  lcmineqlem8  42467  lcmineqlem9  42468  lcmineqlem10  42469  lcmineqlem12  42471  3exp7  42484  3lexlogpow5ineq1  42485  3lexlogpow5ineq5  42491  aks4d1p1p4  42502  aks4d1p1p7  42505  aks4d1p1  42507  facp2  42574  1p3e4  42690  sn-1ne2  42696  sqdeccom12  42720  235t711  42736  sin2t3rdpi  42784  cos2t3rdpi  42785  re1m1e0m0  42828  ipiiie0  42869  sn-0tie0  42895  fltnltalem  43094  sum9cubes  43104  3cubeslem3l  43117  3cubeslem3r  43118  eldioph2lem1  43191  lzenom  43201  irrapxlem1  43253  rmspecsqrtnq  43337  rmxm1  43365  rmym1  43366  2nn0ind  43376  jm2.24nn  43390  jm2.17a  43391  jm2.17b  43392  jm2.17c  43393  jm2.24  43394  acongeq  43414  jm2.18  43419  jm2.27c  43438  jm3.1lem2  43449  rngunsnply  43600  flcidc  43601  inductionexd  44585  unitadd  44625  hashnzfzclim  44752  ofdivrec  44756  lhe4.4ex1a  44759  expgrowth  44765  dvradcnv2  44777  binomcxplemrat  44780  binomcxplemnotnn0  44786  isosctrlem1ALT  45363  monoord2xrv  45915  dvsinax  46345  dvnprodlem3  46380  itgsin0pilem1  46382  itgsbtaddcnst  46414  stoweidlem13  46445  stoweidlem26  46458  stoweidlem34  46466  stoweidlem38  46470  wallispilem2  46498  wallispilem4  46500  wallispi2lem1  46503  stirlinglem1  46506  stirlinglem5  46510  stirlinglem10  46515  dirkerper  46528  dirkertrigeqlem1  46530  dirkertrigeqlem3  46532  dirkertrigeq  46533  dirkercncflem4  46538  fourierdlem24  46563  sqwvfoura  46660  sqwvfourb  46661  fourierswlem  46662  lambert0  47321  lamberte  47322  cjnpoly  47323  1t10e1p1e11  47744  ceil5half3  47774  modm2nep1  47800  modm1nep2  47802  modm1nem2  47803  fmtnorec3  47982  fmtno5lem4  47990  fmtno5  47991  257prm  47995  fmtno4nprmfac193  48008  m3prm  48026  139prmALT  48030  127prm  48033  m7prm  48034  lighneallem3  48041  proththd  48048  3exp4mod41  48050  41prothprmlem2  48052  perfectALTVlem2  48156  perfectALTV  48157  11t31e341  48166  evengpop3  48232  nnsum4primeseven  48234  nnsum4primesevenALTV  48235  bgoldbtbndlem1  48239  0nodd  48604  altgsumbcALT  48787  exple2lt6  48798  nn0sumshdiglemB  49054  ackval3  49117  ackval3012  49126  line2ylem  49185  onetansqsecsq  50194  cotsqcscsq  50195  5m4e1  50230