Axiom ax-1cn 11282

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

This axiom is used by:  0cn  11322  1cnd  11326  1ex  11327  mulrid  11330  mullid  11331  1re  11332  0re  11334  muladd11  11504  peano2cn  11506  mul02lem2  11511  addrid  11514  cnegex2  11516  peano2cnm  11648  0reALT  11679  ine0  11775  mulm1  11781  0lt1  11862  ixi  11969  muleqadd  11984  reccl  12005  recne0  12011  recid  12012  recid2  12013  diveq1  12027  div1  12030  1div1e1  12031  recdiv  12047  divdiv1  12052  divdiv2  12053  recdiv2  12054  conjmul  12058  eqneg  12061  div2neg  12064  recp1lt1  12239  recreclt  12240  recgt0ii  12247  neg1cn  12329  neg1ne0  12331  negneg1e1  12333  ofnegsub  12342  peano5nni  12362  nnsscn  12364  nn1m1nn  12380  nn1suc  12381  nnaddcl  12382  nnmulcl  12383  nnne0  12396  nnsub  12406  1m1e0  12439  2cn  12442  3cn  12448  4cn  12452  5cn  12455  6cn  12458  7cn  12461  8cn  12464  9cn  12467  1pneg1e0  12484  1m0e1  12486  0p1e1  12487  1p0e1  12489  2m1e1  12491  2m1e1OLD  12492  3m1e2  12494  4m1e3  12495  5m1e4  12496  6m1e5  12497  7m1e6  12498  8m1e7  12499  9m1e8  12500  2p2e4  12501  1p2e3  12509  1p2e3ALT  12510  3p2e5  12517  3p3e6  12518  4p2e6  12519  4p3e7  12520  4p4e8  12521  5p2e7  12522  5p3e8  12523  5p4e9  12524  6p2e8  12525  6p3e9  12526  7p2e9  12527  1t1e1  12528  3t3e9  12534  neg1mulneg1e1  12582  1mhlfehlf  12589  8th4div3  12590  halfthird  12591  halfpm6th  12592  addltmul  12606  elnn0nn  12672  elz2  12735  zlem1lt  12772  zltlem1  12773  nnaddm1cl  12780  zextlt  12797  zeo  12809  peano5uzi  12812  numsuc  12852  numltc  12869  numsucc  12883  numaddc  12891  6p5lem  12913  5p5e10  12914  6p4e10  12915  7p3e10  12918  8p2e10  12923  10m1e9  12939  4t3lem  12940  7t4e28  12954  9t11e99OLD  12974  decbin2  12986  5recm6rec  12988  uzp1  13026  peano2uzr  13054  uzaddcl  13055  rebtwnz  13098  qbtwnre  13353  iccf1o  13651  fz01en  13710  fztp  13738  fzsuc2  13740  fztpval  13744  fseq1m1p1  13757  elfzp1b  13759  predfz  13811  fzoss2  13846  fzval3  13893  fzosplitsnm1  13899  fzo1to4tp  13913  fldiv4p1lem1div2  13999  ceim1l  14011  fldiv  14024  uzrdgxfr  14134  fzen2  14136  nn0ennn  14146  seqm1  14186  seqshft2  14195  monoord2  14200  sermono  14201  seqf1olem1  14208  seqf1olem2  14209  seqz  14217  ser1const  14225  expcl  14246  expclzlem  14250  m1expcl2  14252  expm1t  14257  1exp  14258  mulexpz  14269  expadd  14271  expaddz  14273  expmul  14274  expubnd  14345  sqrecii  14350  neg1sqe1  14363  irec  14369  i4  14372  binom21  14387  sq01  14393  crreczi  14396  bernneq  14397  bernneq2  14398  nn0opthlem1  14436  facndiv  14456  faclbnd4lem1  14461  faclbnd6  14467  bcnp1n  14482  bcm1k  14483  bcp1nk  14485  bcn2  14487  bcp1m1  14488  bcpasc  14489  hashgadd  14545  hashfz  14596  hashfzo  14598  hashxplem  14602  hashbclem  14621  hashf1  14626  seqcoll  14633  swrds1  14841  swrdlsw  14842  wrdind  14896  wrd2ind  14897  swrds2  15117  relexpaddg  15232  sgnneg  15279  rei  15349  imi  15350  recan  15530  iserex  15850  isercoll2  15862  serf0  15874  iseraltlem2  15876  iseraltlem3  15877  iseralt  15878  sumrblem  15903  fsumm1  15943  telfsumo  15995  fsumparts  15999  hashiun  16015  binomlem  16024  binom  16025  binom1p  16026  binom11  16027  binom1dif  16028  bcxmas  16030  isumsplit  16035  isum1p  16036  climcndslem1  16044  supcvg  16051  harmonic  16054  arisum  16055  trireciplem  16057  geoserg  16061  geolim  16065  geolim2  16066  georeclim  16067  geo2sum  16068  geo2sum2  16069  geoisum1c  16075  0.999...  16076  geoihalfsum  16077  cvgrat  16078  mertenslem1  16079  mertenslem2  16080  mertens  16081  prodf1  16086  prodfclim1  16088  prodrblem  16122  fprodcvg  16123  prodmolem2a  16127  zprod  16130  fprodntriv  16135  prodss  16140  fprodss  16141  fprodsplit  16159  fprodn0f  16184  risefaccl  16208  fallfaccl  16209  risefacfac  16227  binomfallfac  16233  bpolycl  16244  bpolysum  16245  bpolydiflem  16246  fsumkthpow  16248  bpoly2  16249  bpoly3  16250  bpoly4  16251  fsumcube  16252  esum  16272  ege2le3  16282  efsub  16294  efexp  16295  efzval  16296  eftlub  16303  effsumlt  16305  ef4p  16307  tanval3  16328  efi4p  16331  tan0  16345  efival  16346  tanadd  16361  cos2t  16372  cos2tsin  16373  ef01bndlem  16378  cos1bnd  16381  cos2bnd  16382  demoivreALT  16395  eirrlem  16398  rpnnen2lem3  16410  rpnnen2lem11  16418  ruclem12  16435  3dvds  16527  3dvdsdec  16528  3dvds2dec  16529  odd2np1lem  16536  odd2np1  16537  opoe  16559  omoe  16560  opeo  16561  omeo  16562  n2dvdsm1  16565  m1exp1  16572  flodddiv4  16611  bitsfzo  16631  sqgcd  16762  expgcd  16763  nn0seqcvgd  16771  prmind2  16886  hashdvds  16978  phiprmpw  16979  phiprm  16980  eulerthlem2  16985  iserodd  17039  sumhash  17100  fldivp1  17101  prmpwdvds  17108  pockthlem  17109  pockthi  17111  prmreclem4  17123  prmreclem6  17125  4sqlem11  17159  4sqlem19  17167  vdwapun  17178  vdwapid1  17179  vdwlem3  17187  vdwlem5  17189  vdwlem6  17190  vdwlem8  17192  vdwlem9  17193  vdwnnlem2  17200  ramub1lem1  17230  ramub1lem2  17231  ramcl  17233  prmo1  17241  dec5nprm  17270  prmlem0  17309  43prm  17326  83prm  17327  139prm  17328  163prm  17329  317prm  17330  631prm  17331  1259lem2  17336  1259lem3  17337  1259lem4  17338  1259lem5  17339  1259prm  17340  2503lem1  17341  2503lem2  17342  2503lem3  17343  2503prm  17344  4001lem1  17345  4001lem2  17346  4001lem3  17347  4001lem4  17348  4001prm  17349  gsumsgrpccat  19062  mulgnndir  19339  mulgneg2  19344  m1expaddsub  19739  sylow1lem1  19839  sylow2a  19860  efgsval2  19974  efgsrel  19975  efgsres  19979  cncrng  21726  cnfld1  21730  zsssubrg  21758  cnmgpid  21762  zringcyg  21802  mulgrhm2  21811  pzriprng1ALT  21829  cnmsgnsubg  21910  cnmsgnbas  21911  cnmsgngrp  21912  psgninv  21915  evpmodpmf1o  21929  psdmplcl  22510  blcvx  25144  iihalf2  25281  icopnfcnv  25290  iccpnfhmeo  25293  xrhmeo  25294  icccvx  25298  lebnumii  25314  reparphti  25345  pcoass  25372  pcorevlem  25374  pcorev2  25376  pi1xfrcnv  25405  cnstrcvs  25489  cncvs  25493  ncvsm1  25502  pjthlem1  25785  divcncf  25795  ovolunlem1a  25844  ovolunlem1  25845  ovolicc2lem4  25868  uniioombllem3  25933  uniioombllem4  25934  dyadovol  25941  vitalilem4  25959  mbf0  25982  iblcnlem1  26135  itgcnlem  26137  dvid  26265  dvexp  26300  dvexp2  26301  dvexp3  26325  dveflem  26326  dvlipcn  26341  dvcvx  26367  dvfsumle  26368  dvfsumlem1  26373  degltp1le  26418  ply1divex  26482  fta1glem1  26513  plyaddlem1  26559  plymullem1  26560  coeidp  26609  dgrid  26610  dvply1  26632  dvply2g  26633  plyremlem  26652  fta1lem  26655  vieta1lem1  26660  vieta1lem2  26661  qaa  26674  iaa  26678  iaaOLD  26679  aalioulem3  26688  geolim3  26693  aaliou3lem2  26697  aaliou3lem7  26703  taylply2  26722  dvradcnv  26775  pserdvlem2  26782  pserdv2  26784  abelthlem1  26785  abelthlem2  26786  abelthlem6  26790  abelthlem7  26792  abelth  26795  reeff1olem  26800  reeff1o  26801  efcvx  26803  sinhalfpilem  26819  eulerid  26830  cos2pi  26832  sincosq3sgn  26856  sincosq4sgn  26857  tangtx  26861  sincos4thpi  26869  sincos6thpi  26871  pigt3  26873  pige3ALT  26875  abssinper  26876  coskpi  26878  coseq1  26880  efeq1  26883  tanregt0  26894  logneg2  26970  logdivlti  26975  logcnlem4  27000  dvlog2lem  27007  dvlog2  27008  advlog  27009  advlogexp  27010  logtayl  27015  logtayl2  27017  logccv  27018  cxpval  27019  1cxp  27027  cxpcl  27029  cxpp1  27035  cxpsqrt  27058  dvsqrt  27097  dvcnsqrt  27099  sqrtcn  27105  cxpaddlelem  27106  root1id  27109  root1cj  27111  logrec  27118  logb1  27124  logbmpt  27143  ang180lem1  27164  ang180lem2  27165  ang180lem3  27166  isosctrlem1  27173  isosctrlem2  27174  1cubrlem  27196  1cubr  27197  mcubic  27202  binom4  27205  dquartlem1  27206  quartlem1  27212  asinlem  27223  asinlem2  27224  asinlem3a  27225  asinlem3  27226  asinf  27227  atandm2  27232  atandm4  27234  atanf  27235  asinneg  27241  efiasin  27243  sinasin  27244  asinsin  27247  asin1  27249  acos1  27250  reasinsin  27251  asinbnd  27254  cosasin  27259  atanneg  27262  atancj  27265  efiatan  27267  atanlogaddlem  27268  atanlogadd  27269  atanlogsublem  27270  atanlogsub  27271  efiatan2  27272  2efiatan  27273  tanatan  27274  cosatan  27276  cosatanne0  27277  atantan  27278  atanbndlem  27280  bndatandm  27284  atans2  27286  dvatan  27290  atantayl  27292  atantayl2  27293  atantayl3  27294  leibpilem2  27296  leibpi  27297  log2cnv  27299  log2tlbnd  27300  log2ublem3  27303  log2ub  27304  birthdaylem2  27307  birthday  27309  efrlim  27324  dfef2  27325  cvxcl  27339  scvxcvx  27340  emcllem2  27351  emcllem4  27353  emcllem7  27356  harmonicbnd4  27365  fsumharmonic  27366  zetacvg  27369  lgamcvg2  27409  lgam1  27418  gam1  27419  wilthlem1  27422  wilthlem2  27423  wilthlem3  27424  basellem2  27436  basellem5  27439  basellem6  27440  basellem7  27441  basellem8  27442  basellem9  27443  0sgm  27498  mule1  27502  ppiprm  27505  ppinprm  27506  chtprm  27507  chtnprm  27508  chpp1  27509  mumullem2  27534  1sgmprm  27553  1sgm2ppw  27554  ppiub  27558  chtublem  27565  chtub  27566  logfaclbnd  27576  logfacbnd3  27577  logfacrlim  27578  logexprlim  27579  mersenne  27581  perfect1  27582  perfectlem1  27583  perfectlem2  27584  perfect  27585  dchrelbasd  27593  dchrmullid  27606  dchrfi  27609  dchrsum2  27622  sumdchr2  27624  bcp1ctr  27633  bposlem8  27645  zabsle1  27650  lgslem1  27651  lgslem2  27652  lgsfcl2  27657  lgsvalmod  27670  lgsneg  27675  lgsdilem  27678  lgsdir2lem1  27679  lgsdir2lem2  27680  lgsdir2lem3  27681  lgsdir2lem5  27683  lgsdir2  27684  lgsdir  27686  lgsdi  27688  lgsne0  27689  lgseisenlem1  27729  lgseisenlem2  27730  lgseisen  27733  lgsquadlem1  27734  lgsquadlem2  27735  lgsquad2lem1  27738  lgsquad2  27740  m1lgs  27742  2lgslem3c  27752  2lgsoddprmlem3c  27766  2lgsoddprmlem3d  27767  2sqlem10  27782  2sqlem11  27783  2sqblem  27785  addsqn2reu  27795  addsqrexnreu  27796  addsqnreup  27797  chtppilimlem2  27828  chebbnd2  27831  chto1lb  27832  rplogsumlem1  27838  rpvmasumlem  27841  dchrmusumlema  27847  dchrmusum2  27848  dchrisum0flblem1  27862  rpvmasum2  27866  mudivsum  27884  mulogsum  27886  vmalogdivsum2  27892  selberg2lem  27904  logdivbnd  27910  pntrmax  27918  pntrsumo1  27919  pntrsumbnd2  27921  pntrlog2bndlem5  27935  pntpbnd1a  27939  pntpbnd2  27941  pntibndlem2  27945  pntlemd  27948  pntlemc  27949  pntlemr  27956  brbtwn2  29510  colinearalglem4  29514  ax5seglem1  29533  ax5seglem2  29534  ax5seglem3  29536  ax5seglem5  29538  ax5seglem7  29540  ax5seglem9  29542  axbtwnid  29544  axpaschlem  29545  axlowdimlem13  29559  axlowdimlem14  29560  axlowdimlem16  29562  axeuclidlem  29567  axcontlem2  29570  axcontlem4  29572  axcontlem7  29575  axcontlem8  29576  crctcshwlkn0lem6  30431  clwwlkf1  30667  clwwlknonex2lem2  30726  ex-fl  31075  ex-ind-dvds  31089  vc2OLD  31197  vc0  31203  vcm  31205  nvm1  31294  nvmtri  31300  nvge0  31302  ipval2lem3  31334  ipidsq  31339  lnoadd  31387  ip1ilem  31455  ip1i  31456  ip2i  31457  ipdirilem  31458  ipasslem1  31460  ipasslem2  31461  ipasslem10  31468  minvecolem2  31504  hvsubid  31655  hv2times  31690  hisubcomi  31733  normlem9  31747  normlem7tALT  31748  norm-ii-i  31766  normsubi  31770  hhssnv  31893  pjhthlem1  32020  h1de2bi  32183  homullid  32429  ho2times  32448  lnop0  32595  lnopaddi  32600  lnophmlem2  32646  lnfn0i  32671  lnfnaddi  32672  hst1h  32856  sto2i  32866  stadd3i  32877  addltmulALT  33117  dpmul4  33547  psgnid  33725  cnmsgn0g  33774  altgnsg  33777  isarchi3  33815  archirngz  33817  1fldgenq  33951  ply1dg3rt0irred  34183  esplyfvaln  34273  ccfldextdgrr  34371  constrsscn  34439  constrabscl  34477  cos9thpiminplylem1  34481  cos9thpiminplylem4  34484  cos9thpiminplylem5  34485  lmatfvlem  34514  qqhval2lem  34680  dya2ub  34969  omssubadd  34999  eulerpartlemgs2  35079  fib5  35104  fib6  35105  ballotlem2  35188  signswch  35257  signlem0  35283  itgexpif  35302  reprlt  35315  breprexp  35329  breprexpnat  35330  hgt750lem2  35348  subfacp1lem5  36115  subfacp1lem6  36116  subfacval2  36118  subfaclim  36119  subfacval3  36120  cvxsconn  36174  resconn  36177  cvmliftlem7  36222  cvmliftlem10  36225  problem4  36599  sinccvglem  36603  sqdivzi  36670  faclimlem1  36685  dnibndlem5  37525  dnibndlem10  37530  ltflcei  38722  sin2h  38724  cos2h  38725  tan2h  38726  poimirlem13  38742  poimirlem16  38745  poimirlem17  38746  poimirlem19  38748  poimirlem20  38749  poimirlem31  38760  mblfinlem2  38767  mblfinlem3  38768  dvtan  38779  itg2addnclem3  38782  dvasin  38813  dvacos  38814  areacirc  38822  fdc  38870  mettrifi  38882  heiborlem4  38939  heiborlem6  38941  60gcd7e1  43246  lcmineqlem1  43270  lcmineqlem8  43277  lcmineqlem9  43278  lcmineqlem10  43279  lcmineqlem12  43281  3exp7  43294  3lexlogpow5ineq1  43295  3lexlogpow5ineq5  43301  aks4d1p1p4  43312  aks4d1p1p7  43315  aks4d1p1  43317  facp2  43384  25or6to4  43447  1p3e4  43501  1p4e5  43502  1p5e6  43503  1p6e7  43504  1p7e8  43505  1p8e9  43506  2p3e5  43507  4p5e9  43515  sn-1ne2  43521  sqdeccom12  43537  235t711  43553  sin2t3rdpi  43595  cos2t3rdpi  43596  re1m1e0m0  43639  ipiiie0  43680  sn-0tie0  43706  fltnltalem  43864  sum9cubes  43874  3cubeslem3l  43887  3cubeslem3r  43888  eldioph2lem1  43962  lzenom  43972  irrapxlem1  44020  rmspecsqrtnq  44104  rmxm1  44132  rmym1  44133  2nn0ind  44143  jm2.24nn  44157  jm2.17a  44158  jm2.17b  44159  jm2.17c  44160  jm2.24  44161  acongeq  44181  jm2.18  44186  jm2.27c  44205  jm3.1lem2  44216  rngunsnply  44361  flcidc  44362  inductionexd  45345  unitadd  45385  hashnzfzclim  45496  ofdivrec  45500  lhe4.4ex1a  45503  expgrowth  45509  dvradcnv2  45521  binomcxplemrat  45524  binomcxplemnotnn0  45530  isosctrlem1ALT  46105  monoord2xrv  46696  dvsinax  47126  dvnprodlem3  47161  itgsin0pilem1  47163  itgsbtaddcnst  47195  stoweidlem13  47226  stoweidlem26  47239  stoweidlem34  47247  stoweidlem38  47251  wallispilem2  47279  wallispilem4  47281  wallispi2lem1  47284  stirlinglem1  47287  stirlinglem5  47291  stirlinglem10  47296  dirkerper  47309  dirkertrigeqlem1  47311  dirkertrigeqlem3  47313  dirkertrigeq  47314  dirkercncflem4  47319  fourierdlem24  47344  sqwvfoura  47441  sqwvfourb  47442  fourierswlem  47443  cos5t  48128  goldpolyfactor  48130  goldratmolem2  48136  goldratmolem4  48138  goldratval  48139  lambert0  48140  lamberte  48141  cjnpoly  48142  sqrtnpoly  48146  1t10e1p1e11  48583  ceil5half3  48619  modm2nep1  48645  modm1nep2  48647  modm1nem2  48648  fmtnorec3  48836  fmtno5lem4  48844  fmtno5  48845  257prm  48849  fmtno4nprmfac193  48862  m3prm  48880  139prmALT  48884  127prm  48887  m7prm  48888  lighneallem3  48895  proththd  48902  3exp4mod41  48904  41prothprmlem2  48906  perfectALTVlem2  49023  perfectALTV  49024  11t31e341  49033  evengpop3  49099  nnsum4primeseven  49101  nnsum4primesevenALTV  49102  bgoldbtbndlem1  49106  0nodd  49470  altgsumbcALT  49668  exple2lt6  49679  nn0sumshdiglemB  49935  ackval3  49998  ackval3012  50007  line2ylem  50066  onetansqsecsq  51132  cotsqcscsq  51133  dvsec  51134  dvcsc  51135  dvcot  51136  5m4e1  51213