Axiom ax-1cn 11133

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

This axiom is referenced by:  0cn  11173  1cnd  11177  1ex  11178  mulrid  11181  mullid  11182  1re  11183  0re  11185  muladd11  11355  peano2cn  11357  mul02lem2  11362  addrid  11365  cnegex2  11367  peano2cnm  11499  0reALT  11530  ine0  11624  mulm1  11630  0lt1  11711  ixi  11818  muleqadd  11833  reccl  11854  recne0  11860  recid  11861  recid2  11862  diveq1  11877  div1  11882  1div1e1  11883  recdiv  11899  divdiv1  11904  divdiv2  11905  recdiv2  11906  conjmul  11910  eqneg  11913  div2neg  11916  recp1lt1  12092  recreclt  12093  recgt0ii  12100  neg1cn  12182  neg1ne0  12184  negneg1e1  12186  ofnegsub  12195  peano5nni  12215  nnsscn  12217  nn1m1nn  12233  nn1suc  12234  nnaddcl  12235  nnmulcl  12236  nnne0  12249  nnsub  12259  1m1e0  12292  2cn  12295  3cn  12301  4cn  12305  5cn  12308  6cn  12311  7cn  12314  8cn  12317  9cn  12320  1pneg1e0  12337  1m0e1  12339  0p1e1  12340  1p0e1  12342  2m1e1  12344  2m1e1OLD  12345  3m1e2  12347  4m1e3  12348  5m1e4  12349  6m1e5  12350  7m1e6  12351  8m1e7  12352  9m1e8  12353  2p2e4  12354  1p2e3  12362  1p2e3ALT  12363  3p2e5  12370  3p3e6  12371  4p2e6  12372  4p3e7  12373  4p4e8  12374  5p2e7  12375  5p3e8  12376  5p4e9  12377  6p2e8  12378  6p3e9  12379  7p2e9  12380  1t1e1  12381  3t3e9  12387  neg1mulneg1e1  12435  1mhlfehlf  12442  8th4div3  12443  halfthird  12444  halfpm6th  12445  addltmul  12459  elnn0nn  12525  elz2  12588  zlem1lt  12625  zltlem1  12626  nnaddm1cl  12632  zextlt  12649  zeo  12661  peano5uzi  12664  numsuc  12704  numltc  12721  numsucc  12735  numaddc  12743  6p5lem  12765  5p5e10  12766  6p4e10  12767  7p3e10  12770  8p2e10  12775  10m1e9  12791  4t3lem  12792  7t4e28  12806  9t11e99OLD  12826  decbin2  12838  5recm6rec  12840  uzp1  12878  peano2uzr  12906  uzaddcl  12907  rebtwnz  12950  qbtwnre  13204  iccf1o  13502  fz01en  13559  fztp  13587  fzsuc2  13589  fztpval  13593  fseq1m1p1  13606  elfzp1b  13608  predfz  13660  fzoss2  13695  fzval3  13742  fzosplitsnm1  13748  fzo1to4tp  13762  fldiv4p1lem1div2  13847  ceim1l  13859  fldiv  13872  uzrdgxfr  13982  fzen2  13984  nn0ennn  13994  seqm1  14034  seqshft2  14043  monoord2  14048  sermono  14049  seqf1olem1  14056  seqf1olem2  14057  seqz  14065  ser1const  14073  expcl  14094  expclzlem  14098  m1expcl2  14100  expm1t  14105  1exp  14106  mulexpz  14117  expadd  14119  expaddz  14121  expmul  14122  expubnd  14193  sqrecii  14198  neg1sqe1  14211  irec  14216  i4  14219  binom21  14234  sq01  14240  crreczi  14243  bernneq  14244  bernneq2  14245  nn0opthlem1  14283  facndiv  14303  faclbnd4lem1  14308  faclbnd6  14314  bcnp1n  14329  bcm1k  14330  bcp1nk  14332  bcn2  14334  bcp1m1  14335  bcpasc  14336  hashgadd  14392  hashfz  14442  hashfzo  14444  hashxplem  14448  hashbclem  14467  hashf1  14472  seqcoll  14479  swrds1  14682  swrdlsw  14683  wrdind  14737  wrd2ind  14738  swrds2  14955  relexpaddg  15068  sgnneg  15115  rei  15185  imi  15186  recan  15366  iserex  15686  isercoll2  15698  serf0  15710  iseraltlem2  15712  iseraltlem3  15713  iseralt  15714  sumrblem  15740  fsumm1  15780  telfsumo  15832  fsumparts  15836  hashiun  15852  binomlem  15861  binom  15862  binom1p  15863  binom11  15864  binom1dif  15865  bcxmas  15867  isumsplit  15872  isum1p  15873  climcndslem1  15881  supcvg  15888  harmonic  15891  arisum  15892  arisum2  15893  trireciplem  15894  geoserg  15898  geolim  15902  geolim2  15903  georeclim  15904  geo2sum  15905  geo2sum2  15906  geoisum1c  15912  0.999...  15913  geoihalfsum  15914  cvgrat  15915  mertenslem1  15916  mertenslem2  15917  mertens  15918  prodf1  15923  prodfclim1  15925  prodrblem  15961  fprodcvg  15962  prodmolem2a  15966  zprod  15969  fprodntriv  15974  prodss  15979  fprodss  15980  fprodsplit  15998  fprodn0f  16023  risefaccl  16047  fallfaccl  16048  risefacfac  16067  binomfallfac  16073  bpolycl  16084  bpolysum  16085  bpolydiflem  16086  fsumkthpow  16088  bpoly2  16089  bpoly3  16090  bpoly4  16091  fsumcube  16092  esum  16112  ege2le3  16122  efsub  16134  efexp  16135  efzval  16136  eftlub  16143  effsumlt  16145  ef4p  16147  tanval3  16168  efi4p  16171  tan0  16185  efival  16186  tanadd  16201  cos2t  16212  cos2tsin  16213  ef01bndlem  16218  cos1bnd  16221  cos2bnd  16222  demoivreALT  16235  eirrlem  16238  rpnnen2lem3  16250  rpnnen2lem11  16258  ruclem12  16275  3dvds  16367  3dvdsdec  16368  3dvds2dec  16369  odd2np1lem  16376  odd2np1  16377  opoe  16399  omoe  16400  opeo  16401  omeo  16402  n2dvdsm1  16405  m1exp1  16412  flodddiv4  16451  bitsfzo  16471  sqgcd  16598  expgcd  16599  nn0seqcvgd  16606  prmind2  16721  hashdvds  16812  phiprmpw  16813  phiprm  16814  eulerthlem2  16819  iserodd  16873  sumhash  16934  fldivp1  16935  prmpwdvds  16942  pockthlem  16943  pockthi  16945  prmreclem4  16957  prmreclem6  16959  4sqlem11  16993  4sqlem19  17001  vdwapun  17012  vdwapid1  17013  vdwlem3  17021  vdwlem5  17023  vdwlem6  17024  vdwlem8  17026  vdwlem9  17027  vdwnnlem2  17034  ramub1lem1  17064  ramub1lem2  17065  ramcl  17067  prmo1  17075  dec5nprm  17104  prmlem0  17143  43prm  17160  83prm  17161  139prm  17162  163prm  17163  317prm  17164  631prm  17165  1259lem2  17170  1259lem3  17171  1259lem4  17172  1259lem5  17173  1259prm  17174  2503lem1  17175  2503lem2  17176  2503lem3  17177  2503prm  17178  4001lem1  17179  4001lem2  17180  4001lem3  17181  4001lem4  17182  4001prm  17183  gsumsgrpccat  18876  mulgnndir  19147  mulgneg2  19152  m1expaddsub  19540  sylow1lem1  19640  sylow2a  19661  efgsval2  19775  efgsrel  19776  efgsres  19780  cncrng  21447  cnfld1  21451  zsssubrg  21479  cnmgpid  21483  zringcyg  21523  mulgrhm2  21532  pzriprng1ALT  21550  cnmsgnsubg  21631  cnmsgnbas  21632  cnmsgngrp  21633  psgninv  21636  evpmodpmf1o  21650  psdmplcl  22229  blcvx  24860  iihalf2  24997  icopnfcnv  25006  iccpnfhmeo  25009  xrhmeo  25010  icccvx  25014  lebnumii  25030  reparphti  25061  pcoass  25088  pcorevlem  25090  pcorev2  25092  pi1xfrcnv  25121  cnstrcvs  25205  cncvs  25209  ncvsm1  25218  pjthlem1  25501  divcncf  25511  ovolunlem1a  25560  ovolunlem1  25561  ovolicc2lem4  25584  uniioombllem3  25649  uniioombllem4  25650  dyadovol  25657  vitalilem4  25675  mbf0  25698  iblcnlem1  25852  itgcnlem  25854  dvid  25982  dvexp  26017  dvexp2  26018  dvexp3  26042  dveflem  26043  dvlipcn  26058  dvcvx  26084  dvfsumle  26085  dvfsumlem1  26090  degltp1le  26135  ply1divex  26199  fta1glem1  26230  plyaddlem1  26275  plymullem1  26276  coeidp  26325  dgrid  26326  dvply1  26350  dvply2g  26351  plyremlem  26370  fta1lem  26373  vieta1lem1  26376  vieta1lem2  26377  qaa  26389  iaa  26391  aalioulem3  26400  geolim3  26405  aaliou3lem2  26409  aaliou3lem7  26415  taylply2  26433  dvradcnv  26486  pserdvlem2  26493  pserdv2  26495  abelthlem1  26496  abelthlem2  26497  abelthlem6  26501  abelthlem7  26503  abelth  26506  reeff1olem  26511  reeff1o  26512  efcvx  26514  sinhalfpilem  26530  eulerid  26541  cos2pi  26543  sincosq3sgn  26567  sincosq4sgn  26568  tangtx  26572  sincos4thpi  26580  sincos6thpi  26583  pigt3  26585  pige3ALT  26587  abssinper  26588  coskpi  26590  coseq1  26592  efeq1  26595  tanregt0  26606  logneg2  26682  logdivlti  26687  logcnlem4  26712  dvlog2lem  26719  dvlog2  26720  advlog  26721  advlogexp  26722  logtayl  26727  logtayl2  26729  logccv  26730  cxpval  26731  1cxp  26739  cxpcl  26741  cxpp1  26747  cxpsqrt  26770  dvsqrt  26809  dvcnsqrt  26811  sqrtcn  26817  cxpaddlelem  26818  root1id  26821  root1cj  26823  logrec  26830  logb1  26836  logbmpt  26855  ang180lem1  26876  ang180lem2  26877  ang180lem3  26878  isosctrlem1  26885  isosctrlem2  26886  1cubrlem  26908  1cubr  26909  mcubic  26914  binom4  26917  dquartlem1  26918  quartlem1  26924  asinlem  26935  asinlem2  26936  asinlem3a  26937  asinlem3  26938  asinf  26939  atandm2  26944  atandm4  26946  atanf  26947  asinneg  26953  efiasin  26955  sinasin  26956  asinsin  26959  asin1  26961  acos1  26962  reasinsin  26963  asinbnd  26966  cosasin  26971  atanneg  26974  atancj  26977  efiatan  26979  atanlogaddlem  26980  atanlogadd  26981  atanlogsublem  26982  atanlogsub  26983  efiatan2  26984  2efiatan  26985  tanatan  26986  cosatan  26988  cosatanne0  26989  atantan  26990  atanbndlem  26992  bndatandm  26996  atans2  26998  dvatan  27002  atantayl  27004  atantayl2  27005  atantayl3  27006  leibpilem2  27008  leibpi  27009  log2cnv  27011  log2tlbnd  27012  log2ublem3  27015  log2ub  27016  birthdaylem2  27019  birthday  27021  efrlim  27036  dfef2  27037  cvxcl  27051  scvxcvx  27052  emcllem2  27063  emcllem4  27065  emcllem7  27068  harmonicbnd4  27077  fsumharmonic  27078  zetacvg  27081  lgamcvg2  27121  lgam1  27130  gam1  27131  wilthlem1  27134  wilthlem2  27135  wilthlem3  27136  basellem2  27148  basellem5  27151  basellem6  27152  basellem7  27153  basellem8  27154  basellem9  27155  0sgm  27210  mule1  27214  ppiprm  27217  ppinprm  27218  chtprm  27219  chtnprm  27220  chpp1  27221  mumullem2  27246  1sgmprm  27265  1sgm2ppw  27266  ppiub  27270  chtublem  27277  chtub  27278  logfaclbnd  27288  logfacbnd3  27289  logfacrlim  27290  logexprlim  27291  mersenne  27293  perfect1  27294  perfectlem1  27295  perfectlem2  27296  perfect  27297  dchrelbasd  27305  dchrmullid  27318  dchrfi  27321  dchrsum2  27334  sumdchr2  27336  bcp1ctr  27345  bposlem8  27357  zabsle1  27362  lgslem1  27363  lgslem2  27364  lgsfcl2  27369  lgsvalmod  27382  lgsneg  27387  lgsdilem  27390  lgsdir2lem1  27391  lgsdir2lem2  27392  lgsdir2lem3  27393  lgsdir2lem5  27395  lgsdir2  27396  lgsdir  27398  lgsdi  27400  lgsne0  27401  lgseisenlem1  27441  lgseisenlem2  27442  lgseisen  27445  lgsquadlem1  27446  lgsquadlem2  27447  lgsquad2lem1  27450  lgsquad2  27452  m1lgs  27454  2lgslem3c  27464  2lgsoddprmlem3c  27478  2lgsoddprmlem3d  27479  2sqlem10  27494  2sqlem11  27495  2sqblem  27497  addsqn2reu  27507  addsqrexnreu  27508  addsqnreup  27509  chtppilimlem2  27540  chebbnd2  27543  chto1lb  27544  rplogsumlem1  27550  rpvmasumlem  27553  dchrmusumlema  27559  dchrmusum2  27560  dchrisum0flblem1  27574  rpvmasum2  27578  mudivsum  27596  mulogsum  27598  vmalogdivsum2  27604  selberg2lem  27616  logdivbnd  27622  pntrmax  27630  pntrsumo1  27631  pntrsumbnd2  27633  pntrlog2bndlem5  27647  pntpbnd1a  27651  pntpbnd2  27653  pntibndlem2  27657  pntlemd  27660  pntlemc  27661  pntlemr  27668  brbtwn2  29108  colinearalglem4  29112  ax5seglem1  29131  ax5seglem2  29132  ax5seglem3  29134  ax5seglem5  29136  ax5seglem7  29138  ax5seglem9  29140  axbtwnid  29142  axpaschlem  29143  axlowdimlem13  29157  axlowdimlem14  29158  axlowdimlem16  29160  axeuclidlem  29165  axcontlem2  29168  axcontlem4  29170  axcontlem7  29173  axcontlem8  29174  crctcshwlkn0lem6  30017  clwwlkf1  30253  clwwlknonex2lem2  30312  ex-fl  30651  ex-ind-dvds  30665  vc2OLD  30773  vc0  30779  vcm  30781  nvm1  30870  nvmtri  30876  nvge0  30878  ipval2lem3  30910  ipidsq  30915  lnoadd  30963  ip1ilem  31031  ip1i  31032  ip2i  31033  ipdirilem  31034  ipasslem1  31036  ipasslem2  31037  ipasslem10  31044  minvecolem2  31080  hvsubid  31231  hv2times  31266  hisubcomi  31309  normlem9  31323  normlem7tALT  31324  norm-ii-i  31342  normsubi  31346  hhssnv  31469  pjhthlem1  31596  h1de2bi  31759  homullid  32005  ho2times  32024  lnop0  32171  lnopaddi  32176  lnophmlem2  32222  lnfn0i  32247  lnfnaddi  32248  hst1h  32432  sto2i  32442  stadd3i  32453  addltmulALT  32651  dpmul4  33093  psgnid  33279  cnmsgn0g  33328  altgnsg  33331  isarchi3  33369  archirngz  33371  1fldgenq  33511  ply1dg3rt0irred  33782  esplyfvaln  33873  ccfldextdgrr  33971  constrsscn  34039  constrabscl  34077  cos9thpiminplylem1  34081  cos9thpiminplylem4  34084  cos9thpiminplylem5  34085  lmatfvlem  34114  qqhval2lem  34280  dya2ub  34569  omssubadd  34599  eulerpartlemgs2  34679  fib5  34704  fib6  34705  ballotlem2  34788  signswch  34857  signlem0  34883  itgexpif  34902  reprlt  34915  breprexp  34929  breprexpnat  34930  hgt750lem2  34948  subfacp1lem5  35539  subfacp1lem6  35540  subfacval2  35542  subfaclim  35543  subfacval3  35544  cvxsconn  35598  resconn  35601  cvmliftlem7  35646  cvmliftlem10  35649  problem4  36023  sinccvglem  36027  sqdivzi  36083  faclimlem1  36098  dnibndlem5  36925  dnibndlem10  36930  ltflcei  38112  sin2h  38114  cos2h  38115  tan2h  38116  poimirlem13  38137  poimirlem16  38140  poimirlem17  38141  poimirlem19  38143  poimirlem20  38144  poimirlem31  38155  mblfinlem2  38162  mblfinlem3  38163  dvtan  38174  itg2addnclem3  38177  dvasin  38208  dvacos  38209  areacirc  38217  fdc  38249  mettrifi  38261  heiborlem4  38318  heiborlem6  38320  60gcd7e1  42627  lcmineqlem1  42651  lcmineqlem8  42658  lcmineqlem9  42659  lcmineqlem10  42660  lcmineqlem12  42662  3exp7  42675  3lexlogpow5ineq1  42676  3lexlogpow5ineq5  42682  aks4d1p1p4  42693  aks4d1p1p7  42696  aks4d1p1  42698  facp2  42765  1p3e4  42879  sn-1ne2  42885  sqdeccom12  42903  235t711  42919  sin2t3rdpi  42967  cos2t3rdpi  42968  re1m1e0m0  43011  ipiiie0  43052  sn-0tie0  43078  fltnltalem  43249  sum9cubes  43259  3cubeslem3l  43272  3cubeslem3r  43273  eldioph2lem1  43346  lzenom  43356  irrapxlem1  43404  rmspecsqrtnq  43488  rmxm1  43516  rmym1  43517  2nn0ind  43527  jm2.24nn  43541  jm2.17a  43542  jm2.17b  43543  jm2.17c  43544  jm2.24  43545  acongeq  43565  jm2.18  43570  jm2.27c  43589  jm3.1lem2  43600  rngunsnply  43751  flcidc  43752  inductionexd  44736  unitadd  44776  hashnzfzclim  44903  ofdivrec  44907  lhe4.4ex1a  44910  expgrowth  44916  dvradcnv2  44928  binomcxplemrat  44931  binomcxplemnotnn0  44937  isosctrlem1ALT  45514  monoord2xrv  46062  dvsinax  46492  dvnprodlem3  46527  itgsin0pilem1  46529  itgsbtaddcnst  46561  stoweidlem13  46592  stoweidlem26  46605  stoweidlem34  46613  stoweidlem38  46617  wallispilem2  46645  wallispilem4  46647  wallispi2lem1  46650  stirlinglem1  46653  stirlinglem5  46657  stirlinglem10  46662  dirkerper  46675  dirkertrigeqlem1  46677  dirkertrigeqlem3  46679  dirkertrigeq  46680  dirkercncflem4  46685  fourierdlem24  46710  sqwvfoura  46807  sqwvfourb  46808  fourierswlem  46809  cos5t  47478  goldratmolem2  47485  lambert0  47486  lamberte  47487  cjnpoly  47488  1t10e1p1e11  47909  ceil5half3  47945  modm2nep1  47971  modm1nep2  47973  modm1nem2  47974  fmtnorec3  48162  fmtno5lem4  48170  fmtno5  48171  257prm  48175  fmtno4nprmfac193  48188  m3prm  48206  139prmALT  48210  127prm  48213  m7prm  48214  lighneallem3  48221  proththd  48228  3exp4mod41  48230  41prothprmlem2  48232  perfectALTVlem2  48349  perfectALTV  48350  11t31e341  48359  evengpop3  48425  nnsum4primeseven  48427  nnsum4primesevenALTV  48428  bgoldbtbndlem1  48432  0nodd  48797  altgsumbcALT  48980  exple2lt6  48991  nn0sumshdiglemB  49247  ackval3  49310  ackval3012  49319  line2ylem  49378  onetansqsecsq  50387  cotsqcscsq  50388  5m4e1  50423