Axiom ax-1cn 10860

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

This axiom is referenced by:  0cn  10898  1cnd  10901  1ex  10902  mulid1  10904  mulid2  10905  1re  10906  0re  10908  muladd11  11075  peano2cn  11077  mul02lem2  11082  addid1  11085  cnegex2  11087  peano2cnm  11217  0reALT  11248  ine0  11340  mulm1  11346  0lt1  11427  ixi  11534  muleqadd  11549  reccl  11570  recne0  11576  recid  11577  recid2  11578  div1  11594  1div1e1  11595  diveq1  11596  recdiv  11611  divdiv1  11616  divdiv2  11617  recdiv2  11618  conjmul  11622  eqneg  11625  div2neg  11628  recp1lt1  11803  recreclt  11804  recgt0ii  11811  inelr  11893  ofnegsub  11901  peano5nni  11906  nnsscn  11908  nn1m1nn  11924  nn1suc  11925  nnaddcl  11926  nnmulcl  11927  nnne0  11937  nnsub  11947  1m1e0  11975  2cn  11978  3cn  11984  4cn  11988  5cn  11991  6cn  11994  7cn  11997  8cn  12000  9cn  12003  neg1cn  12017  neg1ne0  12019  negneg1e1  12021  1pneg1e0  12022  1m0e1  12024  0p1e1  12025  1p0e1  12027  2m1e1  12029  3m1e2  12031  4m1e3  12032  5m1e4  12033  6m1e5  12034  7m1e6  12035  8m1e7  12036  9m1e8  12037  2p2e4  12038  1p2e3  12046  1p2e3ALT  12047  3p2e5  12054  3p3e6  12055  4p2e6  12056  4p3e7  12057  4p4e8  12058  5p2e7  12059  5p3e8  12060  5p4e9  12061  6p2e8  12062  6p3e9  12063  7p2e9  12064  1t1e1  12065  3t3e9  12070  neg1mulneg1e1  12116  1mhlfehlf  12122  8th4div3  12123  halfpm6th  12124  addltmul  12139  elnn0nn  12205  elz2  12267  zlem1lt  12302  zltlem1  12303  nnaddm1cl  12307  zextlt  12324  zeo  12336  peano5uzi  12339  numsuc  12380  numltc  12392  numsucc  12406  numaddc  12414  6p5lem  12436  5p5e10  12437  6p4e10  12438  7p3e10  12441  8p2e10  12446  10m1e9  12462  4t3lem  12463  7t4e28  12477  9t11e99  12496  decbin2  12507  halfthird  12509  5recm6rec  12510  uzp1  12548  peano2uzr  12572  uzaddcl  12573  rebtwnz  12616  qbtwnre  12862  iccf1o  13157  fz01en  13213  fztp  13241  fzsuc2  13243  fztpval  13247  fseq1m1p1  13260  elfzp1b  13262  fz0to4untppr  13288  predfz  13310  fzoss2  13343  fzval3  13384  fzosplitsnm1  13390  fzo1to4tp  13403  fldiv4p1lem1div2  13483  ceim1l  13495  fldiv  13508  uzrdgxfr  13615  fzen2  13617  nn0ennn  13627  seqm1  13668  seqshft2  13677  monoord2  13682  sermono  13683  seqf1olem1  13690  seqf1olem2  13691  seqz  13699  ser1const  13707  expcl  13728  m1expcl2  13732  expclzlem  13734  expm1t  13739  1exp  13740  mulexpz  13751  expadd  13753  expaddz  13755  expmul  13756  expubnd  13823  sqrecii  13828  neg1sqe1  13841  irec  13846  i4  13849  binom21  13862  sq01  13868  crreczi  13871  bernneq  13872  bernneq2  13873  nn0opthlem1  13910  facndiv  13930  faclbnd4lem1  13935  faclbnd6  13941  bcnp1n  13956  bcm1k  13957  bcp1nk  13959  bcn2  13961  bcp1m1  13962  bcpasc  13963  hashgadd  14020  hashfz  14070  hashfzo  14072  hashxplem  14076  hashbclem  14092  hashf1  14099  seqcoll  14106  swrds1  14307  swrdlsw  14308  wrdind  14363  wrd2ind  14364  swrds2  14581  relexpaddg  14692  rei  14795  imi  14796  recan  14976  iserex  15296  isercoll2  15308  serf0  15320  iseraltlem2  15322  iseraltlem3  15323  iseralt  15324  sumrblem  15351  fsumm1  15391  fsump1  15396  telfsumo  15442  fsumparts  15446  hashiun  15462  binomlem  15469  binom  15470  binom1p  15471  binom11  15472  binom1dif  15473  bcxmas  15475  isumsplit  15480  isum1p  15481  climcndslem1  15489  supcvg  15496  harmonic  15499  arisum  15500  arisum2  15501  trireciplem  15502  geoserg  15506  geolim  15510  geolim2  15511  georeclim  15512  geo2sum  15513  geo2sum2  15514  geoisum1c  15520  0.999...  15521  geoihalfsum  15522  cvgrat  15523  mertenslem1  15524  mertenslem2  15525  mertens  15526  prodf1  15531  prodfclim1  15533  prodrblem  15567  fprodcvg  15568  prodmolem2a  15572  zprod  15575  fprodntriv  15580  prodss  15585  fprodss  15586  fprodsplit  15604  fprodn0f  15629  risefaccl  15653  fallfaccl  15654  risefacfac  15673  binomfallfac  15679  bpolycl  15690  bpolysum  15691  bpolydiflem  15692  fsumkthpow  15694  bpoly2  15695  bpoly3  15696  bpoly4  15697  fsumcube  15698  esum  15718  ege2le3  15727  efsub  15737  efexp  15738  efzval  15739  eftlub  15746  effsumlt  15748  ef4p  15750  tanval3  15771  efi4p  15774  tan0  15788  efival  15789  tanadd  15804  cos2t  15815  cos2tsin  15816  ef01bndlem  15821  cos1bnd  15824  cos2bnd  15825  demoivreALT  15838  eirrlem  15841  rpnnen2lem3  15853  rpnnen2lem11  15861  ruclem12  15878  3dvds  15968  3dvdsdec  15969  3dvds2dec  15970  odd2np1lem  15977  odd2np1  15978  opoe  16000  omoe  16001  opeo  16002  omeo  16003  n2dvdsm1  16006  m1exp1  16013  flodddiv4  16050  bitsfzo  16070  gcdmultipleOLD  16188  sqgcd  16198  nn0seqcvgd  16203  prmind2  16318  hashdvds  16404  phiprmpw  16405  phiprm  16406  eulerthlem2  16411  iserodd  16464  sumhash  16525  fldivp1  16526  prmpwdvds  16533  pockthlem  16534  pockthi  16536  prmreclem4  16548  prmreclem6  16550  4sqlem11  16584  4sqlem19  16592  vdwapun  16603  vdwapid1  16604  vdwlem3  16612  vdwlem5  16614  vdwlem6  16615  vdwlem8  16617  vdwlem9  16618  vdwnnlem2  16625  ramub1lem1  16655  ramub1lem2  16656  ramcl  16658  prmo1  16666  dec5nprm  16695  decexp2  16704  prmlem0  16735  43prm  16751  83prm  16752  139prm  16753  163prm  16754  317prm  16755  631prm  16756  1259lem2  16761  1259lem3  16762  1259lem4  16763  1259lem5  16764  1259prm  16765  2503lem1  16766  2503lem2  16767  2503lem3  16768  2503prm  16769  4001lem1  16770  4001lem2  16771  4001lem3  16772  4001lem4  16773  4001prm  16774  gsumsgrpccat  18393  gsumccatOLD  18394  mulgnndir  18647  mulgneg2  18652  m1expaddsub  19021  sylow1lem1  19118  sylow2a  19139  efgsval2  19254  efgsrel  19255  efgsres  19259  cnfld1  20535  zsssubrg  20568  cnmgpid  20572  zringcyg  20603  mulgrhm2  20612  cnmsgnsubg  20694  cnmsgnbas  20695  cnmsgngrp  20696  psgninv  20699  evpmodpmf1o  20713  blcvx  23867  iihalf2  24002  icopnfcnv  24011  iccpnfhmeo  24014  xrhmeo  24015  icccvx  24019  lebnumii  24035  reparphti  24066  pcoass  24093  pcorevlem  24095  pcorev2  24097  pi1xfrcnv  24126  cnstrcvs  24210  cncvs  24214  ncvsm1  24223  pjthlem1  24506  divcncf  24516  ovolunlem1a  24565  ovolunlem1  24566  ovolicc2lem4  24589  uniioombllem3  24654  uniioombllem4  24655  dyadovol  24662  vitalilem4  24680  mbf0  24703  iblcnlem1  24857  itgcnlem  24859  dvid  24987  dvexp  25022  dvexp2  25023  dvexp3  25047  dveflem  25048  dvlipcn  25063  dvcvx  25089  dvfsumle  25090  dvfsumlem1  25095  degltp1le  25143  ply1divex  25206  fta1glem1  25235  plyaddlem1  25279  plymullem1  25280  coeidp  25329  dgrid  25330  dvply1  25349  dvply2g  25350  plyremlem  25369  fta1lem  25372  vieta1lem1  25375  vieta1lem2  25376  qaa  25388  iaa  25390  aalioulem3  25399  geolim3  25404  aaliou3lem2  25408  aaliou3lem7  25414  taylply2  25432  dvradcnv  25485  pserdvlem2  25492  pserdv2  25494  abelthlem1  25495  abelthlem2  25496  abelthlem6  25500  abelthlem7  25502  abelth  25505  reeff1olem  25510  reeff1o  25511  efcvx  25513  sinhalfpilem  25525  eulerid  25536  cos2pi  25538  sincosq3sgn  25562  sincosq4sgn  25563  tangtx  25567  sincos4thpi  25575  sincos6thpi  25577  pigt3  25579  pige3ALT  25581  abssinper  25582  coskpi  25584  coseq1  25586  efeq1  25589  tanregt0  25600  logneg2  25675  logdivlti  25680  logcnlem4  25705  dvlog2lem  25712  dvlog2  25713  advlog  25714  advlogexp  25715  logtayl  25720  logtayl2  25722  logccv  25723  cxpval  25724  1cxp  25732  cxpcl  25734  cxpp1  25740  cxpsqrt  25763  dvsqrt  25800  dvcnsqrt  25802  sqrtcn  25808  cxpaddlelem  25809  root1id  25812  root1cj  25814  logrec  25818  logb1  25824  logbmpt  25843  ang180lem1  25864  ang180lem2  25865  ang180lem3  25866  isosctrlem1  25873  isosctrlem2  25874  1cubrlem  25896  1cubr  25897  mcubic  25902  binom4  25905  dquartlem1  25906  quartlem1  25912  asinlem  25923  asinlem2  25924  asinlem3a  25925  asinlem3  25926  asinf  25927  atandm2  25932  atandm4  25934  atanf  25935  asinneg  25941  efiasin  25943  sinasin  25944  asinsin  25947  asin1  25949  acos1  25950  reasinsin  25951  asinbnd  25954  cosasin  25959  atanneg  25962  atancj  25965  efiatan  25967  atanlogaddlem  25968  atanlogadd  25969  atanlogsublem  25970  atanlogsub  25971  efiatan2  25972  2efiatan  25973  tanatan  25974  cosatan  25976  cosatanne0  25977  atantan  25978  atanbndlem  25980  bndatandm  25984  atans2  25986  dvatan  25990  atantayl  25992  atantayl2  25993  atantayl3  25994  leibpilem2  25996  leibpi  25997  log2cnv  25999  log2tlbnd  26000  log2ublem3  26003  log2ub  26004  birthdaylem2  26007  birthday  26009  efrlim  26024  dfef2  26025  cvxcl  26039  scvxcvx  26040  emcllem2  26051  emcllem4  26053  emcllem7  26056  harmonicbnd4  26065  fsumharmonic  26066  zetacvg  26069  lgamcvg2  26109  lgam1  26118  gam1  26119  wilthlem1  26122  wilthlem2  26123  wilthlem3  26124  basellem2  26136  basellem5  26139  basellem6  26140  basellem7  26141  basellem8  26142  basellem9  26143  0sgm  26198  mule1  26202  ppiprm  26205  ppinprm  26206  chtprm  26207  chtnprm  26208  chpp1  26209  mumullem2  26234  1sgmprm  26252  1sgm2ppw  26253  ppiub  26257  chtublem  26264  chtub  26265  logfaclbnd  26275  logfacbnd3  26276  logfacrlim  26277  logexprlim  26278  mersenne  26280  perfect1  26281  perfectlem1  26282  perfectlem2  26283  perfect  26284  dchrelbasd  26292  dchrmulid2  26305  dchrfi  26308  dchrsum2  26321  sumdchr2  26323  bcp1ctr  26332  bposlem8  26344  zabsle1  26349  lgslem1  26350  lgslem2  26351  lgsfcl2  26356  lgsvalmod  26369  lgsneg  26374  lgsdilem  26377  lgsdir2lem1  26378  lgsdir2lem2  26379  lgsdir2lem3  26380  lgsdir2lem5  26382  lgsdir2  26383  lgsdir  26385  lgsdi  26387  lgsne0  26388  lgseisenlem1  26428  lgseisenlem2  26429  lgseisen  26432  lgsquadlem1  26433  lgsquadlem2  26434  lgsquad2lem1  26437  lgsquad2  26439  m1lgs  26441  2lgslem3c  26451  2lgsoddprmlem3c  26465  2lgsoddprmlem3d  26466  2sqlem10  26481  2sqlem11  26482  2sqblem  26484  addsqn2reu  26494  addsqrexnreu  26495  addsqnreup  26496  chtppilimlem2  26527  chebbnd2  26530  chto1lb  26531  rplogsumlem1  26537  rpvmasumlem  26540  dchrmusumlema  26546  dchrmusum2  26547  dchrisum0flblem1  26561  rpvmasum2  26565  mudivsum  26583  mulogsum  26585  vmalogdivsum2  26591  selberg2lem  26603  logdivbnd  26609  pntrmax  26617  pntrsumo1  26618  pntrsumbnd2  26620  pntrlog2bndlem5  26634  pntpbnd1a  26638  pntpbnd2  26640  pntibndlem2  26644  pntlemd  26647  pntlemc  26648  pntlemr  26655  brbtwn2  27176  colinearalglem4  27180  ax5seglem1  27199  ax5seglem2  27200  ax5seglem3  27202  ax5seglem5  27204  ax5seglem7  27206  ax5seglem9  27208  axbtwnid  27210  axpaschlem  27211  axlowdimlem13  27225  axlowdimlem14  27226  axlowdimlem16  27228  axeuclidlem  27233  axcontlem2  27236  axcontlem4  27238  axcontlem7  27241  axcontlem8  27242  crctcshwlkn0lem6  28081  clwwlkf1  28314  clwwlknonex2lem2  28373  ex-fl  28712  ex-ind-dvds  28726  vc2OLD  28831  vc0  28837  vcm  28839  nvm1  28928  nvmtri  28934  nvge0  28936  ipval2lem3  28968  ipidsq  28973  lnoadd  29021  ip1ilem  29089  ip1i  29090  ip2i  29091  ipdirilem  29092  ipasslem1  29094  ipasslem2  29095  ipasslem10  29102  minvecolem2  29138  hvsubid  29289  hv2times  29324  hisubcomi  29367  normlem9  29381  normlem7tALT  29382  norm-ii-i  29400  normsubi  29404  hhssnv  29527  pjhthlem1  29654  h1de2bi  29817  homulid2  30063  ho2times  30082  lnop0  30229  lnopaddi  30234  lnophmlem2  30280  lnfn0i  30305  lnfnaddi  30306  hst1h  30490  sto2i  30500  stadd3i  30511  addltmulALT  30709  dpmul4  31090  psgnid  31266  cnmsgn0g  31315  altgnsg  31318  isarchi3  31343  archirngz  31345  ccfldextdgrr  31644  lmatfvlem  31667  qqhval2lem  31831  dya2ub  32137  omssubadd  32167  eulerpartlemgs2  32247  fib5  32272  fib6  32273  ballotlem2  32355  sgnneg  32407  signswch  32440  signlem0  32466  itgexpif  32486  reprlt  32499  breprexp  32513  breprexpnat  32514  hgt750lem2  32532  subfacp1lem5  33046  subfacp1lem6  33047  subfacval2  33049  subfaclim  33050  subfacval3  33051  cvxsconn  33105  resconn  33108  cvmliftlem7  33153  cvmliftlem10  33156  problem4  33526  sinccvglem  33530  sqdivzi  33599  faclimlem1  33615  dnibndlem5  34589  dnibndlem10  34594  ltflcei  35692  sin2h  35694  cos2h  35695  tan2h  35696  poimirlem13  35717  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem31  35735  mblfinlem2  35742  mblfinlem3  35743  dvtan  35754  itg2addnclem3  35757  dvasin  35788  dvacos  35789  areacirc  35797  fdc  35830  mettrifi  35842  heiborlem4  35899  heiborlem6  35901  60gcd7e1  39941  lcmineqlem1  39965  lcmineqlem8  39972  lcmineqlem9  39973  lcmineqlem10  39974  lcmineqlem12  39976  3exp7  39989  3lexlogpow5ineq1  39990  3lexlogpow5ineq5  39996  aks4d1p1p4  40007  aks4d1p1p7  40010  aks4d1p1  40012  facp2  40027  fac2xp3  40088  2xp3dxp2ge1d  40090  factwoffsmonot  40091  sn-1ne2  40216  sqdeccom12  40238  235t711  40240  expgcd  40255  re1m1e0m0  40301  ipiiie0  40340  sn-0tie0  40342  fltnltalem  40415  3cubeslem3l  40424  3cubeslem3r  40425  eldioph2lem1  40498  lzenom  40508  irrapxlem1  40560  rmspecsqrtnq  40644  rmxm1  40672  rmym1  40673  2nn0ind  40683  jm2.24nn  40697  jm2.17a  40698  jm2.17b  40699  jm2.17c  40700  jm2.24  40701  acongeq  40721  jm2.18  40726  jm2.27c  40745  jm3.1lem2  40756  rngunsnply  40914  flcidc  40915  inductionexd  41654  unitadd  41695  hashnzfzclim  41829  ofdivrec  41833  lhe4.4ex1a  41836  expgrowth  41842  dvradcnv2  41854  binomcxplemrat  41857  binomcxplemnotnn0  41863  isosctrlem1ALT  42443  monoord2xrv  42914  dvsinax  43344  dvnprodlem3  43379  itgsin0pilem1  43381  itgsbtaddcnst  43413  stoweidlem13  43444  stoweidlem26  43457  stoweidlem34  43465  stoweidlem38  43469  wallispilem2  43497  wallispilem4  43499  wallispi2lem1  43502  stirlinglem1  43505  stirlinglem5  43509  stirlinglem10  43514  dirkerper  43527  dirkertrigeqlem1  43529  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkercncflem4  43537  fourierdlem24  43562  sqwvfoura  43659  sqwvfourb  43660  fourierswlem  43661  1t10e1p1e11  44690  fmtnorec3  44888  fmtno5lem4  44896  fmtno5  44897  257prm  44901  fmtno4nprmfac193  44914  m3prm  44932  139prmALT  44936  127prm  44939  m7prm  44940  lighneallem3  44947  proththd  44954  3exp4mod41  44956  41prothprmlem2  44958  perfectALTVlem2  45062  perfectALTV  45063  11t31e341  45072  evengpop3  45138  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  bgoldbtbndlem1  45145  0nodd  45252  altgsumbcALT  45577  exple2lt6  45588  nn0sumshdiglemB  45854  ackval3  45917  ackval3012  45926  line2ylem  45985  onetansqsecsq  46349  cotsqcscsq  46350  5m4e1  46387