Axiom ax-1cn 11071

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

This axiom is referenced by:  0cn  11111  1cnd  11114  1ex  11115  mulrid  11117  mullid  11118  1re  11119  0re  11121  muladd11  11290  peano2cn  11292  mul02lem2  11297  addrid  11300  cnegex2  11302  peano2cnm  11434  0reALT  11465  ine0  11559  mulm1  11565  0lt1  11646  ixi  11753  muleqadd  11768  reccl  11790  recne0  11796  recid  11797  recid2  11798  diveq1  11813  div1  11818  1div1e1  11819  recdiv  11834  divdiv1  11839  divdiv2  11840  recdiv2  11841  conjmul  11845  eqneg  11848  div2neg  11851  recp1lt1  12027  recreclt  12028  recgt0ii  12035  neg1cn  12117  neg1ne0  12119  negneg1e1  12121  ofnegsub  12130  peano5nni  12135  nnsscn  12137  nn1m1nn  12153  nn1suc  12154  nnaddcl  12155  nnmulcl  12156  nnne0  12166  nnsub  12176  1m1e0  12204  2cn  12207  3cn  12213  4cn  12217  5cn  12220  6cn  12223  7cn  12226  8cn  12229  9cn  12232  1pneg1e0  12246  1m0e1  12248  0p1e1  12249  1p0e1  12251  2m1e1  12253  3m1e2  12255  4m1e3  12256  5m1e4  12257  6m1e5  12258  7m1e6  12259  8m1e7  12260  9m1e8  12261  2p2e4  12262  1p2e3  12270  1p2e3ALT  12271  3p2e5  12278  3p3e6  12279  4p2e6  12280  4p3e7  12281  4p4e8  12282  5p2e7  12283  5p3e8  12284  5p4e9  12285  6p2e8  12286  6p3e9  12287  7p2e9  12288  1t1e1  12289  3t3e9  12294  neg1mulneg1e1  12340  1mhlfehlf  12347  8th4div3  12348  halfthird  12349  halfpm6th  12350  addltmul  12364  elnn0nn  12430  elz2  12493  zlem1lt  12530  zltlem1  12531  nnaddm1cl  12536  zextlt  12553  zeo  12565  peano5uzi  12568  numsuc  12608  numltc  12620  numsucc  12634  numaddc  12642  6p5lem  12664  5p5e10  12665  6p4e10  12666  7p3e10  12669  8p2e10  12674  10m1e9  12690  4t3lem  12691  7t4e28  12705  9t11e99  12724  decbin2  12735  5recm6rec  12737  uzp1  12775  peano2uzr  12803  uzaddcl  12804  rebtwnz  12847  qbtwnre  13100  iccf1o  13398  fz01en  13454  fztp  13482  fzsuc2  13484  fztpval  13488  fseq1m1p1  13501  elfzp1b  13503  predfz  13555  fzoss2  13589  fzval3  13636  fzosplitsnm1  13642  fzo1to4tp  13656  fldiv4p1lem1div2  13741  ceim1l  13753  fldiv  13766  uzrdgxfr  13876  fzen2  13878  nn0ennn  13888  seqm1  13928  seqshft2  13937  monoord2  13942  sermono  13943  seqf1olem1  13950  seqf1olem2  13951  seqz  13959  ser1const  13967  expcl  13988  expclzlem  13992  m1expcl2  13994  expm1t  13999  1exp  14000  mulexpz  14011  expadd  14013  expaddz  14015  expmul  14016  expubnd  14087  sqrecii  14092  neg1sqe1  14105  irec  14110  i4  14113  binom21  14128  sq01  14134  crreczi  14137  bernneq  14138  bernneq2  14139  nn0opthlem1  14177  facndiv  14197  faclbnd4lem1  14202  faclbnd6  14208  bcnp1n  14223  bcm1k  14224  bcp1nk  14226  bcn2  14228  bcp1m1  14229  bcpasc  14230  hashgadd  14286  hashfz  14336  hashfzo  14338  hashxplem  14342  hashbclem  14361  hashf1  14366  seqcoll  14373  swrds1  14576  swrdlsw  14577  wrdind  14631  wrd2ind  14632  swrds2  14849  relexpaddg  14962  rei  15065  imi  15066  recan  15246  iserex  15566  isercoll2  15578  serf0  15590  iseraltlem2  15592  iseraltlem3  15593  iseralt  15594  sumrblem  15620  fsumm1  15660  telfsumo  15711  fsumparts  15715  hashiun  15731  binomlem  15738  binom  15739  binom1p  15740  binom11  15741  binom1dif  15742  bcxmas  15744  isumsplit  15749  isum1p  15750  climcndslem1  15758  supcvg  15765  harmonic  15768  arisum  15769  arisum2  15770  trireciplem  15771  geoserg  15775  geolim  15779  geolim2  15780  georeclim  15781  geo2sum  15782  geo2sum2  15783  geoisum1c  15789  0.999...  15790  geoihalfsum  15791  cvgrat  15792  mertenslem1  15793  mertenslem2  15794  mertens  15795  prodf1  15800  prodfclim1  15802  prodrblem  15838  fprodcvg  15839  prodmolem2a  15843  zprod  15846  fprodntriv  15851  prodss  15856  fprodss  15857  fprodsplit  15875  fprodn0f  15900  risefaccl  15924  fallfaccl  15925  risefacfac  15944  binomfallfac  15950  bpolycl  15961  bpolysum  15962  bpolydiflem  15963  fsumkthpow  15965  bpoly2  15966  bpoly3  15967  bpoly4  15968  fsumcube  15969  esum  15989  ege2le3  15999  efsub  16011  efexp  16012  efzval  16013  eftlub  16020  effsumlt  16022  ef4p  16024  tanval3  16045  efi4p  16048  tan0  16062  efival  16063  tanadd  16078  cos2t  16089  cos2tsin  16090  ef01bndlem  16095  cos1bnd  16098  cos2bnd  16099  demoivreALT  16112  eirrlem  16115  rpnnen2lem3  16127  rpnnen2lem11  16135  ruclem12  16152  3dvds  16244  3dvdsdec  16245  3dvds2dec  16246  odd2np1lem  16253  odd2np1  16254  opoe  16276  omoe  16277  opeo  16278  omeo  16279  n2dvdsm1  16282  m1exp1  16289  flodddiv4  16328  bitsfzo  16348  sqgcd  16475  expgcd  16476  nn0seqcvgd  16483  prmind2  16598  hashdvds  16688  phiprmpw  16689  phiprm  16690  eulerthlem2  16695  iserodd  16749  sumhash  16810  fldivp1  16811  prmpwdvds  16818  pockthlem  16819  pockthi  16821  prmreclem4  16833  prmreclem6  16835  4sqlem11  16869  4sqlem19  16877  vdwapun  16888  vdwapid1  16889  vdwlem3  16897  vdwlem5  16899  vdwlem6  16900  vdwlem8  16902  vdwlem9  16903  vdwnnlem2  16910  ramub1lem1  16940  ramub1lem2  16941  ramcl  16943  prmo1  16951  dec5nprm  16980  prmlem0  17019  43prm  17035  83prm  17036  139prm  17037  163prm  17038  317prm  17039  631prm  17040  1259lem2  17045  1259lem3  17046  1259lem4  17047  1259lem5  17048  1259prm  17049  2503lem1  17050  2503lem2  17051  2503lem3  17052  2503prm  17053  4001lem1  17054  4001lem2  17055  4001lem3  17056  4001lem4  17057  4001prm  17058  gsumsgrpccat  18750  mulgnndir  19018  mulgneg2  19023  m1expaddsub  19412  sylow1lem1  19512  sylow2a  19533  efgsval2  19647  efgsrel  19648  efgsres  19652  cncrng  21327  cnfld1  21332  cnfld1OLD  21333  zsssubrg  21364  cnmgpid  21368  zringcyg  21408  mulgrhm2  21417  pzriprng1ALT  21435  cnmsgnsubg  21516  cnmsgnbas  21517  cnmsgngrp  21518  psgninv  21521  evpmodpmf1o  21535  psdmplcl  22078  blcvx  24714  iihalf2  24856  icopnfcnv  24868  iccpnfhmeo  24871  xrhmeo  24872  icccvx  24876  lebnumii  24893  reparphti  24924  reparphtiOLD  24925  pcoass  24952  pcorevlem  24954  pcorev2  24956  pi1xfrcnv  24985  cnstrcvs  25069  cncvs  25073  ncvsm1  25082  pjthlem1  25365  divcncf  25376  ovolunlem1a  25425  ovolunlem1  25426  ovolicc2lem4  25449  uniioombllem3  25514  uniioombllem4  25515  dyadovol  25522  vitalilem4  25540  mbf0  25563  iblcnlem1  25717  itgcnlem  25719  dvid  25847  dvexp  25885  dvexp2  25886  dvexp3  25910  dveflem  25911  dvlipcn  25927  dvcvx  25953  dvfsumle  25954  dvfsumleOLD  25955  dvfsumlem1  25960  degltp1le  26006  ply1divex  26070  fta1glem1  26101  plyaddlem1  26146  plymullem1  26147  coeidp  26197  dgrid  26198  dvply1  26219  dvply2g  26220  dvply2gOLD  26221  plyremlem  26240  fta1lem  26243  vieta1lem1  26246  vieta1lem2  26247  qaa  26259  iaa  26261  aalioulem3  26270  geolim3  26275  aaliou3lem2  26279  aaliou3lem7  26285  taylply2  26303  taylply2OLD  26304  dvradcnv  26358  pserdvlem2  26366  pserdv2  26368  abelthlem1  26369  abelthlem2  26370  abelthlem6  26374  abelthlem7  26376  abelth  26379  reeff1olem  26384  reeff1o  26385  efcvx  26387  sinhalfpilem  26400  eulerid  26411  cos2pi  26413  sincosq3sgn  26437  sincosq4sgn  26438  tangtx  26442  sincos4thpi  26450  sincos6thpi  26453  pigt3  26455  pige3ALT  26457  abssinper  26458  coskpi  26460  coseq1  26462  efeq1  26465  tanregt0  26476  logneg2  26552  logdivlti  26557  logcnlem4  26582  dvlog2lem  26589  dvlog2  26590  advlog  26591  advlogexp  26592  logtayl  26597  logtayl2  26599  logccv  26600  cxpval  26601  1cxp  26609  cxpcl  26611  cxpp1  26617  cxpsqrt  26640  dvsqrt  26679  dvcnsqrt  26681  sqrtcn  26688  cxpaddlelem  26689  root1id  26692  root1cj  26694  logrec  26701  logb1  26707  logbmpt  26726  ang180lem1  26747  ang180lem2  26748  ang180lem3  26749  isosctrlem1  26756  isosctrlem2  26757  1cubrlem  26779  1cubr  26780  mcubic  26785  binom4  26788  dquartlem1  26789  quartlem1  26795  asinlem  26806  asinlem2  26807  asinlem3a  26808  asinlem3  26809  asinf  26810  atandm2  26815  atandm4  26817  atanf  26818  asinneg  26824  efiasin  26826  sinasin  26827  asinsin  26830  asin1  26832  acos1  26833  reasinsin  26834  asinbnd  26837  cosasin  26842  atanneg  26845  atancj  26848  efiatan  26850  atanlogaddlem  26851  atanlogadd  26852  atanlogsublem  26853  atanlogsub  26854  efiatan2  26855  2efiatan  26856  tanatan  26857  cosatan  26859  cosatanne0  26860  atantan  26861  atanbndlem  26863  bndatandm  26867  atans2  26869  dvatan  26873  atantayl  26875  atantayl2  26876  atantayl3  26877  leibpilem2  26879  leibpi  26880  log2cnv  26882  log2tlbnd  26883  log2ublem3  26886  log2ub  26887  birthdaylem2  26890  birthday  26892  efrlim  26907  efrlimOLD  26908  dfef2  26909  cvxcl  26923  scvxcvx  26924  emcllem2  26935  emcllem4  26937  emcllem7  26940  harmonicbnd4  26949  fsumharmonic  26950  zetacvg  26953  lgamcvg2  26993  lgam1  27002  gam1  27003  wilthlem1  27006  wilthlem2  27007  wilthlem3  27008  basellem2  27020  basellem5  27023  basellem6  27024  basellem7  27025  basellem8  27026  basellem9  27027  0sgm  27082  mule1  27086  ppiprm  27089  ppinprm  27090  chtprm  27091  chtnprm  27092  chpp1  27093  mumullem2  27118  1sgmprm  27138  1sgm2ppw  27139  ppiub  27143  chtublem  27150  chtub  27151  logfaclbnd  27161  logfacbnd3  27162  logfacrlim  27163  logexprlim  27164  mersenne  27166  perfect1  27167  perfectlem1  27168  perfectlem2  27169  perfect  27170  dchrelbasd  27178  dchrmullid  27191  dchrfi  27194  dchrsum2  27207  sumdchr2  27209  bcp1ctr  27218  bposlem8  27230  zabsle1  27235  lgslem1  27236  lgslem2  27237  lgsfcl2  27242  lgsvalmod  27255  lgsneg  27260  lgsdilem  27263  lgsdir2lem1  27264  lgsdir2lem2  27265  lgsdir2lem3  27266  lgsdir2lem5  27268  lgsdir2  27269  lgsdir  27271  lgsdi  27273  lgsne0  27274  lgseisenlem1  27314  lgseisenlem2  27315  lgseisen  27318  lgsquadlem1  27319  lgsquadlem2  27320  lgsquad2lem1  27323  lgsquad2  27325  m1lgs  27327  2lgslem3c  27337  2lgsoddprmlem3c  27351  2lgsoddprmlem3d  27352  2sqlem10  27367  2sqlem11  27368  2sqblem  27370  addsqn2reu  27380  addsqrexnreu  27381  addsqnreup  27382  chtppilimlem2  27413  chebbnd2  27416  chto1lb  27417  rplogsumlem1  27423  rpvmasumlem  27426  dchrmusumlema  27432  dchrmusum2  27433  dchrisum0flblem1  27447  rpvmasum2  27451  mudivsum  27469  mulogsum  27471  vmalogdivsum2  27477  selberg2lem  27489  logdivbnd  27495  pntrmax  27503  pntrsumo1  27504  pntrsumbnd2  27506  pntrlog2bndlem5  27520  pntpbnd1a  27524  pntpbnd2  27526  pntibndlem2  27530  pntlemd  27533  pntlemc  27534  pntlemr  27541  brbtwn2  28885  colinearalglem4  28889  ax5seglem1  28908  ax5seglem2  28909  ax5seglem3  28911  ax5seglem5  28913  ax5seglem7  28915  ax5seglem9  28917  axbtwnid  28919  axpaschlem  28920  axlowdimlem13  28934  axlowdimlem14  28935  axlowdimlem16  28937  axeuclidlem  28942  axcontlem2  28945  axcontlem4  28947  axcontlem7  28950  axcontlem8  28951  crctcshwlkn0lem6  29795  clwwlkf1  30031  clwwlknonex2lem2  30090  ex-fl  30429  ex-ind-dvds  30443  vc2OLD  30550  vc0  30556  vcm  30558  nvm1  30647  nvmtri  30653  nvge0  30655  ipval2lem3  30687  ipidsq  30692  lnoadd  30740  ip1ilem  30808  ip1i  30809  ip2i  30810  ipdirilem  30811  ipasslem1  30813  ipasslem2  30814  ipasslem10  30821  minvecolem2  30857  hvsubid  31008  hv2times  31043  hisubcomi  31086  normlem9  31100  normlem7tALT  31101  norm-ii-i  31119  normsubi  31123  hhssnv  31246  pjhthlem1  31373  h1de2bi  31536  homullid  31782  ho2times  31801  lnop0  31948  lnopaddi  31953  lnophmlem2  31999  lnfn0i  32024  lnfnaddi  32025  hst1h  32209  sto2i  32219  stadd3i  32230  addltmulALT  32428  sgnneg  32821  dpmul4  32901  psgnid  33073  cnmsgn0g  33122  altgnsg  33125  isarchi3  33163  archirngz  33165  1fldgenq  33295  ply1dg3rt0irred  33553  ccfldextdgrr  33706  constrsscn  33774  constrabscl  33812  cos9thpiminplylem1  33816  cos9thpiminplylem4  33819  cos9thpiminplylem5  33820  lmatfvlem  33849  qqhval2lem  34015  dya2ub  34304  omssubadd  34334  eulerpartlemgs2  34414  fib5  34439  fib6  34440  ballotlem2  34523  signswch  34595  signlem0  34621  itgexpif  34640  reprlt  34653  breprexp  34667  breprexpnat  34668  hgt750lem2  34686  subfacp1lem5  35249  subfacp1lem6  35250  subfacval2  35252  subfaclim  35253  subfacval3  35254  cvxsconn  35308  resconn  35311  cvmliftlem7  35356  cvmliftlem10  35359  problem4  35733  sinccvglem  35737  sqdivzi  35793  faclimlem1  35808  dnibndlem5  36547  dnibndlem10  36552  ltflcei  37668  sin2h  37670  cos2h  37671  tan2h  37672  poimirlem13  37693  poimirlem16  37696  poimirlem17  37697  poimirlem19  37699  poimirlem20  37700  poimirlem31  37711  mblfinlem2  37718  mblfinlem3  37719  dvtan  37730  itg2addnclem3  37733  dvasin  37764  dvacos  37765  areacirc  37773  fdc  37805  mettrifi  37817  heiborlem4  37874  heiborlem6  37876  60gcd7e1  42118  lcmineqlem1  42142  lcmineqlem8  42149  lcmineqlem9  42150  lcmineqlem10  42151  lcmineqlem12  42153  3exp7  42166  3lexlogpow5ineq1  42167  3lexlogpow5ineq5  42173  aks4d1p1p4  42184  aks4d1p1p7  42187  aks4d1p1  42189  facp2  42256  1p3e4  42377  sn-1ne2  42383  sqdeccom12  42407  235t711  42423  sin2t3rdpi  42471  cos2t3rdpi  42472  re1m1e0m0  42515  ipiiie0  42556  sn-0tie0  42569  fltnltalem  42780  sum9cubes  42790  3cubeslem3l  42803  3cubeslem3r  42804  eldioph2lem1  42877  lzenom  42887  irrapxlem1  42939  rmspecsqrtnq  43023  rmxm1  43051  rmym1  43052  2nn0ind  43062  jm2.24nn  43076  jm2.17a  43077  jm2.17b  43078  jm2.17c  43079  jm2.24  43080  acongeq  43100  jm2.18  43105  jm2.27c  43124  jm3.1lem2  43135  rngunsnply  43286  flcidc  43287  inductionexd  44272  unitadd  44312  hashnzfzclim  44439  ofdivrec  44443  lhe4.4ex1a  44446  expgrowth  44452  dvradcnv2  44464  binomcxplemrat  44467  binomcxplemnotnn0  44473  isosctrlem1ALT  45050  monoord2xrv  45605  dvsinax  46035  dvnprodlem3  46070  itgsin0pilem1  46072  itgsbtaddcnst  46104  stoweidlem13  46135  stoweidlem26  46148  stoweidlem34  46156  stoweidlem38  46160  wallispilem2  46188  wallispilem4  46190  wallispi2lem1  46193  stirlinglem1  46196  stirlinglem5  46200  stirlinglem10  46205  dirkerper  46218  dirkertrigeqlem1  46220  dirkertrigeqlem3  46222  dirkertrigeq  46223  dirkercncflem4  46228  fourierdlem24  46253  sqwvfoura  46350  sqwvfourb  46351  fourierswlem  46352  lambert0  47011  lamberte  47012  cjnpoly  47013  1t10e1p1e11  47434  ceil5half3  47464  modm2nep1  47490  modm1nep2  47492  modm1nem2  47493  fmtnorec3  47672  fmtno5lem4  47680  fmtno5  47681  257prm  47685  fmtno4nprmfac193  47698  m3prm  47716  139prmALT  47720  127prm  47723  m7prm  47724  lighneallem3  47731  proththd  47738  3exp4mod41  47740  41prothprmlem2  47742  perfectALTVlem2  47846  perfectALTV  47847  11t31e341  47856  evengpop3  47922  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  bgoldbtbndlem1  47929  0nodd  48294  altgsumbcALT  48477  exple2lt6  48488  nn0sumshdiglemB  48745  ackval3  48808  ackval3012  48817  line2ylem  48876  onetansqsecsq  49886  cotsqcscsq  49887  5m4e1  49922