Axiom ax-1cn 10595

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

This axiom is referenced by:  0cn  10633  1cnd  10636  1ex  10637  mulid1  10639  mulid2  10640  1re  10641  0re  10643  muladd11  10810  peano2cn  10812  mul02lem2  10817  addid1  10820  cnegex2  10822  peano2cnm  10952  0reALT  10983  ine0  11075  mulm1  11081  0lt1  11162  ixi  11269  muleqadd  11284  reccl  11305  recne0  11311  recid  11312  recid2  11313  div1  11329  1div1e1  11330  diveq1  11331  recdiv  11346  divdiv1  11351  divdiv2  11352  recdiv2  11353  conjmul  11357  eqneg  11360  div2neg  11363  recp1lt1  11538  recreclt  11539  recgt0ii  11546  inelr  11628  ofnegsub  11636  peano5nni  11641  nnsscn  11643  nn1m1nn  11659  nn1suc  11660  nnaddcl  11661  nnmulcl  11662  nnne0  11672  nnsub  11682  1m1e0  11710  2cn  11713  3cn  11719  4cn  11723  5cn  11726  6cn  11729  7cn  11732  8cn  11735  9cn  11738  neg1cn  11752  neg1ne0  11754  negneg1e1  11756  1pneg1e0  11757  1m0e1  11759  0p1e1  11760  1p0e1  11762  2m1e1  11764  3m1e2  11766  4m1e3  11767  5m1e4  11768  6m1e5  11769  7m1e6  11770  8m1e7  11771  9m1e8  11772  2p2e4  11773  1p2e3  11781  1p2e3ALT  11782  3p2e5  11789  3p3e6  11790  4p2e6  11791  4p3e7  11792  4p4e8  11793  5p2e7  11794  5p3e8  11795  5p4e9  11796  6p2e8  11797  6p3e9  11798  7p2e9  11799  1t1e1  11800  3t3e9  11805  neg1mulneg1e1  11851  1mhlfehlf  11857  8th4div3  11858  halfpm6th  11859  addltmul  11874  elnn0nn  11940  elz2  12000  zlem1lt  12035  zltlem1  12036  nnaddm1cl  12040  zextlt  12057  zeo  12069  peano5uzi  12072  numsuc  12113  numltc  12125  numsucc  12139  numaddc  12147  6p5lem  12169  5p5e10  12170  6p4e10  12171  7p3e10  12174  8p2e10  12179  10m1e9  12195  4t3lem  12196  7t4e28  12210  9t11e99  12229  decbin2  12240  halfthird  12242  5recm6rec  12243  uzp1  12280  peano2uzr  12304  uzaddcl  12305  rebtwnz  12348  qbtwnre  12593  iccf1o  12883  fz01en  12936  fztp  12964  fzsuc2  12966  fztpval  12970  fseq1m1p1  12983  elfzp1b  12985  fz0to4untppr  13011  predfz  13033  fzoss2  13066  fzval3  13107  fzosplitsnm1  13113  fzo1to4tp  13126  fldiv4p1lem1div2  13206  ceim1l  13216  fldiv  13229  uzrdgxfr  13336  fzen2  13338  nn0ennn  13348  seqm1  13388  seqshft2  13397  monoord2  13402  sermono  13403  seqf1olem1  13410  seqf1olem2  13411  seqz  13419  ser1const  13427  expcl  13448  m1expcl2  13452  expclzlem  13454  expm1t  13458  1exp  13459  mulexpz  13470  expadd  13472  expaddz  13474  expmul  13475  expubnd  13542  sqrecii  13547  neg1sqe1  13560  irec  13565  i4  13568  binom21  13581  sq01  13587  crreczi  13590  bernneq  13591  bernneq2  13592  nn0opthlem1  13629  facndiv  13649  faclbnd4lem1  13654  faclbnd6  13660  bcnp1n  13675  bcm1k  13676  bcp1nk  13678  bcn2  13680  bcp1m1  13681  bcpasc  13682  hashgadd  13739  hashfz  13789  hashfzo  13791  hashxplem  13795  hashbclem  13811  hashf1  13816  seqcoll  13823  swrds1  14028  swrdlsw  14029  wrdind  14084  wrd2ind  14085  swrds2  14302  relexpaddg  14412  rei  14515  imi  14516  recan  14696  iserex  15013  isercoll2  15025  serf0  15037  iseraltlem2  15039  iseraltlem3  15040  iseralt  15041  sumrblem  15068  fsumm1  15106  fsump1  15111  telfsumo  15157  fsumparts  15161  hashiun  15177  binomlem  15184  binom  15185  binom1p  15186  binom11  15187  binom1dif  15188  bcxmas  15190  isumsplit  15195  isum1p  15196  climcndslem1  15204  supcvg  15211  harmonic  15214  arisum  15215  arisum2  15216  trireciplem  15217  geoserg  15221  geolim  15226  geolim2  15227  georeclim  15228  geo2sum  15229  geo2sum2  15230  geoisum1c  15236  0.999...  15237  geoihalfsum  15238  cvgrat  15239  mertenslem1  15240  mertenslem2  15241  mertens  15242  prodf1  15247  prodfclim1  15249  prodrblem  15283  fprodcvg  15284  prodmolem2a  15288  zprod  15291  fprodntriv  15296  prodss  15301  fprodss  15302  fprodsplit  15320  fprodn0f  15345  risefaccl  15369  fallfaccl  15370  risefacfac  15389  binomfallfac  15395  bpolycl  15406  bpolysum  15407  bpolydiflem  15408  fsumkthpow  15410  bpoly2  15411  bpoly3  15412  bpoly4  15413  fsumcube  15414  esum  15434  ege2le3  15443  efsub  15453  efexp  15454  efzval  15455  eftlub  15462  effsumlt  15464  ef4p  15466  tanval3  15487  efi4p  15490  tan0  15504  efival  15505  tanadd  15520  cos2t  15531  cos2tsin  15532  ef01bndlem  15537  cos1bnd  15540  cos2bnd  15541  demoivreALT  15554  eirrlem  15557  rpnnen2lem3  15569  rpnnen2lem11  15577  ruclem12  15594  3dvds  15680  3dvdsdec  15681  3dvds2dec  15682  odd2np1lem  15689  odd2np1  15690  opoe  15712  omoe  15713  opeo  15714  omeo  15715  n2dvdsm1  15719  m1exp1  15727  flodddiv4  15764  bitsfzo  15784  gcdmultipleOLD  15900  sqgcd  15909  nn0seqcvgd  15914  prmind2  16029  hashdvds  16112  phiprmpw  16113  phiprm  16114  eulerthlem2  16119  iserodd  16172  sumhash  16232  fldivp1  16233  prmpwdvds  16240  pockthlem  16241  pockthi  16243  prmreclem4  16255  prmreclem6  16257  4sqlem11  16291  4sqlem19  16299  vdwapun  16310  vdwapid1  16311  vdwlem3  16319  vdwlem5  16321  vdwlem6  16322  vdwlem8  16324  vdwlem9  16325  vdwnnlem2  16332  ramub1lem1  16362  ramub1lem2  16363  ramcl  16365  prmo1  16373  dec5nprm  16402  decexp2  16411  prmlem0  16439  43prm  16455  83prm  16456  139prm  16457  163prm  16458  317prm  16459  631prm  16460  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  1259prm  16469  2503lem1  16470  2503lem2  16471  2503lem3  16472  2503prm  16473  4001lem1  16474  4001lem2  16475  4001lem3  16476  4001lem4  16477  4001prm  16478  gsumsgrpccat  18004  gsumccatOLD  18005  mulgnndir  18256  mulgneg2  18261  m1expaddsub  18626  sylow1lem1  18723  sylow2a  18744  efgsval2  18859  efgsrel  18860  efgsres  18864  cnfld1  20570  zsssubrg  20603  cnmgpid  20607  zringcyg  20638  mulgrhm2  20646  cnmsgnsubg  20721  cnmsgnbas  20722  cnmsgngrp  20723  psgninv  20726  evpmodpmf1o  20740  blcvx  23406  iihalf2  23537  icopnfcnv  23546  iccpnfhmeo  23549  xrhmeo  23550  icccvx  23554  lebnumii  23570  reparphti  23601  pcoass  23628  pcorevlem  23630  pcorev2  23632  pi1xfrcnv  23661  cnstrcvs  23745  cncvs  23749  ncvsm1  23758  pjthlem1  24040  divcncf  24048  ovolunlem1a  24097  ovolunlem1  24098  ovolicc2lem4  24121  uniioombllem3  24186  uniioombllem4  24187  dyadovol  24194  vitalilem4  24212  mbf0  24235  iblcnlem1  24388  itgcnlem  24390  dvid  24515  dvexp  24550  dvexp2  24551  dvexp3  24575  dveflem  24576  dvlipcn  24591  dvcvx  24617  dvfsumle  24618  dvfsumlem1  24623  degltp1le  24667  ply1divex  24730  fta1glem1  24759  plyaddlem1  24803  plymullem1  24804  coeidp  24853  dgrid  24854  dvply1  24873  dvply2g  24874  plyremlem  24893  fta1lem  24896  vieta1lem1  24899  vieta1lem2  24900  qaa  24912  iaa  24914  aalioulem3  24923  geolim3  24928  aaliou3lem2  24932  aaliou3lem7  24938  taylply2  24956  dvradcnv  25009  pserdvlem2  25016  pserdv2  25018  abelthlem1  25019  abelthlem2  25020  abelthlem6  25024  abelthlem7  25026  abelth  25029  reeff1olem  25034  reeff1o  25035  efcvx  25037  sinhalfpilem  25049  eulerid  25060  cos2pi  25062  sincosq3sgn  25086  sincosq4sgn  25087  tangtx  25091  sincos4thpi  25099  sincos6thpi  25101  pigt3  25103  pige3ALT  25105  abssinper  25106  coskpi  25108  coseq1  25110  efeq1  25113  tanregt0  25123  logneg2  25198  logdivlti  25203  logcnlem4  25228  dvlog2lem  25235  dvlog2  25236  advlog  25237  advlogexp  25238  logtayl  25243  logtayl2  25245  logccv  25246  cxpval  25247  1cxp  25255  cxpcl  25257  cxpp1  25263  cxpsqrt  25286  dvsqrt  25323  dvcnsqrt  25325  sqrtcn  25331  cxpaddlelem  25332  root1id  25335  root1cj  25337  logrec  25341  logb1  25347  logbmpt  25366  ang180lem1  25387  ang180lem2  25388  ang180lem3  25389  isosctrlem1  25396  isosctrlem2  25397  1cubrlem  25419  1cubr  25420  mcubic  25425  binom4  25428  dquartlem1  25429  quartlem1  25435  asinlem  25446  asinlem2  25447  asinlem3a  25448  asinlem3  25449  asinf  25450  atandm2  25455  atandm4  25457  atanf  25458  asinneg  25464  efiasin  25466  sinasin  25467  asinsin  25470  asin1  25472  acos1  25473  reasinsin  25474  asinbnd  25477  cosasin  25482  atanneg  25485  atancj  25488  efiatan  25490  atanlogaddlem  25491  atanlogadd  25492  atanlogsublem  25493  atanlogsub  25494  efiatan2  25495  2efiatan  25496  tanatan  25497  cosatan  25499  cosatanne0  25500  atantan  25501  atanbndlem  25503  bndatandm  25507  atans2  25509  dvatan  25513  atantayl  25515  atantayl2  25516  atantayl3  25517  leibpilem2  25519  leibpi  25520  log2cnv  25522  log2tlbnd  25523  log2ublem3  25526  log2ub  25527  birthdaylem2  25530  birthday  25532  efrlim  25547  dfef2  25548  cvxcl  25562  scvxcvx  25563  emcllem2  25574  emcllem4  25576  emcllem7  25579  harmonicbnd4  25588  fsumharmonic  25589  zetacvg  25592  lgamcvg2  25632  lgam1  25641  gam1  25642  wilthlem1  25645  wilthlem2  25646  wilthlem3  25647  basellem2  25659  basellem5  25662  basellem6  25663  basellem7  25664  basellem8  25665  basellem9  25666  0sgm  25721  mule1  25725  ppiprm  25728  ppinprm  25729  chtprm  25730  chtnprm  25731  chpp1  25732  mumullem2  25757  1sgmprm  25775  1sgm2ppw  25776  ppiub  25780  chtublem  25787  chtub  25788  logfaclbnd  25798  logfacbnd3  25799  logfacrlim  25800  logexprlim  25801  mersenne  25803  perfect1  25804  perfectlem1  25805  perfectlem2  25806  perfect  25807  dchrelbasd  25815  dchrmulid2  25828  dchrfi  25831  dchrsum2  25844  sumdchr2  25846  bcp1ctr  25855  bposlem8  25867  zabsle1  25872  lgslem1  25873  lgslem2  25874  lgsfcl2  25879  lgsvalmod  25892  lgsneg  25897  lgsdilem  25900  lgsdir2lem1  25901  lgsdir2lem2  25902  lgsdir2lem3  25903  lgsdir2lem5  25905  lgsdir2  25906  lgsdir  25908  lgsdi  25910  lgsne0  25911  lgseisenlem1  25951  lgseisenlem2  25952  lgseisen  25955  lgsquadlem1  25956  lgsquadlem2  25957  lgsquad2lem1  25960  lgsquad2  25962  m1lgs  25964  2lgslem3c  25974  2lgsoddprmlem3c  25988  2lgsoddprmlem3d  25989  2sqlem10  26004  2sqlem11  26005  2sqblem  26007  addsqn2reu  26017  addsqrexnreu  26018  addsqnreup  26019  chtppilimlem2  26050  chebbnd2  26053  chto1lb  26054  rplogsumlem1  26060  rpvmasumlem  26063  dchrmusumlema  26069  dchrmusum2  26070  dchrisum0flblem1  26084  rpvmasum2  26088  mudivsum  26106  mulogsum  26108  vmalogdivsum2  26114  selberg2lem  26126  logdivbnd  26132  pntrmax  26140  pntrsumo1  26141  pntrsumbnd2  26143  pntrlog2bndlem5  26157  pntpbnd1a  26161  pntpbnd2  26163  pntibndlem2  26167  pntlemd  26170  pntlemc  26171  pntlemr  26178  brbtwn2  26691  colinearalglem4  26695  ax5seglem1  26714  ax5seglem2  26715  ax5seglem3  26717  ax5seglem5  26719  ax5seglem7  26721  ax5seglem9  26723  axbtwnid  26725  axpaschlem  26726  axlowdimlem13  26740  axlowdimlem14  26741  axlowdimlem16  26743  axeuclidlem  26748  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  axcontlem8  26757  crctcshwlkn0lem6  27593  clwwlkf1  27828  clwwlknonex2lem2  27887  ex-fl  28226  ex-ind-dvds  28240  vc2OLD  28345  vc0  28351  vcm  28353  nvm1  28442  nvmtri  28448  nvge0  28450  ipval2lem3  28482  ipidsq  28487  lnoadd  28535  ip1ilem  28603  ip1i  28604  ip2i  28605  ipdirilem  28606  ipasslem1  28608  ipasslem2  28609  ipasslem10  28616  minvecolem2  28652  hvsubid  28803  hv2times  28838  hisubcomi  28881  normlem9  28895  normlem7tALT  28896  norm-ii-i  28914  normsubi  28918  hhssnv  29041  pjhthlem1  29168  h1de2bi  29331  homulid2  29577  ho2times  29596  lnop0  29743  lnopaddi  29748  lnophmlem2  29794  lnfn0i  29819  lnfnaddi  29820  hst1h  30004  sto2i  30014  stadd3i  30025  addltmulALT  30223  dpmul4  30590  psgnid  30739  cnmsgn0g  30788  altgnsg  30791  isarchi3  30816  archirngz  30818  ccfldextdgrr  31057  lmatfvlem  31080  qqhval2lem  31222  dya2ub  31528  omssubadd  31558  eulerpartlemgs2  31638  fib5  31663  fib6  31664  ballotlem2  31746  sgnneg  31798  signswch  31831  signlem0  31857  itgexpif  31877  reprlt  31890  breprexp  31904  breprexpnat  31905  hgt750lem2  31923  subfacp1lem5  32431  subfacp1lem6  32432  subfacval2  32434  subfaclim  32435  subfacval3  32436  cvxsconn  32490  resconn  32493  cvmliftlem7  32538  cvmliftlem10  32541  problem4  32911  sinccvglem  32915  sqdivzi  32959  faclimlem1  32975  dnibndlem5  33821  dnibndlem10  33826  ltflcei  34895  sin2h  34897  cos2h  34898  tan2h  34899  poimirlem13  34920  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem31  34938  mblfinlem2  34945  mblfinlem3  34946  dvtan  34957  itg2addnclem3  34960  dvasin  34993  dvacos  34994  areacirc  35002  fdc  35035  mettrifi  35047  heiborlem4  35107  heiborlem6  35109  60gcd7e1  39126  fac2xp3  39143  facp2  39144  2xp3dxp2ge1d  39146  factwoffsmonot  39147  sn-1ne2  39207  sqdeccom12  39224  235t711  39226  expgcd  39232  re1m1e0m0  39276  fltnltalem  39323  3cubeslem3l  39332  3cubeslem3r  39333  eldioph2lem1  39406  lzenom  39416  irrapxlem1  39468  rmspecsqrtnq  39552  rmxm1  39580  rmym1  39581  2nn0ind  39591  jm2.24nn  39605  jm2.17a  39606  jm2.17b  39607  jm2.17c  39608  jm2.24  39609  acongeq  39629  jm2.18  39634  jm2.27c  39653  jm3.1lem2  39664  rngunsnply  39822  flcidc  39823  inductionexd  40554  unitadd  40597  hashnzfzclim  40703  ofdivrec  40707  lhe4.4ex1a  40710  expgrowth  40716  dvradcnv2  40728  binomcxplemrat  40731  binomcxplemnotnn0  40737  isosctrlem1ALT  41317  monoord2xrv  41809  dvsinax  42246  dvnprodlem3  42282  itgsin0pilem1  42284  itgsbtaddcnst  42316  stoweidlem13  42347  stoweidlem26  42360  stoweidlem34  42368  stoweidlem38  42372  wallispilem2  42400  wallispilem4  42402  wallispi2lem1  42405  stirlinglem1  42408  stirlinglem5  42412  stirlinglem10  42417  dirkerper  42430  dirkertrigeqlem1  42432  dirkertrigeqlem3  42434  dirkertrigeq  42435  dirkercncflem4  42440  fourierdlem24  42465  sqwvfoura  42562  sqwvfourb  42563  fourierswlem  42564  1t10e1p1e11  43559  fmtnorec3  43759  fmtno5lem4  43767  fmtno5  43768  257prm  43772  fmtno4nprmfac193  43785  m3prm  43803  139prmALT  43808  127prm  43812  m7prm  43813  lighneallem3  43821  proththd  43828  3exp4mod41  43830  41prothprmlem2  43832  perfectALTVlem2  43936  perfectALTV  43937  11t31e341  43946  evengpop3  44012  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  bgoldbtbndlem1  44019  0nodd  44126  altgsumbcALT  44450  exple2lt6  44461  nn0sumshdiglemB  44729  line2ylem  44787  onetansqsecsq  44909  cotsqcscsq  44910  5m4e1  44947