Axiom ax-1cn 11185

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

This axiom is referenced by:  0cn  11225  1cnd  11228  1ex  11229  mulrid  11231  mullid  11232  1re  11233  0re  11235  muladd11  11403  peano2cn  11405  mul02lem2  11410  addrid  11413  cnegex2  11415  peano2cnm  11547  0reALT  11578  ine0  11670  mulm1  11676  0lt1  11757  ixi  11864  muleqadd  11879  reccl  11901  recne0  11907  recid  11908  recid2  11909  diveq1  11924  div1  11929  1div1e1  11930  recdiv  11945  divdiv1  11950  divdiv2  11951  recdiv2  11952  conjmul  11956  eqneg  11959  div2neg  11962  recp1lt1  12138  recreclt  12139  recgt0ii  12146  inelr  12228  ofnegsub  12236  peano5nni  12241  nnsscn  12243  nn1m1nn  12259  nn1suc  12260  nnaddcl  12261  nnmulcl  12262  nnne0  12272  nnsub  12282  1m1e0  12310  2cn  12313  3cn  12319  4cn  12323  5cn  12326  6cn  12329  7cn  12332  8cn  12335  9cn  12338  neg1cn  12352  neg1ne0  12354  negneg1e1  12356  1pneg1e0  12357  1m0e1  12359  0p1e1  12360  1p0e1  12362  2m1e1  12364  3m1e2  12366  4m1e3  12367  5m1e4  12368  6m1e5  12369  7m1e6  12370  8m1e7  12371  9m1e8  12372  2p2e4  12373  1p2e3  12381  1p2e3ALT  12382  3p2e5  12389  3p3e6  12390  4p2e6  12391  4p3e7  12392  4p4e8  12393  5p2e7  12394  5p3e8  12395  5p4e9  12396  6p2e8  12397  6p3e9  12398  7p2e9  12399  1t1e1  12400  3t3e9  12405  neg1mulneg1e1  12451  1mhlfehlf  12458  8th4div3  12459  halfthird  12460  halfpm6th  12461  addltmul  12475  elnn0nn  12541  elz2  12604  zlem1lt  12642  zltlem1  12643  nnaddm1cl  12648  zextlt  12665  zeo  12677  peano5uzi  12680  numsuc  12720  numltc  12732  numsucc  12746  numaddc  12754  6p5lem  12776  5p5e10  12777  6p4e10  12778  7p3e10  12781  8p2e10  12786  10m1e9  12802  4t3lem  12803  7t4e28  12817  9t11e99  12836  decbin2  12847  5recm6rec  12849  uzp1  12891  peano2uzr  12917  uzaddcl  12918  rebtwnz  12961  qbtwnre  13213  iccf1o  13511  fz01en  13567  fztp  13595  fzsuc2  13597  fztpval  13601  fseq1m1p1  13614  elfzp1b  13616  predfz  13668  fzoss2  13702  fzval3  13748  fzosplitsnm1  13754  fzo1to4tp  13768  fldiv4p1lem1div2  13850  ceim1l  13862  fldiv  13875  uzrdgxfr  13983  fzen2  13985  nn0ennn  13995  seqm1  14035  seqshft2  14044  monoord2  14049  sermono  14050  seqf1olem1  14057  seqf1olem2  14058  seqz  14066  ser1const  14074  expcl  14095  expclzlem  14099  m1expcl2  14101  expm1t  14106  1exp  14107  mulexpz  14118  expadd  14120  expaddz  14122  expmul  14123  expubnd  14194  sqrecii  14199  neg1sqe1  14212  irec  14217  i4  14220  binom21  14235  sq01  14241  crreczi  14244  bernneq  14245  bernneq2  14246  nn0opthlem1  14284  facndiv  14304  faclbnd4lem1  14309  faclbnd6  14315  bcnp1n  14330  bcm1k  14331  bcp1nk  14333  bcn2  14335  bcp1m1  14336  bcpasc  14337  hashgadd  14393  hashfz  14443  hashfzo  14445  hashxplem  14449  hashbclem  14468  hashf1  14473  seqcoll  14480  swrds1  14682  swrdlsw  14683  wrdind  14738  wrd2ind  14739  swrds2  14957  relexpaddg  15070  rei  15173  imi  15174  recan  15353  iserex  15671  isercoll2  15683  serf0  15695  iseraltlem2  15697  iseraltlem3  15698  iseralt  15699  sumrblem  15725  fsumm1  15765  telfsumo  15816  fsumparts  15820  hashiun  15836  binomlem  15843  binom  15844  binom1p  15845  binom11  15846  binom1dif  15847  bcxmas  15849  isumsplit  15854  isum1p  15855  climcndslem1  15863  supcvg  15870  harmonic  15873  arisum  15874  arisum2  15875  trireciplem  15876  geoserg  15880  geolim  15884  geolim2  15885  georeclim  15886  geo2sum  15887  geo2sum2  15888  geoisum1c  15894  0.999...  15895  geoihalfsum  15896  cvgrat  15897  mertenslem1  15898  mertenslem2  15899  mertens  15900  prodf1  15905  prodfclim1  15907  prodrblem  15943  fprodcvg  15944  prodmolem2a  15948  zprod  15951  fprodntriv  15956  prodss  15961  fprodss  15962  fprodsplit  15980  fprodn0f  16005  risefaccl  16029  fallfaccl  16030  risefacfac  16049  binomfallfac  16055  bpolycl  16066  bpolysum  16067  bpolydiflem  16068  fsumkthpow  16070  bpoly2  16071  bpoly3  16072  bpoly4  16073  fsumcube  16074  esum  16094  ege2le3  16104  efsub  16116  efexp  16117  efzval  16118  eftlub  16125  effsumlt  16127  ef4p  16129  tanval3  16150  efi4p  16153  tan0  16167  efival  16168  tanadd  16183  cos2t  16194  cos2tsin  16195  ef01bndlem  16200  cos1bnd  16203  cos2bnd  16204  demoivreALT  16217  eirrlem  16220  rpnnen2lem3  16232  rpnnen2lem11  16240  ruclem12  16257  3dvds  16348  3dvdsdec  16349  3dvds2dec  16350  odd2np1lem  16357  odd2np1  16358  opoe  16380  omoe  16381  opeo  16382  omeo  16383  n2dvdsm1  16386  m1exp1  16393  flodddiv4  16432  bitsfzo  16452  sqgcd  16579  expgcd  16580  nn0seqcvgd  16587  prmind2  16702  hashdvds  16792  phiprmpw  16793  phiprm  16794  eulerthlem2  16799  iserodd  16853  sumhash  16914  fldivp1  16915  prmpwdvds  16922  pockthlem  16923  pockthi  16925  prmreclem4  16937  prmreclem6  16939  4sqlem11  16973  4sqlem19  16981  vdwapun  16992  vdwapid1  16993  vdwlem3  17001  vdwlem5  17003  vdwlem6  17004  vdwlem8  17006  vdwlem9  17007  vdwnnlem2  17014  ramub1lem1  17044  ramub1lem2  17045  ramcl  17047  prmo1  17055  dec5nprm  17084  prmlem0  17123  43prm  17139  83prm  17140  139prm  17141  163prm  17142  317prm  17143  631prm  17144  1259lem2  17149  1259lem3  17150  1259lem4  17151  1259lem5  17152  1259prm  17153  2503lem1  17154  2503lem2  17155  2503lem3  17156  2503prm  17157  4001lem1  17158  4001lem2  17159  4001lem3  17160  4001lem4  17161  4001prm  17162  gsumsgrpccat  18816  mulgnndir  19084  mulgneg2  19089  m1expaddsub  19477  sylow1lem1  19577  sylow2a  19598  efgsval2  19712  efgsrel  19713  efgsres  19717  cncrng  21349  cnfld1  21354  cnfld1OLD  21355  zsssubrg  21391  cnmgpid  21395  zringcyg  21428  mulgrhm2  21437  pzriprng1ALT  21455  cnmsgnsubg  21535  cnmsgnbas  21536  cnmsgngrp  21537  psgninv  21540  evpmodpmf1o  21554  psdmplcl  22098  blcvx  24735  iihalf2  24877  icopnfcnv  24889  iccpnfhmeo  24892  xrhmeo  24893  icccvx  24897  lebnumii  24914  reparphti  24945  reparphtiOLD  24946  pcoass  24973  pcorevlem  24975  pcorev2  24977  pi1xfrcnv  25006  cnstrcvs  25090  cncvs  25094  ncvsm1  25104  pjthlem1  25387  divcncf  25398  ovolunlem1a  25447  ovolunlem1  25448  ovolicc2lem4  25471  uniioombllem3  25536  uniioombllem4  25537  dyadovol  25544  vitalilem4  25562  mbf0  25585  iblcnlem1  25739  itgcnlem  25741  dvid  25869  dvexp  25907  dvexp2  25908  dvexp3  25932  dveflem  25933  dvlipcn  25949  dvcvx  25975  dvfsumle  25976  dvfsumleOLD  25977  dvfsumlem1  25982  degltp1le  26028  ply1divex  26092  fta1glem1  26123  plyaddlem1  26168  plymullem1  26169  coeidp  26219  dgrid  26220  dvply1  26241  dvply2g  26242  dvply2gOLD  26243  plyremlem  26262  fta1lem  26265  vieta1lem1  26268  vieta1lem2  26269  qaa  26281  iaa  26283  aalioulem3  26292  geolim3  26297  aaliou3lem2  26301  aaliou3lem7  26307  taylply2  26325  taylply2OLD  26326  dvradcnv  26380  pserdvlem2  26388  pserdv2  26390  abelthlem1  26391  abelthlem2  26392  abelthlem6  26396  abelthlem7  26398  abelth  26401  reeff1olem  26406  reeff1o  26407  efcvx  26409  sinhalfpilem  26422  eulerid  26433  cos2pi  26435  sincosq3sgn  26459  sincosq4sgn  26460  tangtx  26464  sincos4thpi  26472  sincos6thpi  26475  pigt3  26477  pige3ALT  26479  abssinper  26480  coskpi  26482  coseq1  26484  efeq1  26487  tanregt0  26498  logneg2  26574  logdivlti  26579  logcnlem4  26604  dvlog2lem  26611  dvlog2  26612  advlog  26613  advlogexp  26614  logtayl  26619  logtayl2  26621  logccv  26622  cxpval  26623  1cxp  26631  cxpcl  26633  cxpp1  26639  cxpsqrt  26662  dvsqrt  26701  dvcnsqrt  26703  sqrtcn  26710  cxpaddlelem  26711  root1id  26714  root1cj  26716  logrec  26723  logb1  26729  logbmpt  26748  ang180lem1  26769  ang180lem2  26770  ang180lem3  26771  isosctrlem1  26778  isosctrlem2  26779  1cubrlem  26801  1cubr  26802  mcubic  26807  binom4  26810  dquartlem1  26811  quartlem1  26817  asinlem  26828  asinlem2  26829  asinlem3a  26830  asinlem3  26831  asinf  26832  atandm2  26837  atandm4  26839  atanf  26840  asinneg  26846  efiasin  26848  sinasin  26849  asinsin  26852  asin1  26854  acos1  26855  reasinsin  26856  asinbnd  26859  cosasin  26864  atanneg  26867  atancj  26870  efiatan  26872  atanlogaddlem  26873  atanlogadd  26874  atanlogsublem  26875  atanlogsub  26876  efiatan2  26877  2efiatan  26878  tanatan  26879  cosatan  26881  cosatanne0  26882  atantan  26883  atanbndlem  26885  bndatandm  26889  atans2  26891  dvatan  26895  atantayl  26897  atantayl2  26898  atantayl3  26899  leibpilem2  26901  leibpi  26902  log2cnv  26904  log2tlbnd  26905  log2ublem3  26908  log2ub  26909  birthdaylem2  26912  birthday  26914  efrlim  26929  efrlimOLD  26930  dfef2  26931  cvxcl  26945  scvxcvx  26946  emcllem2  26957  emcllem4  26959  emcllem7  26962  harmonicbnd4  26971  fsumharmonic  26972  zetacvg  26975  lgamcvg2  27015  lgam1  27024  gam1  27025  wilthlem1  27028  wilthlem2  27029  wilthlem3  27030  basellem2  27042  basellem5  27045  basellem6  27046  basellem7  27047  basellem8  27048  basellem9  27049  0sgm  27104  mule1  27108  ppiprm  27111  ppinprm  27112  chtprm  27113  chtnprm  27114  chpp1  27115  mumullem2  27140  1sgmprm  27160  1sgm2ppw  27161  ppiub  27165  chtublem  27172  chtub  27173  logfaclbnd  27183  logfacbnd3  27184  logfacrlim  27185  logexprlim  27186  mersenne  27188  perfect1  27189  perfectlem1  27190  perfectlem2  27191  perfect  27192  dchrelbasd  27200  dchrmullid  27213  dchrfi  27216  dchrsum2  27229  sumdchr2  27231  bcp1ctr  27240  bposlem8  27252  zabsle1  27257  lgslem1  27258  lgslem2  27259  lgsfcl2  27264  lgsvalmod  27277  lgsneg  27282  lgsdilem  27285  lgsdir2lem1  27286  lgsdir2lem2  27287  lgsdir2lem3  27288  lgsdir2lem5  27290  lgsdir2  27291  lgsdir  27293  lgsdi  27295  lgsne0  27296  lgseisenlem1  27336  lgseisenlem2  27337  lgseisen  27340  lgsquadlem1  27341  lgsquadlem2  27342  lgsquad2lem1  27345  lgsquad2  27347  m1lgs  27349  2lgslem3c  27359  2lgsoddprmlem3c  27373  2lgsoddprmlem3d  27374  2sqlem10  27389  2sqlem11  27390  2sqblem  27392  addsqn2reu  27402  addsqrexnreu  27403  addsqnreup  27404  chtppilimlem2  27435  chebbnd2  27438  chto1lb  27439  rplogsumlem1  27445  rpvmasumlem  27448  dchrmusumlema  27454  dchrmusum2  27455  dchrisum0flblem1  27469  rpvmasum2  27473  mudivsum  27491  mulogsum  27493  vmalogdivsum2  27499  selberg2lem  27511  logdivbnd  27517  pntrmax  27525  pntrsumo1  27526  pntrsumbnd2  27528  pntrlog2bndlem5  27542  pntpbnd1a  27546  pntpbnd2  27548  pntibndlem2  27552  pntlemd  27555  pntlemc  27556  pntlemr  27563  brbtwn2  28830  colinearalglem4  28834  ax5seglem1  28853  ax5seglem2  28854  ax5seglem3  28856  ax5seglem5  28858  ax5seglem7  28860  ax5seglem9  28862  axbtwnid  28864  axpaschlem  28865  axlowdimlem13  28879  axlowdimlem14  28880  axlowdimlem16  28882  axeuclidlem  28887  axcontlem2  28890  axcontlem4  28892  axcontlem7  28895  axcontlem8  28896  crctcshwlkn0lem6  29743  clwwlkf1  29976  clwwlknonex2lem2  30035  ex-fl  30374  ex-ind-dvds  30388  vc2OLD  30495  vc0  30501  vcm  30503  nvm1  30592  nvmtri  30598  nvge0  30600  ipval2lem3  30632  ipidsq  30637  lnoadd  30685  ip1ilem  30753  ip1i  30754  ip2i  30755  ipdirilem  30756  ipasslem1  30758  ipasslem2  30759  ipasslem10  30766  minvecolem2  30802  hvsubid  30953  hv2times  30988  hisubcomi  31031  normlem9  31045  normlem7tALT  31046  norm-ii-i  31064  normsubi  31068  hhssnv  31191  pjhthlem1  31318  h1de2bi  31481  homullid  31727  ho2times  31746  lnop0  31893  lnopaddi  31898  lnophmlem2  31944  lnfn0i  31969  lnfnaddi  31970  hst1h  32154  sto2i  32164  stadd3i  32175  addltmulALT  32373  sgnneg  32758  dpmul4  32834  psgnid  33054  cnmsgn0g  33103  altgnsg  33106  isarchi3  33131  archirngz  33133  1fldgenq  33262  ply1dg3rt0irred  33541  ccfldextdgrr  33659  constrsscn  33720  constrabscl  33758  cos9thpiminplylem1  33762  cos9thpiminplylem4  33765  cos9thpiminplylem5  33766  lmatfvlem  33792  qqhval2lem  33958  dya2ub  34248  omssubadd  34278  eulerpartlemgs2  34358  fib5  34383  fib6  34384  ballotlem2  34467  signswch  34539  signlem0  34565  itgexpif  34584  reprlt  34597  breprexp  34611  breprexpnat  34612  hgt750lem2  34630  subfacp1lem5  35152  subfacp1lem6  35153  subfacval2  35155  subfaclim  35156  subfacval3  35157  cvxsconn  35211  resconn  35214  cvmliftlem7  35259  cvmliftlem10  35262  problem4  35636  sinccvglem  35640  sqdivzi  35691  faclimlem1  35706  dnibndlem5  36446  dnibndlem10  36451  ltflcei  37578  sin2h  37580  cos2h  37581  tan2h  37582  poimirlem13  37603  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem31  37621  mblfinlem2  37628  mblfinlem3  37629  dvtan  37640  itg2addnclem3  37643  dvasin  37674  dvacos  37675  areacirc  37683  fdc  37715  mettrifi  37727  heiborlem4  37784  heiborlem6  37786  60gcd7e1  41964  lcmineqlem1  41988  lcmineqlem8  41995  lcmineqlem9  41996  lcmineqlem10  41997  lcmineqlem12  41999  3exp7  42012  3lexlogpow5ineq1  42013  3lexlogpow5ineq5  42019  aks4d1p1p4  42030  aks4d1p1p7  42033  aks4d1p1  42035  facp2  42102  fac2xp3  42198  2xp3dxp2ge1d  42200  factwoffsmonot  42201  sn-1ne2  42262  sqdeccom12  42286  235t711  42301  re1m1e0m0  42387  ipiiie0  42427  sn-0tie0  42429  fltnltalem  42632  sum9cubes  42642  3cubeslem3l  42656  3cubeslem3r  42657  eldioph2lem1  42730  lzenom  42740  irrapxlem1  42792  rmspecsqrtnq  42876  rmxm1  42905  rmym1  42906  2nn0ind  42916  jm2.24nn  42930  jm2.17a  42931  jm2.17b  42932  jm2.17c  42933  jm2.24  42934  acongeq  42954  jm2.18  42959  jm2.27c  42978  jm3.1lem2  42989  rngunsnply  43140  flcidc  43141  inductionexd  44126  unitadd  44166  hashnzfzclim  44294  ofdivrec  44298  lhe4.4ex1a  44301  expgrowth  44307  dvradcnv2  44319  binomcxplemrat  44322  binomcxplemnotnn0  44328  isosctrlem1ALT  44906  monoord2xrv  45458  dvsinax  45890  dvnprodlem3  45925  itgsin0pilem1  45927  itgsbtaddcnst  45959  stoweidlem13  45990  stoweidlem26  46003  stoweidlem34  46011  stoweidlem38  46015  wallispilem2  46043  wallispilem4  46045  wallispi2lem1  46048  stirlinglem1  46051  stirlinglem5  46055  stirlinglem10  46060  dirkerper  46073  dirkertrigeqlem1  46075  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncflem4  46083  fourierdlem24  46108  sqwvfoura  46205  sqwvfourb  46206  fourierswlem  46207  lambert0  46867  lamberte  46868  1t10e1p1e11  47287  ceil5half3  47317  fmtnorec3  47510  fmtno5lem4  47518  fmtno5  47519  257prm  47523  fmtno4nprmfac193  47536  m3prm  47554  139prmALT  47558  127prm  47561  m7prm  47562  lighneallem3  47569  proththd  47576  3exp4mod41  47578  41prothprmlem2  47580  perfectALTVlem2  47684  perfectALTV  47685  11t31e341  47694  evengpop3  47760  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  bgoldbtbndlem1  47767  0nodd  48093  altgsumbcALT  48276  exple2lt6  48287  nn0sumshdiglemB  48548  ackval3  48611  ackval3012  48620  line2ylem  48679  onetansqsecsq  49573  cotsqcscsq  49574  5m4e1  49609