Axiom ax-1cn 11061

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

This axiom is referenced by:  0cn  11101  1cnd  11104  1ex  11105  mulrid  11107  mullid  11108  1re  11109  0re  11111  muladd11  11280  peano2cn  11282  mul02lem2  11287  addrid  11290  cnegex2  11292  peano2cnm  11424  0reALT  11455  ine0  11549  mulm1  11555  0lt1  11636  ixi  11743  muleqadd  11758  reccl  11780  recne0  11786  recid  11787  recid2  11788  diveq1  11803  div1  11808  1div1e1  11809  recdiv  11824  divdiv1  11829  divdiv2  11830  recdiv2  11831  conjmul  11835  eqneg  11838  div2neg  11841  recp1lt1  12017  recreclt  12018  recgt0ii  12025  neg1cn  12107  neg1ne0  12109  negneg1e1  12111  ofnegsub  12120  peano5nni  12125  nnsscn  12127  nn1m1nn  12143  nn1suc  12144  nnaddcl  12145  nnmulcl  12146  nnne0  12156  nnsub  12166  1m1e0  12194  2cn  12197  3cn  12203  4cn  12207  5cn  12210  6cn  12213  7cn  12216  8cn  12219  9cn  12222  1pneg1e0  12236  1m0e1  12238  0p1e1  12239  1p0e1  12241  2m1e1  12243  3m1e2  12245  4m1e3  12246  5m1e4  12247  6m1e5  12248  7m1e6  12249  8m1e7  12250  9m1e8  12251  2p2e4  12252  1p2e3  12260  1p2e3ALT  12261  3p2e5  12268  3p3e6  12269  4p2e6  12270  4p3e7  12271  4p4e8  12272  5p2e7  12273  5p3e8  12274  5p4e9  12275  6p2e8  12276  6p3e9  12277  7p2e9  12278  1t1e1  12279  3t3e9  12284  neg1mulneg1e1  12330  1mhlfehlf  12337  8th4div3  12338  halfthird  12339  halfpm6th  12340  addltmul  12354  elnn0nn  12420  elz2  12483  zlem1lt  12521  zltlem1  12522  nnaddm1cl  12527  zextlt  12544  zeo  12556  peano5uzi  12559  numsuc  12599  numltc  12611  numsucc  12625  numaddc  12633  6p5lem  12655  5p5e10  12656  6p4e10  12657  7p3e10  12660  8p2e10  12665  10m1e9  12681  4t3lem  12682  7t4e28  12696  9t11e99  12715  decbin2  12726  5recm6rec  12728  uzp1  12770  peano2uzr  12798  uzaddcl  12799  rebtwnz  12842  qbtwnre  13095  iccf1o  13393  fz01en  13449  fztp  13477  fzsuc2  13479  fztpval  13483  fseq1m1p1  13496  elfzp1b  13498  predfz  13550  fzoss2  13584  fzval3  13631  fzosplitsnm1  13637  fzo1to4tp  13651  fldiv4p1lem1div2  13736  ceim1l  13748  fldiv  13761  uzrdgxfr  13871  fzen2  13873  nn0ennn  13883  seqm1  13923  seqshft2  13932  monoord2  13937  sermono  13938  seqf1olem1  13945  seqf1olem2  13946  seqz  13954  ser1const  13962  expcl  13983  expclzlem  13987  m1expcl2  13989  expm1t  13994  1exp  13995  mulexpz  14006  expadd  14008  expaddz  14010  expmul  14011  expubnd  14082  sqrecii  14087  neg1sqe1  14100  irec  14105  i4  14108  binom21  14123  sq01  14129  crreczi  14132  bernneq  14133  bernneq2  14134  nn0opthlem1  14172  facndiv  14192  faclbnd4lem1  14197  faclbnd6  14203  bcnp1n  14218  bcm1k  14219  bcp1nk  14221  bcn2  14223  bcp1m1  14224  bcpasc  14225  hashgadd  14281  hashfz  14331  hashfzo  14333  hashxplem  14337  hashbclem  14356  hashf1  14361  seqcoll  14368  swrds1  14571  swrdlsw  14572  wrdind  14626  wrd2ind  14627  swrds2  14844  relexpaddg  14957  rei  15060  imi  15061  recan  15241  iserex  15561  isercoll2  15573  serf0  15585  iseraltlem2  15587  iseraltlem3  15588  iseralt  15589  sumrblem  15615  fsumm1  15655  telfsumo  15706  fsumparts  15710  hashiun  15726  binomlem  15733  binom  15734  binom1p  15735  binom11  15736  binom1dif  15737  bcxmas  15739  isumsplit  15744  isum1p  15745  climcndslem1  15753  supcvg  15760  harmonic  15763  arisum  15764  arisum2  15765  trireciplem  15766  geoserg  15770  geolim  15774  geolim2  15775  georeclim  15776  geo2sum  15777  geo2sum2  15778  geoisum1c  15784  0.999...  15785  geoihalfsum  15786  cvgrat  15787  mertenslem1  15788  mertenslem2  15789  mertens  15790  prodf1  15795  prodfclim1  15797  prodrblem  15833  fprodcvg  15834  prodmolem2a  15838  zprod  15841  fprodntriv  15846  prodss  15851  fprodss  15852  fprodsplit  15870  fprodn0f  15895  risefaccl  15919  fallfaccl  15920  risefacfac  15939  binomfallfac  15945  bpolycl  15956  bpolysum  15957  bpolydiflem  15958  fsumkthpow  15960  bpoly2  15961  bpoly3  15962  bpoly4  15963  fsumcube  15964  esum  15984  ege2le3  15994  efsub  16006  efexp  16007  efzval  16008  eftlub  16015  effsumlt  16017  ef4p  16019  tanval3  16040  efi4p  16043  tan0  16057  efival  16058  tanadd  16073  cos2t  16084  cos2tsin  16085  ef01bndlem  16090  cos1bnd  16093  cos2bnd  16094  demoivreALT  16107  eirrlem  16110  rpnnen2lem3  16122  rpnnen2lem11  16130  ruclem12  16147  3dvds  16239  3dvdsdec  16240  3dvds2dec  16241  odd2np1lem  16248  odd2np1  16249  opoe  16271  omoe  16272  opeo  16273  omeo  16274  n2dvdsm1  16277  m1exp1  16284  flodddiv4  16323  bitsfzo  16343  sqgcd  16470  expgcd  16471  nn0seqcvgd  16478  prmind2  16593  hashdvds  16683  phiprmpw  16684  phiprm  16685  eulerthlem2  16690  iserodd  16744  sumhash  16805  fldivp1  16806  prmpwdvds  16813  pockthlem  16814  pockthi  16816  prmreclem4  16828  prmreclem6  16830  4sqlem11  16864  4sqlem19  16872  vdwapun  16883  vdwapid1  16884  vdwlem3  16892  vdwlem5  16894  vdwlem6  16895  vdwlem8  16897  vdwlem9  16898  vdwnnlem2  16905  ramub1lem1  16935  ramub1lem2  16936  ramcl  16938  prmo1  16946  dec5nprm  16975  prmlem0  17014  43prm  17030  83prm  17031  139prm  17032  163prm  17033  317prm  17034  631prm  17035  1259lem2  17040  1259lem3  17041  1259lem4  17042  1259lem5  17043  1259prm  17044  2503lem1  17045  2503lem2  17046  2503lem3  17047  2503prm  17048  4001lem1  17049  4001lem2  17050  4001lem3  17051  4001lem4  17052  4001prm  17053  gsumsgrpccat  18745  mulgnndir  19013  mulgneg2  19018  m1expaddsub  19408  sylow1lem1  19508  sylow2a  19529  efgsval2  19643  efgsrel  19644  efgsres  19648  cncrng  21323  cnfld1  21328  cnfld1OLD  21329  zsssubrg  21360  cnmgpid  21364  zringcyg  21404  mulgrhm2  21413  pzriprng1ALT  21431  cnmsgnsubg  21512  cnmsgnbas  21513  cnmsgngrp  21514  psgninv  21517  evpmodpmf1o  21531  psdmplcl  22075  blcvx  24711  iihalf2  24853  icopnfcnv  24865  iccpnfhmeo  24868  xrhmeo  24869  icccvx  24873  lebnumii  24890  reparphti  24921  reparphtiOLD  24922  pcoass  24949  pcorevlem  24951  pcorev2  24953  pi1xfrcnv  24982  cnstrcvs  25066  cncvs  25070  ncvsm1  25079  pjthlem1  25362  divcncf  25373  ovolunlem1a  25422  ovolunlem1  25423  ovolicc2lem4  25446  uniioombllem3  25511  uniioombllem4  25512  dyadovol  25519  vitalilem4  25537  mbf0  25560  iblcnlem1  25714  itgcnlem  25716  dvid  25844  dvexp  25882  dvexp2  25883  dvexp3  25907  dveflem  25908  dvlipcn  25924  dvcvx  25950  dvfsumle  25951  dvfsumleOLD  25952  dvfsumlem1  25957  degltp1le  26003  ply1divex  26067  fta1glem1  26098  plyaddlem1  26143  plymullem1  26144  coeidp  26194  dgrid  26195  dvply1  26216  dvply2g  26217  dvply2gOLD  26218  plyremlem  26237  fta1lem  26240  vieta1lem1  26243  vieta1lem2  26244  qaa  26256  iaa  26258  aalioulem3  26267  geolim3  26272  aaliou3lem2  26276  aaliou3lem7  26282  taylply2  26300  taylply2OLD  26301  dvradcnv  26355  pserdvlem2  26363  pserdv2  26365  abelthlem1  26366  abelthlem2  26367  abelthlem6  26371  abelthlem7  26373  abelth  26376  reeff1olem  26381  reeff1o  26382  efcvx  26384  sinhalfpilem  26397  eulerid  26408  cos2pi  26410  sincosq3sgn  26434  sincosq4sgn  26435  tangtx  26439  sincos4thpi  26447  sincos6thpi  26450  pigt3  26452  pige3ALT  26454  abssinper  26455  coskpi  26457  coseq1  26459  efeq1  26462  tanregt0  26473  logneg2  26549  logdivlti  26554  logcnlem4  26579  dvlog2lem  26586  dvlog2  26587  advlog  26588  advlogexp  26589  logtayl  26594  logtayl2  26596  logccv  26597  cxpval  26598  1cxp  26606  cxpcl  26608  cxpp1  26614  cxpsqrt  26637  dvsqrt  26676  dvcnsqrt  26678  sqrtcn  26685  cxpaddlelem  26686  root1id  26689  root1cj  26691  logrec  26698  logb1  26704  logbmpt  26723  ang180lem1  26744  ang180lem2  26745  ang180lem3  26746  isosctrlem1  26753  isosctrlem2  26754  1cubrlem  26776  1cubr  26777  mcubic  26782  binom4  26785  dquartlem1  26786  quartlem1  26792  asinlem  26803  asinlem2  26804  asinlem3a  26805  asinlem3  26806  asinf  26807  atandm2  26812  atandm4  26814  atanf  26815  asinneg  26821  efiasin  26823  sinasin  26824  asinsin  26827  asin1  26829  acos1  26830  reasinsin  26831  asinbnd  26834  cosasin  26839  atanneg  26842  atancj  26845  efiatan  26847  atanlogaddlem  26848  atanlogadd  26849  atanlogsublem  26850  atanlogsub  26851  efiatan2  26852  2efiatan  26853  tanatan  26854  cosatan  26856  cosatanne0  26857  atantan  26858  atanbndlem  26860  bndatandm  26864  atans2  26866  dvatan  26870  atantayl  26872  atantayl2  26873  atantayl3  26874  leibpilem2  26876  leibpi  26877  log2cnv  26879  log2tlbnd  26880  log2ublem3  26883  log2ub  26884  birthdaylem2  26887  birthday  26889  efrlim  26904  efrlimOLD  26905  dfef2  26906  cvxcl  26920  scvxcvx  26921  emcllem2  26932  emcllem4  26934  emcllem7  26937  harmonicbnd4  26946  fsumharmonic  26947  zetacvg  26950  lgamcvg2  26990  lgam1  26999  gam1  27000  wilthlem1  27003  wilthlem2  27004  wilthlem3  27005  basellem2  27017  basellem5  27020  basellem6  27021  basellem7  27022  basellem8  27023  basellem9  27024  0sgm  27079  mule1  27083  ppiprm  27086  ppinprm  27087  chtprm  27088  chtnprm  27089  chpp1  27090  mumullem2  27115  1sgmprm  27135  1sgm2ppw  27136  ppiub  27140  chtublem  27147  chtub  27148  logfaclbnd  27158  logfacbnd3  27159  logfacrlim  27160  logexprlim  27161  mersenne  27163  perfect1  27164  perfectlem1  27165  perfectlem2  27166  perfect  27167  dchrelbasd  27175  dchrmullid  27188  dchrfi  27191  dchrsum2  27204  sumdchr2  27206  bcp1ctr  27215  bposlem8  27227  zabsle1  27232  lgslem1  27233  lgslem2  27234  lgsfcl2  27239  lgsvalmod  27252  lgsneg  27257  lgsdilem  27260  lgsdir2lem1  27261  lgsdir2lem2  27262  lgsdir2lem3  27263  lgsdir2lem5  27265  lgsdir2  27266  lgsdir  27268  lgsdi  27270  lgsne0  27271  lgseisenlem1  27311  lgseisenlem2  27312  lgseisen  27315  lgsquadlem1  27316  lgsquadlem2  27317  lgsquad2lem1  27320  lgsquad2  27322  m1lgs  27324  2lgslem3c  27334  2lgsoddprmlem3c  27348  2lgsoddprmlem3d  27349  2sqlem10  27364  2sqlem11  27365  2sqblem  27367  addsqn2reu  27377  addsqrexnreu  27378  addsqnreup  27379  chtppilimlem2  27410  chebbnd2  27413  chto1lb  27414  rplogsumlem1  27420  rpvmasumlem  27423  dchrmusumlema  27429  dchrmusum2  27430  dchrisum0flblem1  27444  rpvmasum2  27448  mudivsum  27466  mulogsum  27468  vmalogdivsum2  27474  selberg2lem  27486  logdivbnd  27492  pntrmax  27500  pntrsumo1  27501  pntrsumbnd2  27503  pntrlog2bndlem5  27517  pntpbnd1a  27521  pntpbnd2  27523  pntibndlem2  27527  pntlemd  27530  pntlemc  27531  pntlemr  27538  brbtwn2  28881  colinearalglem4  28885  ax5seglem1  28904  ax5seglem2  28905  ax5seglem3  28907  ax5seglem5  28909  ax5seglem7  28911  ax5seglem9  28913  axbtwnid  28915  axpaschlem  28916  axlowdimlem13  28930  axlowdimlem14  28931  axlowdimlem16  28933  axeuclidlem  28938  axcontlem2  28941  axcontlem4  28943  axcontlem7  28946  axcontlem8  28947  crctcshwlkn0lem6  29791  clwwlkf1  30024  clwwlknonex2lem2  30083  ex-fl  30422  ex-ind-dvds  30436  vc2OLD  30543  vc0  30549  vcm  30551  nvm1  30640  nvmtri  30646  nvge0  30648  ipval2lem3  30680  ipidsq  30685  lnoadd  30733  ip1ilem  30801  ip1i  30802  ip2i  30803  ipdirilem  30804  ipasslem1  30806  ipasslem2  30807  ipasslem10  30814  minvecolem2  30850  hvsubid  31001  hv2times  31036  hisubcomi  31079  normlem9  31093  normlem7tALT  31094  norm-ii-i  31112  normsubi  31116  hhssnv  31239  pjhthlem1  31366  h1de2bi  31529  homullid  31775  ho2times  31794  lnop0  31941  lnopaddi  31946  lnophmlem2  31992  lnfn0i  32017  lnfnaddi  32018  hst1h  32202  sto2i  32212  stadd3i  32223  addltmulALT  32421  sgnneg  32811  dpmul4  32889  psgnid  33061  cnmsgn0g  33110  altgnsg  33113  isarchi3  33151  archirngz  33153  1fldgenq  33283  ply1dg3rt0irred  33541  ccfldextdgrr  33680  constrsscn  33748  constrabscl  33786  cos9thpiminplylem1  33790  cos9thpiminplylem4  33793  cos9thpiminplylem5  33794  lmatfvlem  33823  qqhval2lem  33989  dya2ub  34278  omssubadd  34308  eulerpartlemgs2  34388  fib5  34413  fib6  34414  ballotlem2  34497  signswch  34569  signlem0  34595  itgexpif  34614  reprlt  34627  breprexp  34641  breprexpnat  34642  hgt750lem2  34660  subfacp1lem5  35216  subfacp1lem6  35217  subfacval2  35219  subfaclim  35220  subfacval3  35221  cvxsconn  35275  resconn  35278  cvmliftlem7  35323  cvmliftlem10  35326  problem4  35700  sinccvglem  35704  sqdivzi  35760  faclimlem1  35775  dnibndlem5  36515  dnibndlem10  36520  ltflcei  37647  sin2h  37649  cos2h  37650  tan2h  37651  poimirlem13  37672  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem31  37690  mblfinlem2  37697  mblfinlem3  37698  dvtan  37709  itg2addnclem3  37712  dvasin  37743  dvacos  37744  areacirc  37752  fdc  37784  mettrifi  37796  heiborlem4  37853  heiborlem6  37855  60gcd7e1  42037  lcmineqlem1  42061  lcmineqlem8  42068  lcmineqlem9  42069  lcmineqlem10  42070  lcmineqlem12  42072  3exp7  42085  3lexlogpow5ineq1  42086  3lexlogpow5ineq5  42092  aks4d1p1p4  42103  aks4d1p1p7  42106  aks4d1p1  42108  facp2  42175  1p3e4  42291  sn-1ne2  42297  sqdeccom12  42321  235t711  42337  sin2t3rdpi  42385  cos2t3rdpi  42386  re1m1e0m0  42429  ipiiie0  42470  sn-0tie0  42483  fltnltalem  42694  sum9cubes  42704  3cubeslem3l  42718  3cubeslem3r  42719  eldioph2lem1  42792  lzenom  42802  irrapxlem1  42854  rmspecsqrtnq  42938  rmxm1  42966  rmym1  42967  2nn0ind  42977  jm2.24nn  42991  jm2.17a  42992  jm2.17b  42993  jm2.17c  42994  jm2.24  42995  acongeq  43015  jm2.18  43020  jm2.27c  43039  jm3.1lem2  43050  rngunsnply  43201  flcidc  43202  inductionexd  44187  unitadd  44227  hashnzfzclim  44354  ofdivrec  44358  lhe4.4ex1a  44361  expgrowth  44367  dvradcnv2  44379  binomcxplemrat  44382  binomcxplemnotnn0  44388  isosctrlem1ALT  44965  monoord2xrv  45520  dvsinax  45950  dvnprodlem3  45985  itgsin0pilem1  45987  itgsbtaddcnst  46019  stoweidlem13  46050  stoweidlem26  46063  stoweidlem34  46071  stoweidlem38  46075  wallispilem2  46103  wallispilem4  46105  wallispi2lem1  46108  stirlinglem1  46111  stirlinglem5  46115  stirlinglem10  46120  dirkerper  46133  dirkertrigeqlem1  46135  dirkertrigeqlem3  46137  dirkertrigeq  46138  dirkercncflem4  46143  fourierdlem24  46168  sqwvfoura  46265  sqwvfourb  46266  fourierswlem  46267  lambert0  46917  lamberte  46918  cjnpoly  46919  1t10e1p1e11  47340  ceil5half3  47370  modm2nep1  47396  modm1nep2  47398  modm1nem2  47399  fmtnorec3  47578  fmtno5lem4  47586  fmtno5  47587  257prm  47591  fmtno4nprmfac193  47604  m3prm  47622  139prmALT  47626  127prm  47629  m7prm  47630  lighneallem3  47637  proththd  47644  3exp4mod41  47646  41prothprmlem2  47648  perfectALTVlem2  47752  perfectALTV  47753  11t31e341  47762  evengpop3  47828  nnsum4primeseven  47830  nnsum4primesevenALTV  47831  bgoldbtbndlem1  47835  0nodd  48200  altgsumbcALT  48383  exple2lt6  48394  nn0sumshdiglemB  48651  ackval3  48714  ackval3012  48723  line2ylem  48782  onetansqsecsq  49792  cotsqcscsq  49793  5m4e1  49828