Axiom ax-1cn 11258

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

This axiom is used by:  0cn  11298  1cnd  11302  1ex  11303  mulrid  11306  mullid  11307  1re  11308  0re  11310  muladd11  11480  peano2cn  11482  mul02lem2  11487  addrid  11490  cnegex2  11492  peano2cnm  11624  0reALT  11655  ine0  11751  mulm1  11757  0lt1  11838  ixi  11945  muleqadd  11960  reccl  11981  recne0  11987  recid  11988  recid2  11989  diveq1  12003  div1  12006  1div1e1  12007  recdiv  12023  divdiv1  12028  divdiv2  12029  recdiv2  12030  conjmul  12034  eqneg  12037  div2neg  12040  recp1lt1  12215  recreclt  12216  recgt0ii  12223  neg1cn  12305  neg1ne0  12307  negneg1e1  12309  ofnegsub  12318  peano5nni  12338  nnsscn  12340  nn1m1nn  12356  nn1suc  12357  nnaddcl  12358  nnmulcl  12359  nnne0  12372  nnsub  12382  1m1e0  12415  2cn  12418  3cn  12424  4cn  12428  5cn  12431  6cn  12434  7cn  12437  8cn  12440  9cn  12443  1pneg1e0  12460  1m0e1  12462  0p1e1  12463  1p0e1  12465  2m1e1  12467  2m1e1OLD  12468  3m1e2  12470  4m1e3  12471  5m1e4  12472  6m1e5  12473  7m1e6  12474  8m1e7  12475  9m1e8  12476  2p2e4  12477  1p2e3  12485  1p2e3ALT  12486  3p2e5  12493  3p3e6  12494  4p2e6  12495  4p3e7  12496  4p4e8  12497  5p2e7  12498  5p3e8  12499  5p4e9  12500  6p2e8  12501  6p3e9  12502  7p2e9  12503  1t1e1  12504  3t3e9  12510  neg1mulneg1e1  12558  1mhlfehlf  12565  8th4div3  12566  halfthird  12567  halfpm6th  12568  addltmul  12582  elnn0nn  12648  elz2  12711  zlem1lt  12748  zltlem1  12749  nnaddm1cl  12756  zextlt  12773  zeo  12785  peano5uzi  12788  numsuc  12828  numltc  12845  numsucc  12859  numaddc  12867  6p5lem  12889  5p5e10  12890  6p4e10  12891  7p3e10  12894  8p2e10  12899  10m1e9  12915  4t3lem  12916  7t4e28  12930  9t11e99OLD  12950  decbin2  12962  5recm6rec  12964  uzp1  13002  peano2uzr  13030  uzaddcl  13031  rebtwnz  13074  qbtwnre  13329  iccf1o  13627  fz01en  13686  fztp  13714  fzsuc2  13716  fztpval  13720  fseq1m1p1  13733  elfzp1b  13735  predfz  13787  fzoss2  13822  fzval3  13869  fzosplitsnm1  13875  fzo1to4tp  13889  fldiv4p1lem1div2  13975  ceim1l  13987  fldiv  14000  uzrdgxfr  14110  fzen2  14112  nn0ennn  14122  seqm1  14162  seqshft2  14171  monoord2  14176  sermono  14177  seqf1olem1  14184  seqf1olem2  14185  seqz  14193  ser1const  14201  expcl  14222  expclzlem  14226  m1expcl2  14228  expm1t  14233  1exp  14234  mulexpz  14245  expadd  14247  expaddz  14249  expmul  14250  expubnd  14321  sqrecii  14326  neg1sqe1  14339  irec  14345  i4  14348  binom21  14363  sq01  14369  crreczi  14372  bernneq  14373  bernneq2  14374  nn0opthlem1  14412  facndiv  14432  faclbnd4lem1  14437  faclbnd6  14443  bcnp1n  14458  bcm1k  14459  bcp1nk  14461  bcn2  14463  bcp1m1  14464  bcpasc  14465  hashgadd  14521  hashfz  14572  hashfzo  14574  hashxplem  14578  hashbclem  14597  hashf1  14602  seqcoll  14609  swrds1  14816  swrdlsw  14817  wrdind  14871  wrd2ind  14872  swrds2  15091  relexpaddg  15206  sgnneg  15253  rei  15323  imi  15324  recan  15504  iserex  15824  isercoll2  15836  serf0  15848  iseraltlem2  15850  iseraltlem3  15851  iseralt  15852  sumrblem  15877  fsumm1  15917  telfsumo  15969  fsumparts  15973  hashiun  15989  binomlem  15998  binom  15999  binom1p  16000  binom11  16001  binom1dif  16002  bcxmas  16004  isumsplit  16009  isum1p  16010  climcndslem1  16018  supcvg  16025  harmonic  16028  arisum  16029  arisum2  16030  trireciplem  16031  geoserg  16035  geolim  16039  geolim2  16040  georeclim  16041  geo2sum  16042  geo2sum2  16043  geoisum1c  16049  0.999...  16050  geoihalfsum  16051  cvgrat  16052  mertenslem1  16053  mertenslem2  16054  mertens  16055  prodf1  16060  prodfclim1  16062  prodrblem  16096  fprodcvg  16097  prodmolem2a  16101  zprod  16104  fprodntriv  16109  prodss  16114  fprodss  16115  fprodsplit  16133  fprodn0f  16158  risefaccl  16182  fallfaccl  16183  risefacfac  16201  binomfallfac  16207  bpolycl  16218  bpolysum  16219  bpolydiflem  16220  fsumkthpow  16222  bpoly2  16223  bpoly3  16224  bpoly4  16225  fsumcube  16226  esum  16246  ege2le3  16256  efsub  16268  efexp  16269  efzval  16270  eftlub  16277  effsumlt  16279  ef4p  16281  tanval3  16302  efi4p  16305  tan0  16319  efival  16320  tanadd  16335  cos2t  16346  cos2tsin  16347  ef01bndlem  16352  cos1bnd  16355  cos2bnd  16356  demoivreALT  16369  eirrlem  16372  rpnnen2lem3  16384  rpnnen2lem11  16392  ruclem12  16409  3dvds  16501  3dvdsdec  16502  3dvds2dec  16503  odd2np1lem  16510  odd2np1  16511  opoe  16533  omoe  16534  opeo  16535  omeo  16536  n2dvdsm1  16539  m1exp1  16546  flodddiv4  16585  bitsfzo  16605  sqgcd  16736  expgcd  16737  nn0seqcvgd  16745  prmind2  16860  hashdvds  16952  phiprmpw  16953  phiprm  16954  eulerthlem2  16959  iserodd  17013  sumhash  17074  fldivp1  17075  prmpwdvds  17082  pockthlem  17083  pockthi  17085  prmreclem4  17097  prmreclem6  17099  4sqlem11  17133  4sqlem19  17141  vdwapun  17152  vdwapid1  17153  vdwlem3  17161  vdwlem5  17163  vdwlem6  17164  vdwlem8  17166  vdwlem9  17167  vdwnnlem2  17174  ramub1lem1  17204  ramub1lem2  17205  ramcl  17207  prmo1  17215  dec5nprm  17244  prmlem0  17283  43prm  17300  83prm  17301  139prm  17302  163prm  17303  317prm  17304  631prm  17305  1259lem2  17310  1259lem3  17311  1259lem4  17312  1259lem5  17313  1259prm  17314  2503lem1  17315  2503lem2  17316  2503lem3  17317  2503prm  17318  4001lem1  17319  4001lem2  17320  4001lem3  17321  4001lem4  17322  4001prm  17323  gsumsgrpccat  19036  mulgnndir  19313  mulgneg2  19318  m1expaddsub  19712  sylow1lem1  19812  sylow2a  19833  efgsval2  19947  efgsrel  19948  efgsres  19952  cncrng  21699  cnfld1  21703  zsssubrg  21731  cnmgpid  21735  zringcyg  21775  mulgrhm2  21784  pzriprng1ALT  21802  cnmsgnsubg  21883  cnmsgnbas  21884  cnmsgngrp  21885  psgninv  21888  evpmodpmf1o  21902  psdmplcl  22483  blcvx  25117  iihalf2  25254  icopnfcnv  25263  iccpnfhmeo  25266  xrhmeo  25267  icccvx  25271  lebnumii  25287  reparphti  25318  pcoass  25345  pcorevlem  25347  pcorev2  25349  pi1xfrcnv  25378  cnstrcvs  25462  cncvs  25466  ncvsm1  25475  pjthlem1  25758  divcncf  25768  ovolunlem1a  25817  ovolunlem1  25818  ovolicc2lem4  25841  uniioombllem3  25906  uniioombllem4  25907  dyadovol  25914  vitalilem4  25932  mbf0  25955  iblcnlem1  26108  itgcnlem  26110  dvid  26238  dvexp  26273  dvexp2  26274  dvexp3  26298  dveflem  26299  dvlipcn  26314  dvcvx  26340  dvfsumle  26341  dvfsumlem1  26346  degltp1le  26391  ply1divex  26455  fta1glem1  26486  plyaddlem1  26532  plymullem1  26533  coeidp  26582  dgrid  26583  dvply1  26605  dvply2g  26606  plyremlem  26625  fta1lem  26628  vieta1lem1  26633  vieta1lem2  26634  qaa  26647  iaa  26651  iaaOLD  26652  aalioulem3  26661  geolim3  26666  aaliou3lem2  26670  aaliou3lem7  26676  taylply2  26695  dvradcnv  26748  pserdvlem2  26755  pserdv2  26757  abelthlem1  26758  abelthlem2  26759  abelthlem6  26763  abelthlem7  26765  abelth  26768  reeff1olem  26773  reeff1o  26774  efcvx  26776  sinhalfpilem  26792  eulerid  26803  cos2pi  26805  sincosq3sgn  26829  sincosq4sgn  26830  tangtx  26834  sincos4thpi  26842  sincos6thpi  26844  pigt3  26846  pige3ALT  26848  abssinper  26849  coskpi  26851  coseq1  26853  efeq1  26856  tanregt0  26867  logneg2  26943  logdivlti  26948  logcnlem4  26973  dvlog2lem  26980  dvlog2  26981  advlog  26982  advlogexp  26983  logtayl  26988  logtayl2  26990  logccv  26991  cxpval  26992  1cxp  27000  cxpcl  27002  cxpp1  27008  cxpsqrt  27031  dvsqrt  27070  dvcnsqrt  27072  sqrtcn  27078  cxpaddlelem  27079  root1id  27082  root1cj  27084  logrec  27091  logb1  27097  logbmpt  27116  ang180lem1  27137  ang180lem2  27138  ang180lem3  27139  isosctrlem1  27146  isosctrlem2  27147  1cubrlem  27169  1cubr  27170  mcubic  27175  binom4  27178  dquartlem1  27179  quartlem1  27185  asinlem  27196  asinlem2  27197  asinlem3a  27198  asinlem3  27199  asinf  27200  atandm2  27205  atandm4  27207  atanf  27208  asinneg  27214  efiasin  27216  sinasin  27217  asinsin  27220  asin1  27222  acos1  27223  reasinsin  27224  asinbnd  27227  cosasin  27232  atanneg  27235  atancj  27238  efiatan  27240  atanlogaddlem  27241  atanlogadd  27242  atanlogsublem  27243  atanlogsub  27244  efiatan2  27245  2efiatan  27246  tanatan  27247  cosatan  27249  cosatanne0  27250  atantan  27251  atanbndlem  27253  bndatandm  27257  atans2  27259  dvatan  27263  atantayl  27265  atantayl2  27266  atantayl3  27267  leibpilem2  27269  leibpi  27270  log2cnv  27272  log2tlbnd  27273  log2ublem3  27276  log2ub  27277  birthdaylem2  27280  birthday  27282  efrlim  27297  dfef2  27298  cvxcl  27312  scvxcvx  27313  emcllem2  27324  emcllem4  27326  emcllem7  27329  harmonicbnd4  27338  fsumharmonic  27339  zetacvg  27342  lgamcvg2  27382  lgam1  27391  gam1  27392  wilthlem1  27395  wilthlem2  27396  wilthlem3  27397  basellem2  27409  basellem5  27412  basellem6  27413  basellem7  27414  basellem8  27415  basellem9  27416  0sgm  27471  mule1  27475  ppiprm  27478  ppinprm  27479  chtprm  27480  chtnprm  27481  chpp1  27482  mumullem2  27507  1sgmprm  27526  1sgm2ppw  27527  ppiub  27531  chtublem  27538  chtub  27539  logfaclbnd  27549  logfacbnd3  27550  logfacrlim  27551  logexprlim  27552  mersenne  27554  perfect1  27555  perfectlem1  27556  perfectlem2  27557  perfect  27558  dchrelbasd  27566  dchrmullid  27579  dchrfi  27582  dchrsum2  27595  sumdchr2  27597  bcp1ctr  27606  bposlem8  27618  zabsle1  27623  lgslem1  27624  lgslem2  27625  lgsfcl2  27630  lgsvalmod  27643  lgsneg  27648  lgsdilem  27651  lgsdir2lem1  27652  lgsdir2lem2  27653  lgsdir2lem3  27654  lgsdir2lem5  27656  lgsdir2  27657  lgsdir  27659  lgsdi  27661  lgsne0  27662  lgseisenlem1  27702  lgseisenlem2  27703  lgseisen  27706  lgsquadlem1  27707  lgsquadlem2  27708  lgsquad2lem1  27711  lgsquad2  27713  m1lgs  27715  2lgslem3c  27725  2lgsoddprmlem3c  27739  2lgsoddprmlem3d  27740  2sqlem10  27755  2sqlem11  27756  2sqblem  27758  addsqn2reu  27768  addsqrexnreu  27769  addsqnreup  27770  chtppilimlem2  27801  chebbnd2  27804  chto1lb  27805  rplogsumlem1  27811  rpvmasumlem  27814  dchrmusumlema  27820  dchrmusum2  27821  dchrisum0flblem1  27835  rpvmasum2  27839  mudivsum  27857  mulogsum  27859  vmalogdivsum2  27865  selberg2lem  27877  logdivbnd  27883  pntrmax  27891  pntrsumo1  27892  pntrsumbnd2  27894  pntrlog2bndlem5  27908  pntpbnd1a  27912  pntpbnd2  27914  pntibndlem2  27918  pntlemd  27921  pntlemc  27922  pntlemr  27929  brbtwn2  29483  colinearalglem4  29487  ax5seglem1  29506  ax5seglem2  29507  ax5seglem3  29509  ax5seglem5  29511  ax5seglem7  29513  ax5seglem9  29515  axbtwnid  29517  axpaschlem  29518  axlowdimlem13  29532  axlowdimlem14  29533  axlowdimlem16  29535  axeuclidlem  29540  axcontlem2  29543  axcontlem4  29545  axcontlem7  29548  axcontlem8  29549  crctcshwlkn0lem6  30404  clwwlkf1  30640  clwwlknonex2lem2  30699  ex-fl  31048  ex-ind-dvds  31062  vc2OLD  31170  vc0  31176  vcm  31178  nvm1  31267  nvmtri  31273  nvge0  31275  ipval2lem3  31307  ipidsq  31312  lnoadd  31360  ip1ilem  31428  ip1i  31429  ip2i  31430  ipdirilem  31431  ipasslem1  31433  ipasslem2  31434  ipasslem10  31441  minvecolem2  31477  hvsubid  31628  hv2times  31663  hisubcomi  31706  normlem9  31720  normlem7tALT  31721  norm-ii-i  31739  normsubi  31743  hhssnv  31866  pjhthlem1  31993  h1de2bi  32156  homullid  32402  ho2times  32421  lnop0  32568  lnopaddi  32573  lnophmlem2  32619  lnfn0i  32644  lnfnaddi  32645  hst1h  32829  sto2i  32839  stadd3i  32850  addltmulALT  33090  dpmul4  33522  psgnid  33700  cnmsgn0g  33749  altgnsg  33752  isarchi3  33790  archirngz  33792  1fldgenq  33926  ply1dg3rt0irred  34158  esplyfvaln  34248  ccfldextdgrr  34346  constrsscn  34414  constrabscl  34452  cos9thpiminplylem1  34456  cos9thpiminplylem4  34459  cos9thpiminplylem5  34460  lmatfvlem  34489  qqhval2lem  34655  dya2ub  34944  omssubadd  34974  eulerpartlemgs2  35054  fib5  35079  fib6  35080  ballotlem2  35163  signswch  35232  signlem0  35258  itgexpif  35277  reprlt  35290  breprexp  35304  breprexpnat  35305  hgt750lem2  35323  subfacp1lem5  35991  subfacp1lem6  35992  subfacval2  35994  subfaclim  35995  subfacval3  35996  cvxsconn  36050  resconn  36053  cvmliftlem7  36098  cvmliftlem10  36101  problem4  36475  sinccvglem  36479  sqdivzi  36535  faclimlem1  36550  dnibndlem5  37390  dnibndlem10  37395  ltflcei  38574  sin2h  38576  cos2h  38577  tan2h  38578  poimirlem13  38594  poimirlem16  38597  poimirlem17  38598  poimirlem19  38600  poimirlem20  38601  poimirlem31  38612  mblfinlem2  38619  mblfinlem3  38620  dvtan  38631  itg2addnclem3  38634  dvasin  38665  dvacos  38666  areacirc  38674  fdc  38722  mettrifi  38734  heiborlem4  38791  heiborlem6  38793  60gcd7e1  43098  lcmineqlem1  43122  lcmineqlem8  43129  lcmineqlem9  43130  lcmineqlem10  43131  lcmineqlem12  43133  3exp7  43146  3lexlogpow5ineq1  43147  3lexlogpow5ineq5  43153  aks4d1p1p4  43164  aks4d1p1p7  43167  aks4d1p1  43169  facp2  43236  25or6to4  43299  1p3e4  43353  1p4e5  43354  1p5e6  43355  1p6e7  43356  1p7e8  43357  1p8e9  43358  2p3e5  43359  4p5e9  43367  sn-1ne2  43373  sqdeccom12  43389  235t711  43405  sin2t3rdpi  43447  cos2t3rdpi  43448  re1m1e0m0  43491  ipiiie0  43532  sn-0tie0  43558  fltnltalem  43716  sum9cubes  43726  3cubeslem3l  43739  3cubeslem3r  43740  eldioph2lem1  43813  lzenom  43823  irrapxlem1  43871  rmspecsqrtnq  43955  rmxm1  43983  rmym1  43984  2nn0ind  43994  jm2.24nn  44008  jm2.17a  44009  jm2.17b  44010  jm2.17c  44011  jm2.24  44012  acongeq  44032  jm2.18  44037  jm2.27c  44056  jm3.1lem2  44067  rngunsnply  44213  flcidc  44214  inductionexd  45197  unitadd  45237  hashnzfzclim  45348  ofdivrec  45352  lhe4.4ex1a  45355  expgrowth  45361  dvradcnv2  45373  binomcxplemrat  45376  binomcxplemnotnn0  45382  isosctrlem1ALT  45958  monoord2xrv  46535  dvsinax  46965  dvnprodlem3  47000  itgsin0pilem1  47002  itgsbtaddcnst  47034  stoweidlem13  47065  stoweidlem26  47078  stoweidlem34  47086  stoweidlem38  47090  wallispilem2  47118  wallispilem4  47120  wallispi2lem1  47123  stirlinglem1  47126  stirlinglem5  47130  stirlinglem10  47135  dirkerper  47148  dirkertrigeqlem1  47150  dirkertrigeqlem3  47152  dirkertrigeq  47153  dirkercncflem4  47158  fourierdlem24  47183  sqwvfoura  47280  sqwvfourb  47281  fourierswlem  47282  cos5t  47967  goldpolyfactor  47969  goldratmolem2  47975  goldratmolem4  47977  goldratval  47978  lambert0  47979  lamberte  47980  cjnpoly  47981  sqrtnpoly  47985  1t10e1p1e11  48422  ceil5half3  48458  modm2nep1  48484  modm1nep2  48486  modm1nem2  48487  fmtnorec3  48675  fmtno5lem4  48683  fmtno5  48684  257prm  48688  fmtno4nprmfac193  48701  m3prm  48719  139prmALT  48723  127prm  48726  m7prm  48727  lighneallem3  48734  proththd  48741  3exp4mod41  48743  41prothprmlem2  48745  perfectALTVlem2  48862  perfectALTV  48863  11t31e341  48872  evengpop3  48938  nnsum4primeseven  48940  nnsum4primesevenALTV  48941  bgoldbtbndlem1  48945  0nodd  49309  altgsumbcALT  49507  exple2lt6  49518  nn0sumshdiglemB  49774  ackval3  49837  ackval3012  49846  line2ylem  49905  onetansqsecsq  50896  cotsqcscsq  50897  dvsec  50898  dvcsc  50899  dvcot  50900  5m4e1  50977