Axiom ax-1cn 10787

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

This axiom is referenced by:  0cn  10825  1cnd  10828  1ex  10829  mulid1  10831  mulid2  10832  1re  10833  0re  10835  muladd11  11002  peano2cn  11004  mul02lem2  11009  addid1  11012  cnegex2  11014  peano2cnm  11144  0reALT  11175  ine0  11267  mulm1  11273  0lt1  11354  ixi  11461  muleqadd  11476  reccl  11497  recne0  11503  recid  11504  recid2  11505  div1  11521  1div1e1  11522  diveq1  11523  recdiv  11538  divdiv1  11543  divdiv2  11544  recdiv2  11545  conjmul  11549  eqneg  11552  div2neg  11555  recp1lt1  11730  recreclt  11731  recgt0ii  11738  inelr  11820  ofnegsub  11828  peano5nni  11833  nnsscn  11835  nn1m1nn  11851  nn1suc  11852  nnaddcl  11853  nnmulcl  11854  nnne0  11864  nnsub  11874  1m1e0  11902  2cn  11905  3cn  11911  4cn  11915  5cn  11918  6cn  11921  7cn  11924  8cn  11927  9cn  11930  neg1cn  11944  neg1ne0  11946  negneg1e1  11948  1pneg1e0  11949  1m0e1  11951  0p1e1  11952  1p0e1  11954  2m1e1  11956  3m1e2  11958  4m1e3  11959  5m1e4  11960  6m1e5  11961  7m1e6  11962  8m1e7  11963  9m1e8  11964  2p2e4  11965  1p2e3  11973  1p2e3ALT  11974  3p2e5  11981  3p3e6  11982  4p2e6  11983  4p3e7  11984  4p4e8  11985  5p2e7  11986  5p3e8  11987  5p4e9  11988  6p2e8  11989  6p3e9  11990  7p2e9  11991  1t1e1  11992  3t3e9  11997  neg1mulneg1e1  12043  1mhlfehlf  12049  8th4div3  12050  halfpm6th  12051  addltmul  12066  elnn0nn  12132  elz2  12194  zlem1lt  12229  zltlem1  12230  nnaddm1cl  12234  zextlt  12251  zeo  12263  peano5uzi  12266  numsuc  12307  numltc  12319  numsucc  12333  numaddc  12341  6p5lem  12363  5p5e10  12364  6p4e10  12365  7p3e10  12368  8p2e10  12373  10m1e9  12389  4t3lem  12390  7t4e28  12404  9t11e99  12423  decbin2  12434  halfthird  12436  5recm6rec  12437  uzp1  12475  peano2uzr  12499  uzaddcl  12500  rebtwnz  12543  qbtwnre  12789  iccf1o  13084  fz01en  13140  fztp  13168  fzsuc2  13170  fztpval  13174  fseq1m1p1  13187  elfzp1b  13189  fz0to4untppr  13215  predfz  13237  fzoss2  13270  fzval3  13311  fzosplitsnm1  13317  fzo1to4tp  13330  fldiv4p1lem1div2  13410  ceim1l  13420  fldiv  13433  uzrdgxfr  13540  fzen2  13542  nn0ennn  13552  seqm1  13593  seqshft2  13602  monoord2  13607  sermono  13608  seqf1olem1  13615  seqf1olem2  13616  seqz  13624  ser1const  13632  expcl  13653  m1expcl2  13657  expclzlem  13659  expm1t  13663  1exp  13664  mulexpz  13675  expadd  13677  expaddz  13679  expmul  13680  expubnd  13747  sqrecii  13752  neg1sqe1  13765  irec  13770  i4  13773  binom21  13786  sq01  13792  crreczi  13795  bernneq  13796  bernneq2  13797  nn0opthlem1  13834  facndiv  13854  faclbnd4lem1  13859  faclbnd6  13865  bcnp1n  13880  bcm1k  13881  bcp1nk  13883  bcn2  13885  bcp1m1  13886  bcpasc  13887  hashgadd  13944  hashfz  13994  hashfzo  13996  hashxplem  14000  hashbclem  14016  hashf1  14023  seqcoll  14030  swrds1  14231  swrdlsw  14232  wrdind  14287  wrd2ind  14288  swrds2  14505  relexpaddg  14616  rei  14719  imi  14720  recan  14900  iserex  15220  isercoll2  15232  serf0  15244  iseraltlem2  15246  iseraltlem3  15247  iseralt  15248  sumrblem  15275  fsumm1  15315  fsump1  15320  telfsumo  15366  fsumparts  15370  hashiun  15386  binomlem  15393  binom  15394  binom1p  15395  binom11  15396  binom1dif  15397  bcxmas  15399  isumsplit  15404  isum1p  15405  climcndslem1  15413  supcvg  15420  harmonic  15423  arisum  15424  arisum2  15425  trireciplem  15426  geoserg  15430  geolim  15434  geolim2  15435  georeclim  15436  geo2sum  15437  geo2sum2  15438  geoisum1c  15444  0.999...  15445  geoihalfsum  15446  cvgrat  15447  mertenslem1  15448  mertenslem2  15449  mertens  15450  prodf1  15455  prodfclim1  15457  prodrblem  15491  fprodcvg  15492  prodmolem2a  15496  zprod  15499  fprodntriv  15504  prodss  15509  fprodss  15510  fprodsplit  15528  fprodn0f  15553  risefaccl  15577  fallfaccl  15578  risefacfac  15597  binomfallfac  15603  bpolycl  15614  bpolysum  15615  bpolydiflem  15616  fsumkthpow  15618  bpoly2  15619  bpoly3  15620  bpoly4  15621  fsumcube  15622  esum  15642  ege2le3  15651  efsub  15661  efexp  15662  efzval  15663  eftlub  15670  effsumlt  15672  ef4p  15674  tanval3  15695  efi4p  15698  tan0  15712  efival  15713  tanadd  15728  cos2t  15739  cos2tsin  15740  ef01bndlem  15745  cos1bnd  15748  cos2bnd  15749  demoivreALT  15762  eirrlem  15765  rpnnen2lem3  15777  rpnnen2lem11  15785  ruclem12  15802  3dvds  15892  3dvdsdec  15893  3dvds2dec  15894  odd2np1lem  15901  odd2np1  15902  opoe  15924  omoe  15925  opeo  15926  omeo  15927  n2dvdsm1  15930  m1exp1  15937  flodddiv4  15974  bitsfzo  15994  gcdmultipleOLD  16112  sqgcd  16122  nn0seqcvgd  16127  prmind2  16242  hashdvds  16328  phiprmpw  16329  phiprm  16330  eulerthlem2  16335  iserodd  16388  sumhash  16449  fldivp1  16450  prmpwdvds  16457  pockthlem  16458  pockthi  16460  prmreclem4  16472  prmreclem6  16474  4sqlem11  16508  4sqlem19  16516  vdwapun  16527  vdwapid1  16528  vdwlem3  16536  vdwlem5  16538  vdwlem6  16539  vdwlem8  16541  vdwlem9  16542  vdwnnlem2  16549  ramub1lem1  16579  ramub1lem2  16580  ramcl  16582  prmo1  16590  dec5nprm  16619  decexp2  16628  prmlem0  16659  43prm  16675  83prm  16676  139prm  16677  163prm  16678  317prm  16679  631prm  16680  1259lem2  16685  1259lem3  16686  1259lem4  16687  1259lem5  16688  1259prm  16689  2503lem1  16690  2503lem2  16691  2503lem3  16692  2503prm  16693  4001lem1  16694  4001lem2  16695  4001lem3  16696  4001lem4  16697  4001prm  16698  gsumsgrpccat  18266  gsumccatOLD  18267  mulgnndir  18520  mulgneg2  18525  m1expaddsub  18890  sylow1lem1  18987  sylow2a  19008  efgsval2  19123  efgsrel  19124  efgsres  19128  cnfld1  20388  zsssubrg  20421  cnmgpid  20425  zringcyg  20456  mulgrhm2  20465  cnmsgnsubg  20539  cnmsgnbas  20540  cnmsgngrp  20541  psgninv  20544  evpmodpmf1o  20558  blcvx  23695  iihalf2  23830  icopnfcnv  23839  iccpnfhmeo  23842  xrhmeo  23843  icccvx  23847  lebnumii  23863  reparphti  23894  pcoass  23921  pcorevlem  23923  pcorev2  23925  pi1xfrcnv  23954  cnstrcvs  24038  cncvs  24042  ncvsm1  24051  pjthlem1  24334  divcncf  24344  ovolunlem1a  24393  ovolunlem1  24394  ovolicc2lem4  24417  uniioombllem3  24482  uniioombllem4  24483  dyadovol  24490  vitalilem4  24508  mbf0  24531  iblcnlem1  24685  itgcnlem  24687  dvid  24815  dvexp  24850  dvexp2  24851  dvexp3  24875  dveflem  24876  dvlipcn  24891  dvcvx  24917  dvfsumle  24918  dvfsumlem1  24923  degltp1le  24971  ply1divex  25034  fta1glem1  25063  plyaddlem1  25107  plymullem1  25108  coeidp  25157  dgrid  25158  dvply1  25177  dvply2g  25178  plyremlem  25197  fta1lem  25200  vieta1lem1  25203  vieta1lem2  25204  qaa  25216  iaa  25218  aalioulem3  25227  geolim3  25232  aaliou3lem2  25236  aaliou3lem7  25242  taylply2  25260  dvradcnv  25313  pserdvlem2  25320  pserdv2  25322  abelthlem1  25323  abelthlem2  25324  abelthlem6  25328  abelthlem7  25330  abelth  25333  reeff1olem  25338  reeff1o  25339  efcvx  25341  sinhalfpilem  25353  eulerid  25364  cos2pi  25366  sincosq3sgn  25390  sincosq4sgn  25391  tangtx  25395  sincos4thpi  25403  sincos6thpi  25405  pigt3  25407  pige3ALT  25409  abssinper  25410  coskpi  25412  coseq1  25414  efeq1  25417  tanregt0  25428  logneg2  25503  logdivlti  25508  logcnlem4  25533  dvlog2lem  25540  dvlog2  25541  advlog  25542  advlogexp  25543  logtayl  25548  logtayl2  25550  logccv  25551  cxpval  25552  1cxp  25560  cxpcl  25562  cxpp1  25568  cxpsqrt  25591  dvsqrt  25628  dvcnsqrt  25630  sqrtcn  25636  cxpaddlelem  25637  root1id  25640  root1cj  25642  logrec  25646  logb1  25652  logbmpt  25671  ang180lem1  25692  ang180lem2  25693  ang180lem3  25694  isosctrlem1  25701  isosctrlem2  25702  1cubrlem  25724  1cubr  25725  mcubic  25730  binom4  25733  dquartlem1  25734  quartlem1  25740  asinlem  25751  asinlem2  25752  asinlem3a  25753  asinlem3  25754  asinf  25755  atandm2  25760  atandm4  25762  atanf  25763  asinneg  25769  efiasin  25771  sinasin  25772  asinsin  25775  asin1  25777  acos1  25778  reasinsin  25779  asinbnd  25782  cosasin  25787  atanneg  25790  atancj  25793  efiatan  25795  atanlogaddlem  25796  atanlogadd  25797  atanlogsublem  25798  atanlogsub  25799  efiatan2  25800  2efiatan  25801  tanatan  25802  cosatan  25804  cosatanne0  25805  atantan  25806  atanbndlem  25808  bndatandm  25812  atans2  25814  dvatan  25818  atantayl  25820  atantayl2  25821  atantayl3  25822  leibpilem2  25824  leibpi  25825  log2cnv  25827  log2tlbnd  25828  log2ublem3  25831  log2ub  25832  birthdaylem2  25835  birthday  25837  efrlim  25852  dfef2  25853  cvxcl  25867  scvxcvx  25868  emcllem2  25879  emcllem4  25881  emcllem7  25884  harmonicbnd4  25893  fsumharmonic  25894  zetacvg  25897  lgamcvg2  25937  lgam1  25946  gam1  25947  wilthlem1  25950  wilthlem2  25951  wilthlem3  25952  basellem2  25964  basellem5  25967  basellem6  25968  basellem7  25969  basellem8  25970  basellem9  25971  0sgm  26026  mule1  26030  ppiprm  26033  ppinprm  26034  chtprm  26035  chtnprm  26036  chpp1  26037  mumullem2  26062  1sgmprm  26080  1sgm2ppw  26081  ppiub  26085  chtublem  26092  chtub  26093  logfaclbnd  26103  logfacbnd3  26104  logfacrlim  26105  logexprlim  26106  mersenne  26108  perfect1  26109  perfectlem1  26110  perfectlem2  26111  perfect  26112  dchrelbasd  26120  dchrmulid2  26133  dchrfi  26136  dchrsum2  26149  sumdchr2  26151  bcp1ctr  26160  bposlem8  26172  zabsle1  26177  lgslem1  26178  lgslem2  26179  lgsfcl2  26184  lgsvalmod  26197  lgsneg  26202  lgsdilem  26205  lgsdir2lem1  26206  lgsdir2lem2  26207  lgsdir2lem3  26208  lgsdir2lem5  26210  lgsdir2  26211  lgsdir  26213  lgsdi  26215  lgsne0  26216  lgseisenlem1  26256  lgseisenlem2  26257  lgseisen  26260  lgsquadlem1  26261  lgsquadlem2  26262  lgsquad2lem1  26265  lgsquad2  26267  m1lgs  26269  2lgslem3c  26279  2lgsoddprmlem3c  26293  2lgsoddprmlem3d  26294  2sqlem10  26309  2sqlem11  26310  2sqblem  26312  addsqn2reu  26322  addsqrexnreu  26323  addsqnreup  26324  chtppilimlem2  26355  chebbnd2  26358  chto1lb  26359  rplogsumlem1  26365  rpvmasumlem  26368  dchrmusumlema  26374  dchrmusum2  26375  dchrisum0flblem1  26389  rpvmasum2  26393  mudivsum  26411  mulogsum  26413  vmalogdivsum2  26419  selberg2lem  26431  logdivbnd  26437  pntrmax  26445  pntrsumo1  26446  pntrsumbnd2  26448  pntrlog2bndlem5  26462  pntpbnd1a  26466  pntpbnd2  26468  pntibndlem2  26472  pntlemd  26475  pntlemc  26476  pntlemr  26483  brbtwn2  26996  colinearalglem4  27000  ax5seglem1  27019  ax5seglem2  27020  ax5seglem3  27022  ax5seglem5  27024  ax5seglem7  27026  ax5seglem9  27028  axbtwnid  27030  axpaschlem  27031  axlowdimlem13  27045  axlowdimlem14  27046  axlowdimlem16  27048  axeuclidlem  27053  axcontlem2  27056  axcontlem4  27058  axcontlem7  27061  axcontlem8  27062  crctcshwlkn0lem6  27899  clwwlkf1  28132  clwwlknonex2lem2  28191  ex-fl  28530  ex-ind-dvds  28544  vc2OLD  28649  vc0  28655  vcm  28657  nvm1  28746  nvmtri  28752  nvge0  28754  ipval2lem3  28786  ipidsq  28791  lnoadd  28839  ip1ilem  28907  ip1i  28908  ip2i  28909  ipdirilem  28910  ipasslem1  28912  ipasslem2  28913  ipasslem10  28920  minvecolem2  28956  hvsubid  29107  hv2times  29142  hisubcomi  29185  normlem9  29199  normlem7tALT  29200  norm-ii-i  29218  normsubi  29222  hhssnv  29345  pjhthlem1  29472  h1de2bi  29635  homulid2  29881  ho2times  29900  lnop0  30047  lnopaddi  30052  lnophmlem2  30098  lnfn0i  30123  lnfnaddi  30124  hst1h  30308  sto2i  30318  stadd3i  30329  addltmulALT  30527  dpmul4  30908  psgnid  31083  cnmsgn0g  31132  altgnsg  31135  isarchi3  31160  archirngz  31162  ccfldextdgrr  31456  lmatfvlem  31479  qqhval2lem  31643  dya2ub  31949  omssubadd  31979  eulerpartlemgs2  32059  fib5  32084  fib6  32085  ballotlem2  32167  sgnneg  32219  signswch  32252  signlem0  32278  itgexpif  32298  reprlt  32311  breprexp  32325  breprexpnat  32326  hgt750lem2  32344  subfacp1lem5  32859  subfacp1lem6  32860  subfacval2  32862  subfaclim  32863  subfacval3  32864  cvxsconn  32918  resconn  32921  cvmliftlem7  32966  cvmliftlem10  32969  problem4  33339  sinccvglem  33343  sqdivzi  33411  faclimlem1  33427  dnibndlem5  34399  dnibndlem10  34404  ltflcei  35502  sin2h  35504  cos2h  35505  tan2h  35506  poimirlem13  35527  poimirlem16  35530  poimirlem17  35531  poimirlem19  35533  poimirlem20  35534  poimirlem31  35545  mblfinlem2  35552  mblfinlem3  35553  dvtan  35564  itg2addnclem3  35567  dvasin  35598  dvacos  35599  areacirc  35607  fdc  35640  mettrifi  35652  heiborlem4  35709  heiborlem6  35711  60gcd7e1  39747  lcmineqlem1  39771  lcmineqlem8  39778  lcmineqlem9  39779  lcmineqlem10  39780  lcmineqlem12  39782  3exp7  39795  3lexlogpow5ineq1  39796  3lexlogpow5ineq5  39802  aks4d1p1p4  39812  aks4d1p1p7  39815  aks4d1p1  39817  facp2  39821  fac2xp3  39882  2xp3dxp2ge1d  39884  factwoffsmonot  39885  sn-1ne2  40002  sqdeccom12  40024  235t711  40026  expgcd  40042  re1m1e0m0  40088  ipiiie0  40127  sn-0tie0  40129  fltnltalem  40202  3cubeslem3l  40211  3cubeslem3r  40212  eldioph2lem1  40285  lzenom  40295  irrapxlem1  40347  rmspecsqrtnq  40431  rmxm1  40459  rmym1  40460  2nn0ind  40470  jm2.24nn  40484  jm2.17a  40485  jm2.17b  40486  jm2.17c  40487  jm2.24  40488  acongeq  40508  jm2.18  40513  jm2.27c  40532  jm3.1lem2  40543  rngunsnply  40701  flcidc  40702  inductionexd  41442  unitadd  41484  hashnzfzclim  41613  ofdivrec  41617  lhe4.4ex1a  41620  expgrowth  41626  dvradcnv2  41638  binomcxplemrat  41641  binomcxplemnotnn0  41647  isosctrlem1ALT  42227  monoord2xrv  42699  dvsinax  43129  dvnprodlem3  43164  itgsin0pilem1  43166  itgsbtaddcnst  43198  stoweidlem13  43229  stoweidlem26  43242  stoweidlem34  43250  stoweidlem38  43254  wallispilem2  43282  wallispilem4  43284  wallispi2lem1  43287  stirlinglem1  43290  stirlinglem5  43294  stirlinglem10  43299  dirkerper  43312  dirkertrigeqlem1  43314  dirkertrigeqlem3  43316  dirkertrigeq  43317  dirkercncflem4  43322  fourierdlem24  43347  sqwvfoura  43444  sqwvfourb  43445  fourierswlem  43446  1t10e1p1e11  44475  fmtnorec3  44673  fmtno5lem4  44681  fmtno5  44682  257prm  44686  fmtno4nprmfac193  44699  m3prm  44717  139prmALT  44721  127prm  44724  m7prm  44725  lighneallem3  44732  proththd  44739  3exp4mod41  44741  41prothprmlem2  44743  perfectALTVlem2  44847  perfectALTV  44848  11t31e341  44857  evengpop3  44923  nnsum4primeseven  44925  nnsum4primesevenALTV  44926  bgoldbtbndlem1  44930  0nodd  45037  altgsumbcALT  45362  exple2lt6  45373  nn0sumshdiglemB  45639  ackval3  45702  ackval3012  45711  line2ylem  45770  onetansqsecsq  46134  cotsqcscsq  46135  5m4e1  46172