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  11305  peano2cn  11307  mul02lem2  11312  addrid  11315  cnegex2  11317  peano2cnm  11449  0reALT  11480  ine0  11574  mulm1  11580  0lt1  11661  ixi  11768  muleqadd  11783  reccl  11805  recne0  11811  recid  11812  recid2  11813  diveq1  11828  div1  11833  1div1e1  11834  recdiv  11850  divdiv1  11855  divdiv2  11856  recdiv2  11857  conjmul  11861  eqneg  11864  div2neg  11867  recp1lt1  12043  recreclt  12044  recgt0ii  12051  neg1cn  12133  neg1ne0  12135  negneg1e1  12137  ofnegsub  12146  peano5nni  12166  nnsscn  12168  nn1m1nn  12184  nn1suc  12185  nnaddcl  12186  nnmulcl  12187  nnne0  12200  nnsub  12210  1m1e0  12242  2cn  12245  3cn  12251  4cn  12255  5cn  12258  6cn  12261  7cn  12264  8cn  12267  9cn  12270  1pneg1e0  12284  1m0e1  12286  0p1e1  12287  1p0e1  12289  2m1e1  12291  3m1e2  12293  4m1e3  12294  5m1e4  12295  6m1e5  12296  7m1e6  12297  8m1e7  12298  9m1e8  12299  2p2e4  12300  1p2e3  12308  1p2e3ALT  12309  3p2e5  12316  3p3e6  12317  4p2e6  12318  4p3e7  12319  4p4e8  12320  5p2e7  12321  5p3e8  12322  5p4e9  12323  6p2e8  12324  6p3e9  12325  7p2e9  12326  1t1e1  12327  3t3e9  12332  neg1mulneg1e1  12378  1mhlfehlf  12385  8th4div3  12386  halfthird  12387  halfpm6th  12388  addltmul  12402  elnn0nn  12468  elz2  12531  zlem1lt  12568  zltlem1  12569  nnaddm1cl  12575  zextlt  12592  zeo  12604  peano5uzi  12607  numsuc  12647  numltc  12659  numsucc  12673  numaddc  12681  6p5lem  12703  5p5e10  12704  6p4e10  12705  7p3e10  12708  8p2e10  12713  10m1e9  12729  4t3lem  12730  7t4e28  12744  9t11e99  12763  decbin2  12774  5recm6rec  12776  uzp1  12814  peano2uzr  12842  uzaddcl  12843  rebtwnz  12886  qbtwnre  13140  iccf1o  13438  fz01en  13495  fztp  13523  fzsuc2  13525  fztpval  13529  fseq1m1p1  13542  elfzp1b  13544  predfz  13596  fzoss2  13631  fzval3  13678  fzosplitsnm1  13684  fzo1to4tp  13698  fldiv4p1lem1div2  13783  ceim1l  13795  fldiv  13808  uzrdgxfr  13918  fzen2  13920  nn0ennn  13930  seqm1  13970  seqshft2  13979  monoord2  13984  sermono  13985  seqf1olem1  13992  seqf1olem2  13993  seqz  14001  ser1const  14009  expcl  14030  expclzlem  14034  m1expcl2  14036  expm1t  14041  1exp  14042  mulexpz  14053  expadd  14055  expaddz  14057  expmul  14058  expubnd  14129  sqrecii  14134  neg1sqe1  14147  irec  14152  i4  14155  binom21  14170  sq01  14176  crreczi  14179  bernneq  14180  bernneq2  14181  nn0opthlem1  14219  facndiv  14239  faclbnd4lem1  14244  faclbnd6  14250  bcnp1n  14265  bcm1k  14266  bcp1nk  14268  bcn2  14270  bcp1m1  14271  bcpasc  14272  hashgadd  14328  hashfz  14378  hashfzo  14380  hashxplem  14384  hashbclem  14403  hashf1  14408  seqcoll  14415  swrds1  14618  swrdlsw  14619  wrdind  14673  wrd2ind  14674  swrds2  14891  relexpaddg  15004  rei  15107  imi  15108  recan  15288  iserex  15608  isercoll2  15620  serf0  15632  iseraltlem2  15634  iseraltlem3  15635  iseralt  15636  sumrblem  15662  fsumm1  15702  telfsumo  15754  fsumparts  15758  hashiun  15774  binomlem  15783  binom  15784  binom1p  15785  binom11  15786  binom1dif  15787  bcxmas  15789  isumsplit  15794  isum1p  15795  climcndslem1  15803  supcvg  15810  harmonic  15813  arisum  15814  arisum2  15815  trireciplem  15816  geoserg  15820  geolim  15824  geolim2  15825  georeclim  15826  geo2sum  15827  geo2sum2  15828  geoisum1c  15834  0.999...  15835  geoihalfsum  15836  cvgrat  15837  mertenslem1  15838  mertenslem2  15839  mertens  15840  prodf1  15845  prodfclim1  15847  prodrblem  15883  fprodcvg  15884  prodmolem2a  15888  zprod  15891  fprodntriv  15896  prodss  15901  fprodss  15902  fprodsplit  15920  fprodn0f  15945  risefaccl  15969  fallfaccl  15970  risefacfac  15989  binomfallfac  15995  bpolycl  16006  bpolysum  16007  bpolydiflem  16008  fsumkthpow  16010  bpoly2  16011  bpoly3  16012  bpoly4  16013  fsumcube  16014  esum  16034  ege2le3  16044  efsub  16056  efexp  16057  efzval  16058  eftlub  16065  effsumlt  16067  ef4p  16069  tanval3  16090  efi4p  16093  tan0  16107  efival  16108  tanadd  16123  cos2t  16134  cos2tsin  16135  ef01bndlem  16140  cos1bnd  16143  cos2bnd  16144  demoivreALT  16157  eirrlem  16160  rpnnen2lem3  16172  rpnnen2lem11  16180  ruclem12  16197  3dvds  16289  3dvdsdec  16290  3dvds2dec  16291  odd2np1lem  16298  odd2np1  16299  opoe  16321  omoe  16322  opeo  16323  omeo  16324  n2dvdsm1  16327  m1exp1  16334  flodddiv4  16373  bitsfzo  16393  sqgcd  16520  expgcd  16521  nn0seqcvgd  16528  prmind2  16643  hashdvds  16734  phiprmpw  16735  phiprm  16736  eulerthlem2  16741  iserodd  16795  sumhash  16856  fldivp1  16857  prmpwdvds  16864  pockthlem  16865  pockthi  16867  prmreclem4  16879  prmreclem6  16881  4sqlem11  16915  4sqlem19  16923  vdwapun  16934  vdwapid1  16935  vdwlem3  16943  vdwlem5  16945  vdwlem6  16946  vdwlem8  16948  vdwlem9  16949  vdwnnlem2  16956  ramub1lem1  16986  ramub1lem2  16987  ramcl  16989  prmo1  16997  dec5nprm  17026  prmlem0  17065  43prm  17081  83prm  17082  139prm  17083  163prm  17084  317prm  17085  631prm  17086  1259lem2  17091  1259lem3  17092  1259lem4  17093  1259lem5  17094  1259prm  17095  2503lem1  17096  2503lem2  17097  2503lem3  17098  2503prm  17099  4001lem1  17100  4001lem2  17101  4001lem3  17102  4001lem4  17103  4001prm  17104  gsumsgrpccat  18797  mulgnndir  19068  mulgneg2  19073  m1expaddsub  19462  sylow1lem1  19562  sylow2a  19583  efgsval2  19697  efgsrel  19698  efgsres  19702  cncrng  21362  cnfld1  21366  zsssubrg  21394  cnmgpid  21398  zringcyg  21438  mulgrhm2  21447  pzriprng1ALT  21465  cnmsgnsubg  21546  cnmsgnbas  21547  cnmsgngrp  21548  psgninv  21551  evpmodpmf1o  21565  psdmplcl  22117  blcvx  24751  iihalf2  24888  icopnfcnv  24897  iccpnfhmeo  24900  xrhmeo  24901  icccvx  24905  lebnumii  24921  reparphti  24952  pcoass  24979  pcorevlem  24981  pcorev2  24983  pi1xfrcnv  25012  cnstrcvs  25096  cncvs  25100  ncvsm1  25109  pjthlem1  25392  divcncf  25402  ovolunlem1a  25451  ovolunlem1  25452  ovolicc2lem4  25475  uniioombllem3  25540  uniioombllem4  25541  dyadovol  25548  vitalilem4  25566  mbf0  25589  iblcnlem1  25743  itgcnlem  25745  dvid  25873  dvexp  25908  dvexp2  25909  dvexp3  25933  dveflem  25934  dvlipcn  25949  dvcvx  25975  dvfsumle  25976  dvfsumlem1  25981  degltp1le  26026  ply1divex  26090  fta1glem1  26121  plyaddlem1  26166  plymullem1  26167  coeidp  26216  dgrid  26217  dvply1  26238  dvply2g  26239  plyremlem  26258  fta1lem  26261  vieta1lem1  26264  vieta1lem2  26265  qaa  26277  iaa  26279  aalioulem3  26288  geolim3  26293  aaliou3lem2  26297  aaliou3lem7  26303  taylply2  26321  dvradcnv  26374  pserdvlem2  26381  pserdv2  26383  abelthlem1  26384  abelthlem2  26385  abelthlem6  26389  abelthlem7  26391  abelth  26394  reeff1olem  26399  reeff1o  26400  efcvx  26402  sinhalfpilem  26415  eulerid  26426  cos2pi  26428  sincosq3sgn  26452  sincosq4sgn  26453  tangtx  26457  sincos4thpi  26465  sincos6thpi  26468  pigt3  26470  pige3ALT  26472  abssinper  26473  coskpi  26475  coseq1  26477  efeq1  26480  tanregt0  26491  logneg2  26567  logdivlti  26572  logcnlem4  26597  dvlog2lem  26604  dvlog2  26605  advlog  26606  advlogexp  26607  logtayl  26612  logtayl2  26614  logccv  26615  cxpval  26616  1cxp  26624  cxpcl  26626  cxpp1  26632  cxpsqrt  26655  dvsqrt  26694  dvcnsqrt  26696  sqrtcn  26702  cxpaddlelem  26703  root1id  26706  root1cj  26708  logrec  26715  logb1  26721  logbmpt  26740  ang180lem1  26761  ang180lem2  26762  ang180lem3  26763  isosctrlem1  26770  isosctrlem2  26771  1cubrlem  26793  1cubr  26794  mcubic  26799  binom4  26802  dquartlem1  26803  quartlem1  26809  asinlem  26820  asinlem2  26821  asinlem3a  26822  asinlem3  26823  asinf  26824  atandm2  26829  atandm4  26831  atanf  26832  asinneg  26838  efiasin  26840  sinasin  26841  asinsin  26844  asin1  26846  acos1  26847  reasinsin  26848  asinbnd  26851  cosasin  26856  atanneg  26859  atancj  26862  efiatan  26864  atanlogaddlem  26865  atanlogadd  26866  atanlogsublem  26867  atanlogsub  26868  efiatan2  26869  2efiatan  26870  tanatan  26871  cosatan  26873  cosatanne0  26874  atantan  26875  atanbndlem  26877  bndatandm  26881  atans2  26883  dvatan  26887  atantayl  26889  atantayl2  26890  atantayl3  26891  leibpilem2  26893  leibpi  26894  log2cnv  26896  log2tlbnd  26897  log2ublem3  26900  log2ub  26901  birthdaylem2  26904  birthday  26906  efrlim  26921  dfef2  26922  cvxcl  26936  scvxcvx  26937  emcllem2  26948  emcllem4  26950  emcllem7  26953  harmonicbnd4  26962  fsumharmonic  26963  zetacvg  26966  lgamcvg2  27006  lgam1  27015  gam1  27016  wilthlem1  27019  wilthlem2  27020  wilthlem3  27021  basellem2  27033  basellem5  27036  basellem6  27037  basellem7  27038  basellem8  27039  basellem9  27040  0sgm  27095  mule1  27099  ppiprm  27102  ppinprm  27103  chtprm  27104  chtnprm  27105  chpp1  27106  mumullem2  27131  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  29871  clwwlkf1  30107  clwwlknonex2lem2  30166  ex-fl  30505  ex-ind-dvds  30519  vc2OLD  30627  vc0  30633  vcm  30635  nvm1  30724  nvmtri  30730  nvge0  30732  ipval2lem3  30764  ipidsq  30769  lnoadd  30817  ip1ilem  30885  ip1i  30886  ip2i  30887  ipdirilem  30888  ipasslem1  30890  ipasslem2  30891  ipasslem10  30898  minvecolem2  30934  hvsubid  31085  hv2times  31120  hisubcomi  31163  normlem9  31177  normlem7tALT  31178  norm-ii-i  31196  normsubi  31200  hhssnv  31323  pjhthlem1  31450  h1de2bi  31613  homullid  31859  ho2times  31878  lnop0  32025  lnopaddi  32030  lnophmlem2  32076  lnfn0i  32101  lnfnaddi  32102  hst1h  32286  sto2i  32296  stadd3i  32307  addltmulALT  32505  sgnneg  32894  dpmul4  32961  psgnid  33146  cnmsgn0g  33195  altgnsg  33198  isarchi3  33236  archirngz  33238  1fldgenq  33371  ply1dg3rt0irred  33632  esplyfvaln  33706  ccfldextdgrr  33804  constrsscn  33872  constrabscl  33910  cos9thpiminplylem1  33914  cos9thpiminplylem4  33917  cos9thpiminplylem5  33918  lmatfvlem  33947  qqhval2lem  34113  dya2ub  34402  omssubadd  34432  eulerpartlemgs2  34512  fib5  34537  fib6  34538  ballotlem2  34621  signswch  34693  signlem0  34719  itgexpif  34738  reprlt  34751  breprexp  34765  breprexpnat  34766  hgt750lem2  34784  subfacp1lem5  35354  subfacp1lem6  35355  subfacval2  35357  subfaclim  35358  subfacval3  35359  cvxsconn  35413  resconn  35416  cvmliftlem7  35461  cvmliftlem10  35464  problem4  35838  sinccvglem  35842  sqdivzi  35898  faclimlem1  35913  dnibndlem5  36730  dnibndlem10  36735  ltflcei  37917  sin2h  37919  cos2h  37920  tan2h  37921  poimirlem13  37942  poimirlem16  37945  poimirlem17  37946  poimirlem19  37948  poimirlem20  37949  poimirlem31  37960  mblfinlem2  37967  mblfinlem3  37968  dvtan  37979  itg2addnclem3  37982  dvasin  38013  dvacos  38014  areacirc  38022  fdc  38054  mettrifi  38066  heiborlem4  38123  heiborlem6  38125  60gcd7e1  42432  lcmineqlem1  42456  lcmineqlem8  42463  lcmineqlem9  42464  lcmineqlem10  42465  lcmineqlem12  42467  3exp7  42480  3lexlogpow5ineq1  42481  3lexlogpow5ineq5  42487  aks4d1p1p4  42498  aks4d1p1p7  42501  aks4d1p1  42503  facp2  42570  1p3e4  42685  sn-1ne2  42691  sqdeccom12  42709  235t711  42725  sin2t3rdpi  42773  cos2t3rdpi  42774  re1m1e0m0  42817  ipiiie0  42858  sn-0tie0  42884  fltnltalem  43083  sum9cubes  43093  3cubeslem3l  43106  3cubeslem3r  43107  eldioph2lem1  43180  lzenom  43190  irrapxlem1  43238  rmspecsqrtnq  43322  rmxm1  43350  rmym1  43351  2nn0ind  43361  jm2.24nn  43375  jm2.17a  43376  jm2.17b  43377  jm2.17c  43378  jm2.24  43379  acongeq  43399  jm2.18  43404  jm2.27c  43423  jm3.1lem2  43434  rngunsnply  43585  flcidc  43586  inductionexd  44570  unitadd  44610  hashnzfzclim  44737  ofdivrec  44741  lhe4.4ex1a  44744  expgrowth  44750  dvradcnv2  44762  binomcxplemrat  44765  binomcxplemnotnn0  44771  isosctrlem1ALT  45348  monoord2xrv  45899  dvsinax  46329  dvnprodlem3  46364  itgsin0pilem1  46366  itgsbtaddcnst  46398  stoweidlem13  46429  stoweidlem26  46442  stoweidlem34  46450  stoweidlem38  46454  wallispilem2  46482  wallispilem4  46484  wallispi2lem1  46487  stirlinglem1  46490  stirlinglem5  46494  stirlinglem10  46499  dirkerper  46512  dirkertrigeqlem1  46514  dirkertrigeqlem3  46516  dirkertrigeq  46517  dirkercncflem4  46522  fourierdlem24  46547  sqwvfoura  46644  sqwvfourb  46645  fourierswlem  46646  cos5t  47315  goldratmolem2  47322  lambert0  47323  lamberte  47324  cjnpoly  47325  1t10e1p1e11  47746  ceil5half3  47782  modm2nep1  47808  modm1nep2  47810  modm1nem2  47811  fmtnorec3  47999  fmtno5lem4  48007  fmtno5  48008  257prm  48012  fmtno4nprmfac193  48025  m3prm  48043  139prmALT  48047  127prm  48050  m7prm  48051  lighneallem3  48058  proththd  48065  3exp4mod41  48067  41prothprmlem2  48069  perfectALTVlem2  48186  perfectALTV  48187  11t31e341  48196  evengpop3  48262  nnsum4primeseven  48264  nnsum4primesevenALTV  48265  bgoldbtbndlem1  48269  0nodd  48634  altgsumbcALT  48817  exple2lt6  48828  nn0sumshdiglemB  49084  ackval3  49147  ackval3012  49156  line2ylem  49215  onetansqsecsq  50224  cotsqcscsq  50225  5m4e1  50260