Axiom ax-1cn 11242

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

This axiom is referenced by:  0cn  11282  1cnd  11285  1ex  11286  mulrid  11288  mullid  11289  1re  11290  0re  11292  muladd11  11460  peano2cn  11462  mul02lem2  11467  addrid  11470  cnegex2  11472  peano2cnm  11602  0reALT  11633  ine0  11725  mulm1  11731  0lt1  11812  ixi  11919  muleqadd  11934  reccl  11956  recne0  11962  recid  11963  recid2  11964  diveq1  11979  div1  11984  1div1e1  11985  recdiv  12000  divdiv1  12005  divdiv2  12006  recdiv2  12007  conjmul  12011  eqneg  12014  div2neg  12017  recp1lt1  12193  recreclt  12194  recgt0ii  12201  inelr  12283  ofnegsub  12291  peano5nni  12296  nnsscn  12298  nn1m1nn  12314  nn1suc  12315  nnaddcl  12316  nnmulcl  12317  nnne0  12327  nnsub  12337  1m1e0  12365  2cn  12368  3cn  12374  4cn  12378  5cn  12381  6cn  12384  7cn  12387  8cn  12390  9cn  12393  neg1cn  12407  neg1ne0  12409  negneg1e1  12411  1pneg1e0  12412  1m0e1  12414  0p1e1  12415  1p0e1  12417  2m1e1  12419  3m1e2  12421  4m1e3  12422  5m1e4  12423  6m1e5  12424  7m1e6  12425  8m1e7  12426  9m1e8  12427  2p2e4  12428  1p2e3  12436  1p2e3ALT  12437  3p2e5  12444  3p3e6  12445  4p2e6  12446  4p3e7  12447  4p4e8  12448  5p2e7  12449  5p3e8  12450  5p4e9  12451  6p2e8  12452  6p3e9  12453  7p2e9  12454  1t1e1  12455  3t3e9  12460  neg1mulneg1e1  12506  1mhlfehlf  12512  8th4div3  12513  halfpm6th  12514  addltmul  12529  elnn0nn  12595  elz2  12657  zlem1lt  12695  zltlem1  12696  nnaddm1cl  12700  zextlt  12717  zeo  12729  peano5uzi  12732  numsuc  12772  numltc  12784  numsucc  12798  numaddc  12806  6p5lem  12828  5p5e10  12829  6p4e10  12830  7p3e10  12833  8p2e10  12838  10m1e9  12854  4t3lem  12855  7t4e28  12869  9t11e99  12888  decbin2  12899  halfthird  12901  5recm6rec  12902  uzp1  12944  peano2uzr  12968  uzaddcl  12969  rebtwnz  13012  qbtwnre  13261  iccf1o  13556  fz01en  13612  fztp  13640  fzsuc2  13642  fztpval  13646  fseq1m1p1  13659  elfzp1b  13661  predfz  13710  fzoss2  13744  fzval3  13785  fzosplitsnm1  13791  fzo1to4tp  13804  fldiv4p1lem1div2  13886  ceim1l  13898  fldiv  13911  uzrdgxfr  14018  fzen2  14020  nn0ennn  14030  seqm1  14070  seqshft2  14079  monoord2  14084  sermono  14085  seqf1olem1  14092  seqf1olem2  14093  seqz  14101  ser1const  14109  expcl  14130  expclzlem  14134  m1expcl2  14136  expm1t  14141  1exp  14142  mulexpz  14153  expadd  14155  expaddz  14157  expmul  14158  expubnd  14227  sqrecii  14232  neg1sqe1  14245  irec  14250  i4  14253  binom21  14268  sq01  14274  crreczi  14277  bernneq  14278  bernneq2  14279  nn0opthlem1  14317  facndiv  14337  faclbnd4lem1  14342  faclbnd6  14348  bcnp1n  14363  bcm1k  14364  bcp1nk  14366  bcn2  14368  bcp1m1  14369  bcpasc  14370  hashgadd  14426  hashfz  14476  hashfzo  14478  hashxplem  14482  hashbclem  14501  hashf1  14506  seqcoll  14513  swrds1  14714  swrdlsw  14715  wrdind  14770  wrd2ind  14771  swrds2  14989  relexpaddg  15102  rei  15205  imi  15206  recan  15385  iserex  15705  isercoll2  15717  serf0  15729  iseraltlem2  15731  iseraltlem3  15732  iseralt  15733  sumrblem  15759  fsumm1  15799  telfsumo  15850  fsumparts  15854  hashiun  15870  binomlem  15877  binom  15878  binom1p  15879  binom11  15880  binom1dif  15881  bcxmas  15883  isumsplit  15888  isum1p  15889  climcndslem1  15897  supcvg  15904  harmonic  15907  arisum  15908  arisum2  15909  trireciplem  15910  geoserg  15914  geolim  15918  geolim2  15919  georeclim  15920  geo2sum  15921  geo2sum2  15922  geoisum1c  15928  0.999...  15929  geoihalfsum  15930  cvgrat  15931  mertenslem1  15932  mertenslem2  15933  mertens  15934  prodf1  15939  prodfclim1  15941  prodrblem  15977  fprodcvg  15978  prodmolem2a  15982  zprod  15985  fprodntriv  15990  prodss  15995  fprodss  15996  fprodsplit  16014  fprodn0f  16039  risefaccl  16063  fallfaccl  16064  risefacfac  16083  binomfallfac  16089  bpolycl  16100  bpolysum  16101  bpolydiflem  16102  fsumkthpow  16104  bpoly2  16105  bpoly3  16106  bpoly4  16107  fsumcube  16108  esum  16128  ege2le3  16138  efsub  16148  efexp  16149  efzval  16150  eftlub  16157  effsumlt  16159  ef4p  16161  tanval3  16182  efi4p  16185  tan0  16199  efival  16200  tanadd  16215  cos2t  16226  cos2tsin  16227  ef01bndlem  16232  cos1bnd  16235  cos2bnd  16236  demoivreALT  16249  eirrlem  16252  rpnnen2lem3  16264  rpnnen2lem11  16272  ruclem12  16289  3dvds  16379  3dvdsdec  16380  3dvds2dec  16381  odd2np1lem  16388  odd2np1  16389  opoe  16411  omoe  16412  opeo  16413  omeo  16414  n2dvdsm1  16417  m1exp1  16424  flodddiv4  16461  bitsfzo  16481  sqgcd  16609  expgcd  16610  nn0seqcvgd  16617  prmind2  16732  hashdvds  16822  phiprmpw  16823  phiprm  16824  eulerthlem2  16829  iserodd  16882  sumhash  16943  fldivp1  16944  prmpwdvds  16951  pockthlem  16952  pockthi  16954  prmreclem4  16966  prmreclem6  16968  4sqlem11  17002  4sqlem19  17010  vdwapun  17021  vdwapid1  17022  vdwlem3  17030  vdwlem5  17032  vdwlem6  17033  vdwlem8  17035  vdwlem9  17036  vdwnnlem2  17043  ramub1lem1  17073  ramub1lem2  17074  ramcl  17076  prmo1  17084  dec5nprm  17113  decexp2  17122  prmlem0  17153  43prm  17169  83prm  17170  139prm  17171  163prm  17172  317prm  17173  631prm  17174  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  1259prm  17183  2503lem1  17184  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  4001prm  17192  gsumsgrpccat  18875  mulgnndir  19143  mulgneg2  19148  m1expaddsub  19540  sylow1lem1  19640  sylow2a  19661  efgsval2  19775  efgsrel  19776  efgsres  19780  cncrng  21424  cnfld1  21429  cnfld1OLD  21430  zsssubrg  21466  cnmgpid  21470  zringcyg  21503  mulgrhm2  21512  pzriprng1ALT  21530  cnmsgnsubg  21618  cnmsgnbas  21619  cnmsgngrp  21620  psgninv  21623  evpmodpmf1o  21637  psdmplcl  22189  blcvx  24839  iihalf2  24980  icopnfcnv  24992  iccpnfhmeo  24995  xrhmeo  24996  icccvx  25000  lebnumii  25017  reparphti  25048  reparphtiOLD  25049  pcoass  25076  pcorevlem  25078  pcorev2  25080  pi1xfrcnv  25109  cnstrcvs  25193  cncvs  25197  ncvsm1  25207  pjthlem1  25490  divcncf  25501  ovolunlem1a  25550  ovolunlem1  25551  ovolicc2lem4  25574  uniioombllem3  25639  uniioombllem4  25640  dyadovol  25647  vitalilem4  25665  mbf0  25688  iblcnlem1  25843  itgcnlem  25845  dvid  25973  dvexp  26011  dvexp2  26012  dvexp3  26036  dveflem  26037  dvlipcn  26053  dvcvx  26079  dvfsumle  26080  dvfsumleOLD  26081  dvfsumlem1  26086  degltp1le  26132  ply1divex  26196  fta1glem1  26227  plyaddlem1  26272  plymullem1  26273  coeidp  26323  dgrid  26324  dvply1  26343  dvply2g  26344  dvply2gOLD  26345  plyremlem  26364  fta1lem  26367  vieta1lem1  26370  vieta1lem2  26371  qaa  26383  iaa  26385  aalioulem3  26394  geolim3  26399  aaliou3lem2  26403  aaliou3lem7  26409  taylply2  26427  taylply2OLD  26428  dvradcnv  26482  pserdvlem2  26490  pserdv2  26492  abelthlem1  26493  abelthlem2  26494  abelthlem6  26498  abelthlem7  26500  abelth  26503  reeff1olem  26508  reeff1o  26509  efcvx  26511  sinhalfpilem  26523  eulerid  26534  cos2pi  26536  sincosq3sgn  26560  sincosq4sgn  26561  tangtx  26565  sincos4thpi  26573  sincos6thpi  26576  pigt3  26578  pige3ALT  26580  abssinper  26581  coskpi  26583  coseq1  26585  efeq1  26588  tanregt0  26599  logneg2  26675  logdivlti  26680  logcnlem4  26705  dvlog2lem  26712  dvlog2  26713  advlog  26714  advlogexp  26715  logtayl  26720  logtayl2  26722  logccv  26723  cxpval  26724  1cxp  26732  cxpcl  26734  cxpp1  26740  cxpsqrt  26763  dvsqrt  26802  dvcnsqrt  26804  sqrtcn  26811  cxpaddlelem  26812  root1id  26815  root1cj  26817  logrec  26824  logb1  26830  logbmpt  26849  ang180lem1  26870  ang180lem2  26871  ang180lem3  26872  isosctrlem1  26879  isosctrlem2  26880  1cubrlem  26902  1cubr  26903  mcubic  26908  binom4  26911  dquartlem1  26912  quartlem1  26918  asinlem  26929  asinlem2  26930  asinlem3a  26931  asinlem3  26932  asinf  26933  atandm2  26938  atandm4  26940  atanf  26941  asinneg  26947  efiasin  26949  sinasin  26950  asinsin  26953  asin1  26955  acos1  26956  reasinsin  26957  asinbnd  26960  cosasin  26965  atanneg  26968  atancj  26971  efiatan  26973  atanlogaddlem  26974  atanlogadd  26975  atanlogsublem  26976  atanlogsub  26977  efiatan2  26978  2efiatan  26979  tanatan  26980  cosatan  26982  cosatanne0  26983  atantan  26984  atanbndlem  26986  bndatandm  26990  atans2  26992  dvatan  26996  atantayl  26998  atantayl2  26999  atantayl3  27000  leibpilem2  27002  leibpi  27003  log2cnv  27005  log2tlbnd  27006  log2ublem3  27009  log2ub  27010  birthdaylem2  27013  birthday  27015  efrlim  27030  efrlimOLD  27031  dfef2  27032  cvxcl  27046  scvxcvx  27047  emcllem2  27058  emcllem4  27060  emcllem7  27063  harmonicbnd4  27072  fsumharmonic  27073  zetacvg  27076  lgamcvg2  27116  lgam1  27125  gam1  27126  wilthlem1  27129  wilthlem2  27130  wilthlem3  27131  basellem2  27143  basellem5  27146  basellem6  27147  basellem7  27148  basellem8  27149  basellem9  27150  0sgm  27205  mule1  27209  ppiprm  27212  ppinprm  27213  chtprm  27214  chtnprm  27215  chpp1  27216  mumullem2  27241  1sgmprm  27261  1sgm2ppw  27262  ppiub  27266  chtublem  27273  chtub  27274  logfaclbnd  27284  logfacbnd3  27285  logfacrlim  27286  logexprlim  27287  mersenne  27289  perfect1  27290  perfectlem1  27291  perfectlem2  27292  perfect  27293  dchrelbasd  27301  dchrmullid  27314  dchrfi  27317  dchrsum2  27330  sumdchr2  27332  bcp1ctr  27341  bposlem8  27353  zabsle1  27358  lgslem1  27359  lgslem2  27360  lgsfcl2  27365  lgsvalmod  27378  lgsneg  27383  lgsdilem  27386  lgsdir2lem1  27387  lgsdir2lem2  27388  lgsdir2lem3  27389  lgsdir2lem5  27391  lgsdir2  27392  lgsdir  27394  lgsdi  27396  lgsne0  27397  lgseisenlem1  27437  lgseisenlem2  27438  lgseisen  27441  lgsquadlem1  27442  lgsquadlem2  27443  lgsquad2lem1  27446  lgsquad2  27448  m1lgs  27450  2lgslem3c  27460  2lgsoddprmlem3c  27474  2lgsoddprmlem3d  27475  2sqlem10  27490  2sqlem11  27491  2sqblem  27493  addsqn2reu  27503  addsqrexnreu  27504  addsqnreup  27505  chtppilimlem2  27536  chebbnd2  27539  chto1lb  27540  rplogsumlem1  27546  rpvmasumlem  27549  dchrmusumlema  27555  dchrmusum2  27556  dchrisum0flblem1  27570  rpvmasum2  27574  mudivsum  27592  mulogsum  27594  vmalogdivsum2  27600  selberg2lem  27612  logdivbnd  27618  pntrmax  27626  pntrsumo1  27627  pntrsumbnd2  27629  pntrlog2bndlem5  27643  pntpbnd1a  27647  pntpbnd2  27649  pntibndlem2  27653  pntlemd  27656  pntlemc  27657  pntlemr  27664  brbtwn2  28938  colinearalglem4  28942  ax5seglem1  28961  ax5seglem2  28962  ax5seglem3  28964  ax5seglem5  28966  ax5seglem7  28968  ax5seglem9  28970  axbtwnid  28972  axpaschlem  28973  axlowdimlem13  28987  axlowdimlem14  28988  axlowdimlem16  28990  axeuclidlem  28995  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  axcontlem8  29004  crctcshwlkn0lem6  29848  clwwlkf1  30081  clwwlknonex2lem2  30140  ex-fl  30479  ex-ind-dvds  30493  vc2OLD  30600  vc0  30606  vcm  30608  nvm1  30697  nvmtri  30703  nvge0  30705  ipval2lem3  30737  ipidsq  30742  lnoadd  30790  ip1ilem  30858  ip1i  30859  ip2i  30860  ipdirilem  30861  ipasslem1  30863  ipasslem2  30864  ipasslem10  30871  minvecolem2  30907  hvsubid  31058  hv2times  31093  hisubcomi  31136  normlem9  31150  normlem7tALT  31151  norm-ii-i  31169  normsubi  31173  hhssnv  31296  pjhthlem1  31423  h1de2bi  31586  homullid  31832  ho2times  31851  lnop0  31998  lnopaddi  32003  lnophmlem2  32049  lnfn0i  32074  lnfnaddi  32075  hst1h  32259  sto2i  32269  stadd3i  32280  addltmulALT  32478  dpmul4  32878  psgnid  33090  cnmsgn0g  33139  altgnsg  33142  isarchi3  33167  archirngz  33169  1fldgenq  33289  ply1dg3rt0irred  33572  ccfldextdgrr  33682  constrsscn  33730  lmatfvlem  33761  qqhval2lem  33927  dya2ub  34235  omssubadd  34265  eulerpartlemgs2  34345  fib5  34370  fib6  34371  ballotlem2  34453  sgnneg  34505  signswch  34538  signlem0  34564  itgexpif  34583  reprlt  34596  breprexp  34610  breprexpnat  34611  hgt750lem2  34629  subfacp1lem5  35152  subfacp1lem6  35153  subfacval2  35155  subfaclim  35156  subfacval3  35157  cvxsconn  35211  resconn  35214  cvmliftlem7  35259  cvmliftlem10  35262  problem4  35636  sinccvglem  35640  sqdivzi  35690  faclimlem1  35705  dnibndlem5  36448  dnibndlem10  36453  ltflcei  37568  sin2h  37570  cos2h  37571  tan2h  37572  poimirlem13  37593  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem31  37611  mblfinlem2  37618  mblfinlem3  37619  dvtan  37630  itg2addnclem3  37633  dvasin  37664  dvacos  37665  areacirc  37673  fdc  37705  mettrifi  37717  heiborlem4  37774  heiborlem6  37776  60gcd7e1  41962  lcmineqlem1  41986  lcmineqlem8  41993  lcmineqlem9  41994  lcmineqlem10  41995  lcmineqlem12  41997  3exp7  42010  3lexlogpow5ineq1  42011  3lexlogpow5ineq5  42017  aks4d1p1p4  42028  aks4d1p1p7  42031  aks4d1p1  42033  facp2  42100  fac2xp3  42196  2xp3dxp2ge1d  42198  factwoffsmonot  42199  sn-1ne2  42254  sqdeccom12  42278  235t711  42293  re1m1e0m0  42373  ipiiie0  42413  sn-0tie0  42415  fltnltalem  42617  sum9cubes  42627  3cubeslem3l  42642  3cubeslem3r  42643  eldioph2lem1  42716  lzenom  42726  irrapxlem1  42778  rmspecsqrtnq  42862  rmxm1  42891  rmym1  42892  2nn0ind  42902  jm2.24nn  42916  jm2.17a  42917  jm2.17b  42918  jm2.17c  42919  jm2.24  42920  acongeq  42940  jm2.18  42945  jm2.27c  42964  jm3.1lem2  42975  rngunsnply  43130  flcidc  43131  inductionexd  44117  unitadd  44157  hashnzfzclim  44291  ofdivrec  44295  lhe4.4ex1a  44298  expgrowth  44304  dvradcnv2  44316  binomcxplemrat  44319  binomcxplemnotnn0  44325  isosctrlem1ALT  44905  monoord2xrv  45399  dvsinax  45834  dvnprodlem3  45869  itgsin0pilem1  45871  itgsbtaddcnst  45903  stoweidlem13  45934  stoweidlem26  45947  stoweidlem34  45955  stoweidlem38  45959  wallispilem2  45987  wallispilem4  45989  wallispi2lem1  45992  stirlinglem1  45995  stirlinglem5  45999  stirlinglem10  46004  dirkerper  46017  dirkertrigeqlem1  46019  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkercncflem4  46027  fourierdlem24  46052  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  1t10e1p1e11  47225  fmtnorec3  47422  fmtno5lem4  47430  fmtno5  47431  257prm  47435  fmtno4nprmfac193  47448  m3prm  47466  139prmALT  47470  127prm  47473  m7prm  47474  lighneallem3  47481  proththd  47488  3exp4mod41  47490  41prothprmlem2  47492  perfectALTVlem2  47596  perfectALTV  47597  11t31e341  47606  evengpop3  47672  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbtbndlem1  47679  0nodd  47893  altgsumbcALT  48078  exple2lt6  48089  nn0sumshdiglemB  48354  ackval3  48417  ackval3012  48426  line2ylem  48485  onetansqsecsq  48853  cotsqcscsq  48854  5m4e1  48891