Axiom ax-1cn 10584

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

This axiom is referenced by:  0cn  10622  1cnd  10625  1ex  10626  mulid1  10628  mulid2  10629  1re  10630  0re  10632  muladd11  10799  peano2cn  10801  mul02lem2  10806  addid1  10809  cnegex2  10811  peano2cnm  10941  0reALT  10972  ine0  11064  mulm1  11070  0lt1  11151  ixi  11258  muleqadd  11273  reccl  11294  recne0  11300  recid  11301  recid2  11302  div1  11318  1div1e1  11319  diveq1  11320  recdiv  11335  divdiv1  11340  divdiv2  11341  recdiv2  11342  conjmul  11346  eqneg  11349  div2neg  11352  recp1lt1  11527  recreclt  11528  recgt0ii  11535  inelr  11615  ofnegsub  11623  peano5nni  11628  nnsscn  11630  nn1m1nn  11646  nn1suc  11647  nnaddcl  11648  nnmulcl  11649  nnne0  11659  nnsub  11669  1m1e0  11697  2cn  11700  3cn  11706  4cn  11710  5cn  11713  6cn  11716  7cn  11719  8cn  11722  9cn  11725  neg1cn  11739  neg1ne0  11741  negneg1e1  11743  1pneg1e0  11744  1m0e1  11746  0p1e1  11747  1p0e1  11749  2m1e1  11751  3m1e2  11753  4m1e3  11754  5m1e4  11755  6m1e5  11756  7m1e6  11757  8m1e7  11758  9m1e8  11759  2p2e4  11760  1p2e3  11768  1p2e3ALT  11769  3p2e5  11776  3p3e6  11777  4p2e6  11778  4p3e7  11779  4p4e8  11780  5p2e7  11781  5p3e8  11782  5p4e9  11783  6p2e8  11784  6p3e9  11785  7p2e9  11786  1t1e1  11787  3t3e9  11792  neg1mulneg1e1  11838  1mhlfehlf  11844  8th4div3  11845  halfpm6th  11846  addltmul  11861  elnn0nn  11927  elz2  11987  zlem1lt  12022  zltlem1  12023  nnaddm1cl  12027  zextlt  12044  zeo  12056  peano5uzi  12059  numsuc  12100  numltc  12112  numsucc  12126  numaddc  12134  6p5lem  12156  5p5e10  12157  6p4e10  12158  7p3e10  12161  8p2e10  12166  10m1e9  12182  4t3lem  12183  7t4e28  12197  9t11e99  12216  decbin2  12227  halfthird  12229  5recm6rec  12230  uzp1  12267  peano2uzr  12291  uzaddcl  12292  rebtwnz  12335  qbtwnre  12580  iccf1o  12874  fz01en  12930  fztp  12958  fzsuc2  12960  fztpval  12964  fseq1m1p1  12977  elfzp1b  12979  fz0to4untppr  13005  predfz  13027  fzoss2  13060  fzval3  13101  fzosplitsnm1  13107  fzo1to4tp  13120  fldiv4p1lem1div2  13200  ceim1l  13210  fldiv  13223  uzrdgxfr  13330  fzen2  13332  nn0ennn  13342  seqm1  13383  seqshft2  13392  monoord2  13397  sermono  13398  seqf1olem1  13405  seqf1olem2  13406  seqz  13414  ser1const  13422  expcl  13443  m1expcl2  13447  expclzlem  13449  expm1t  13453  1exp  13454  mulexpz  13465  expadd  13467  expaddz  13469  expmul  13470  expubnd  13537  sqrecii  13542  neg1sqe1  13555  irec  13560  i4  13563  binom21  13576  sq01  13582  crreczi  13585  bernneq  13586  bernneq2  13587  nn0opthlem1  13624  facndiv  13644  faclbnd4lem1  13649  faclbnd6  13655  bcnp1n  13670  bcm1k  13671  bcp1nk  13673  bcn2  13675  bcp1m1  13676  bcpasc  13677  hashgadd  13734  hashfz  13784  hashfzo  13786  hashxplem  13790  hashbclem  13806  hashf1  13811  seqcoll  13818  swrds1  14019  swrdlsw  14020  wrdind  14075  wrd2ind  14076  swrds2  14293  relexpaddg  14404  rei  14507  imi  14508  recan  14688  iserex  15005  isercoll2  15017  serf0  15029  iseraltlem2  15031  iseraltlem3  15032  iseralt  15033  sumrblem  15060  fsumm1  15098  fsump1  15103  telfsumo  15149  fsumparts  15153  hashiun  15169  binomlem  15176  binom  15177  binom1p  15178  binom11  15179  binom1dif  15180  bcxmas  15182  isumsplit  15187  isum1p  15188  climcndslem1  15196  supcvg  15203  harmonic  15206  arisum  15207  arisum2  15208  trireciplem  15209  geoserg  15213  geolim  15218  geolim2  15219  georeclim  15220  geo2sum  15221  geo2sum2  15222  geoisum1c  15228  0.999...  15229  geoihalfsum  15230  cvgrat  15231  mertenslem1  15232  mertenslem2  15233  mertens  15234  prodf1  15239  prodfclim1  15241  prodrblem  15275  fprodcvg  15276  prodmolem2a  15280  zprod  15283  fprodntriv  15288  prodss  15293  fprodss  15294  fprodsplit  15312  fprodn0f  15337  risefaccl  15361  fallfaccl  15362  risefacfac  15381  binomfallfac  15387  bpolycl  15398  bpolysum  15399  bpolydiflem  15400  fsumkthpow  15402  bpoly2  15403  bpoly3  15404  bpoly4  15405  fsumcube  15406  esum  15426  ege2le3  15435  efsub  15445  efexp  15446  efzval  15447  eftlub  15454  effsumlt  15456  ef4p  15458  tanval3  15479  efi4p  15482  tan0  15496  efival  15497  tanadd  15512  cos2t  15523  cos2tsin  15524  ef01bndlem  15529  cos1bnd  15532  cos2bnd  15533  demoivreALT  15546  eirrlem  15549  rpnnen2lem3  15561  rpnnen2lem11  15569  ruclem12  15586  3dvds  15672  3dvdsdec  15673  3dvds2dec  15674  odd2np1lem  15681  odd2np1  15682  opoe  15704  omoe  15705  opeo  15706  omeo  15707  n2dvdsm1  15710  m1exp1  15717  flodddiv4  15754  bitsfzo  15774  gcdmultipleOLD  15890  sqgcd  15899  nn0seqcvgd  15904  prmind2  16019  hashdvds  16102  phiprmpw  16103  phiprm  16104  eulerthlem2  16109  iserodd  16162  sumhash  16222  fldivp1  16223  prmpwdvds  16230  pockthlem  16231  pockthi  16233  prmreclem4  16245  prmreclem6  16247  4sqlem11  16281  4sqlem19  16289  vdwapun  16300  vdwapid1  16301  vdwlem3  16309  vdwlem5  16311  vdwlem6  16312  vdwlem8  16314  vdwlem9  16315  vdwnnlem2  16322  ramub1lem1  16352  ramub1lem2  16353  ramcl  16355  prmo1  16363  dec5nprm  16392  decexp2  16401  prmlem0  16431  43prm  16447  83prm  16448  139prm  16449  163prm  16450  317prm  16451  631prm  16452  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  1259prm  16461  2503lem1  16462  2503lem2  16463  2503lem3  16464  2503prm  16465  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001lem4  16469  4001prm  16470  gsumsgrpccat  17996  gsumccatOLD  17997  mulgnndir  18248  mulgneg2  18253  m1expaddsub  18618  sylow1lem1  18715  sylow2a  18736  efgsval2  18851  efgsrel  18852  efgsres  18856  cnfld1  20116  zsssubrg  20149  cnmgpid  20153  zringcyg  20184  mulgrhm2  20192  cnmsgnsubg  20266  cnmsgnbas  20267  cnmsgngrp  20268  psgninv  20271  evpmodpmf1o  20285  blcvx  23403  iihalf2  23538  icopnfcnv  23547  iccpnfhmeo  23550  xrhmeo  23551  icccvx  23555  lebnumii  23571  reparphti  23602  pcoass  23629  pcorevlem  23631  pcorev2  23633  pi1xfrcnv  23662  cnstrcvs  23746  cncvs  23750  ncvsm1  23759  pjthlem1  24041  divcncf  24051  ovolunlem1a  24100  ovolunlem1  24101  ovolicc2lem4  24124  uniioombllem3  24189  uniioombllem4  24190  dyadovol  24197  vitalilem4  24215  mbf0  24238  iblcnlem1  24391  itgcnlem  24393  dvid  24521  dvexp  24556  dvexp2  24557  dvexp3  24581  dveflem  24582  dvlipcn  24597  dvcvx  24623  dvfsumle  24624  dvfsumlem1  24629  degltp1le  24674  ply1divex  24737  fta1glem1  24766  plyaddlem1  24810  plymullem1  24811  coeidp  24860  dgrid  24861  dvply1  24880  dvply2g  24881  plyremlem  24900  fta1lem  24903  vieta1lem1  24906  vieta1lem2  24907  qaa  24919  iaa  24921  aalioulem3  24930  geolim3  24935  aaliou3lem2  24939  aaliou3lem7  24945  taylply2  24963  dvradcnv  25016  pserdvlem2  25023  pserdv2  25025  abelthlem1  25026  abelthlem2  25027  abelthlem6  25031  abelthlem7  25033  abelth  25036  reeff1olem  25041  reeff1o  25042  efcvx  25044  sinhalfpilem  25056  eulerid  25067  cos2pi  25069  sincosq3sgn  25093  sincosq4sgn  25094  tangtx  25098  sincos4thpi  25106  sincos6thpi  25108  pigt3  25110  pige3ALT  25112  abssinper  25113  coskpi  25115  coseq1  25117  efeq1  25120  tanregt0  25131  logneg2  25206  logdivlti  25211  logcnlem4  25236  dvlog2lem  25243  dvlog2  25244  advlog  25245  advlogexp  25246  logtayl  25251  logtayl2  25253  logccv  25254  cxpval  25255  1cxp  25263  cxpcl  25265  cxpp1  25271  cxpsqrt  25294  dvsqrt  25331  dvcnsqrt  25333  sqrtcn  25339  cxpaddlelem  25340  root1id  25343  root1cj  25345  logrec  25349  logb1  25355  logbmpt  25374  ang180lem1  25395  ang180lem2  25396  ang180lem3  25397  isosctrlem1  25404  isosctrlem2  25405  1cubrlem  25427  1cubr  25428  mcubic  25433  binom4  25436  dquartlem1  25437  quartlem1  25443  asinlem  25454  asinlem2  25455  asinlem3a  25456  asinlem3  25457  asinf  25458  atandm2  25463  atandm4  25465  atanf  25466  asinneg  25472  efiasin  25474  sinasin  25475  asinsin  25478  asin1  25480  acos1  25481  reasinsin  25482  asinbnd  25485  cosasin  25490  atanneg  25493  atancj  25496  efiatan  25498  atanlogaddlem  25499  atanlogadd  25500  atanlogsublem  25501  atanlogsub  25502  efiatan2  25503  2efiatan  25504  tanatan  25505  cosatan  25507  cosatanne0  25508  atantan  25509  atanbndlem  25511  bndatandm  25515  atans2  25517  dvatan  25521  atantayl  25523  atantayl2  25524  atantayl3  25525  leibpilem2  25527  leibpi  25528  log2cnv  25530  log2tlbnd  25531  log2ublem3  25534  log2ub  25535  birthdaylem2  25538  birthday  25540  efrlim  25555  dfef2  25556  cvxcl  25570  scvxcvx  25571  emcllem2  25582  emcllem4  25584  emcllem7  25587  harmonicbnd4  25596  fsumharmonic  25597  zetacvg  25600  lgamcvg2  25640  lgam1  25649  gam1  25650  wilthlem1  25653  wilthlem2  25654  wilthlem3  25655  basellem2  25667  basellem5  25670  basellem6  25671  basellem7  25672  basellem8  25673  basellem9  25674  0sgm  25729  mule1  25733  ppiprm  25736  ppinprm  25737  chtprm  25738  chtnprm  25739  chpp1  25740  mumullem2  25765  1sgmprm  25783  1sgm2ppw  25784  ppiub  25788  chtublem  25795  chtub  25796  logfaclbnd  25806  logfacbnd3  25807  logfacrlim  25808  logexprlim  25809  mersenne  25811  perfect1  25812  perfectlem1  25813  perfectlem2  25814  perfect  25815  dchrelbasd  25823  dchrmulid2  25836  dchrfi  25839  dchrsum2  25852  sumdchr2  25854  bcp1ctr  25863  bposlem8  25875  zabsle1  25880  lgslem1  25881  lgslem2  25882  lgsfcl2  25887  lgsvalmod  25900  lgsneg  25905  lgsdilem  25908  lgsdir2lem1  25909  lgsdir2lem2  25910  lgsdir2lem3  25911  lgsdir2lem5  25913  lgsdir2  25914  lgsdir  25916  lgsdi  25918  lgsne0  25919  lgseisenlem1  25959  lgseisenlem2  25960  lgseisen  25963  lgsquadlem1  25964  lgsquadlem2  25965  lgsquad2lem1  25968  lgsquad2  25970  m1lgs  25972  2lgslem3c  25982  2lgsoddprmlem3c  25996  2lgsoddprmlem3d  25997  2sqlem10  26012  2sqlem11  26013  2sqblem  26015  addsqn2reu  26025  addsqrexnreu  26026  addsqnreup  26027  chtppilimlem2  26058  chebbnd2  26061  chto1lb  26062  rplogsumlem1  26068  rpvmasumlem  26071  dchrmusumlema  26077  dchrmusum2  26078  dchrisum0flblem1  26092  rpvmasum2  26096  mudivsum  26114  mulogsum  26116  vmalogdivsum2  26122  selberg2lem  26134  logdivbnd  26140  pntrmax  26148  pntrsumo1  26149  pntrsumbnd2  26151  pntrlog2bndlem5  26165  pntpbnd1a  26169  pntpbnd2  26171  pntibndlem2  26175  pntlemd  26178  pntlemc  26179  pntlemr  26186  brbtwn2  26699  colinearalglem4  26703  ax5seglem1  26722  ax5seglem2  26723  ax5seglem3  26725  ax5seglem5  26727  ax5seglem7  26729  ax5seglem9  26731  axbtwnid  26733  axpaschlem  26734  axlowdimlem13  26748  axlowdimlem14  26749  axlowdimlem16  26751  axeuclidlem  26756  axcontlem2  26759  axcontlem4  26761  axcontlem7  26764  axcontlem8  26765  crctcshwlkn0lem6  27601  clwwlkf1  27834  clwwlknonex2lem2  27893  ex-fl  28232  ex-ind-dvds  28246  vc2OLD  28351  vc0  28357  vcm  28359  nvm1  28448  nvmtri  28454  nvge0  28456  ipval2lem3  28488  ipidsq  28493  lnoadd  28541  ip1ilem  28609  ip1i  28610  ip2i  28611  ipdirilem  28612  ipasslem1  28614  ipasslem2  28615  ipasslem10  28622  minvecolem2  28658  hvsubid  28809  hv2times  28844  hisubcomi  28887  normlem9  28901  normlem7tALT  28902  norm-ii-i  28920  normsubi  28924  hhssnv  29047  pjhthlem1  29174  h1de2bi  29337  homulid2  29583  ho2times  29602  lnop0  29749  lnopaddi  29754  lnophmlem2  29800  lnfn0i  29825  lnfnaddi  29826  hst1h  30010  sto2i  30020  stadd3i  30031  addltmulALT  30229  dpmul4  30616  psgnid  30789  cnmsgn0g  30838  altgnsg  30841  isarchi3  30866  archirngz  30868  ccfldextdgrr  31145  lmatfvlem  31168  qqhval2lem  31332  dya2ub  31638  omssubadd  31668  eulerpartlemgs2  31748  fib5  31773  fib6  31774  ballotlem2  31856  sgnneg  31908  signswch  31941  signlem0  31967  itgexpif  31987  reprlt  32000  breprexp  32014  breprexpnat  32015  hgt750lem2  32033  subfacp1lem5  32544  subfacp1lem6  32545  subfacval2  32547  subfaclim  32548  subfacval3  32549  cvxsconn  32603  resconn  32606  cvmliftlem7  32651  cvmliftlem10  32654  problem4  33024  sinccvglem  33028  sqdivzi  33072  faclimlem1  33088  dnibndlem5  33934  dnibndlem10  33939  ltflcei  35045  sin2h  35047  cos2h  35048  tan2h  35049  poimirlem13  35070  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem31  35088  mblfinlem2  35095  mblfinlem3  35096  dvtan  35107  itg2addnclem3  35110  dvasin  35141  dvacos  35142  areacirc  35150  fdc  35183  mettrifi  35195  heiborlem4  35252  heiborlem6  35254  60gcd7e1  39293  lcmineqlem1  39317  lcmineqlem8  39324  lcmineqlem9  39325  lcmineqlem10  39326  lcmineqlem12  39328  3lexlogpow5ineq1  39341  facp2  39347  fac2xp3  39385  2xp3dxp2ge1d  39387  factwoffsmonot  39388  sn-1ne2  39466  sqdeccom12  39483  235t711  39485  expgcd  39491  re1m1e0m0  39535  ipiiie0  39574  sn-0tie0  39576  fltnltalem  39618  3cubeslem3l  39627  3cubeslem3r  39628  eldioph2lem1  39701  lzenom  39711  irrapxlem1  39763  rmspecsqrtnq  39847  rmxm1  39875  rmym1  39876  2nn0ind  39886  jm2.24nn  39900  jm2.17a  39901  jm2.17b  39902  jm2.17c  39903  jm2.24  39904  acongeq  39924  jm2.18  39929  jm2.27c  39948  jm3.1lem2  39959  rngunsnply  40117  flcidc  40118  inductionexd  40858  unitadd  40901  hashnzfzclim  41026  ofdivrec  41030  lhe4.4ex1a  41033  expgrowth  41039  dvradcnv2  41051  binomcxplemrat  41054  binomcxplemnotnn0  41060  isosctrlem1ALT  41640  monoord2xrv  42123  dvsinax  42555  dvnprodlem3  42590  itgsin0pilem1  42592  itgsbtaddcnst  42624  stoweidlem13  42655  stoweidlem26  42668  stoweidlem34  42676  stoweidlem38  42680  wallispilem2  42708  wallispilem4  42710  wallispi2lem1  42713  stirlinglem1  42716  stirlinglem5  42720  stirlinglem10  42725  dirkerper  42738  dirkertrigeqlem1  42740  dirkertrigeqlem3  42742  dirkertrigeq  42743  dirkercncflem4  42748  fourierdlem24  42773  sqwvfoura  42870  sqwvfourb  42871  fourierswlem  42872  1t10e1p1e11  43867  fmtnorec3  44065  fmtno5lem4  44073  fmtno5  44074  257prm  44078  fmtno4nprmfac193  44091  m3prm  44109  139prmALT  44113  127prm  44116  m7prm  44117  lighneallem3  44125  proththd  44132  3exp4mod41  44134  41prothprmlem2  44136  perfectALTVlem2  44240  perfectALTV  44241  11t31e341  44250  evengpop3  44316  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbtbndlem1  44323  0nodd  44430  altgsumbcALT  44755  exple2lt6  44766  nn0sumshdiglemB  45034  ackval3  45097  ackval3012  45106  line2ylem  45165  onetansqsecsq  45287  cotsqcscsq  45288  5m4e1  45325