Axiom ax-1cn 11086

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

This axiom is referenced by:  0cn  11126  1cnd  11129  1ex  11130  mulrid  11132  mullid  11133  1re  11134  0re  11136  muladd11  11304  peano2cn  11306  mul02lem2  11311  addrid  11314  cnegex2  11316  peano2cnm  11448  0reALT  11479  ine0  11573  mulm1  11579  0lt1  11660  ixi  11767  muleqadd  11782  reccl  11804  recne0  11810  recid  11811  recid2  11812  diveq1  11827  div1  11832  1div1e1  11833  recdiv  11848  divdiv1  11853  divdiv2  11854  recdiv2  11855  conjmul  11859  eqneg  11862  div2neg  11865  recp1lt1  12041  recreclt  12042  recgt0ii  12049  neg1cn  12131  neg1ne0  12133  negneg1e1  12135  ofnegsub  12144  peano5nni  12149  nnsscn  12151  nn1m1nn  12167  nn1suc  12168  nnaddcl  12169  nnmulcl  12170  nnne0  12180  nnsub  12190  1m1e0  12218  2cn  12221  3cn  12227  4cn  12231  5cn  12234  6cn  12237  7cn  12240  8cn  12243  9cn  12246  1pneg1e0  12260  1m0e1  12262  0p1e1  12263  1p0e1  12265  2m1e1  12267  3m1e2  12269  4m1e3  12270  5m1e4  12271  6m1e5  12272  7m1e6  12273  8m1e7  12274  9m1e8  12275  2p2e4  12276  1p2e3  12284  1p2e3ALT  12285  3p2e5  12292  3p3e6  12293  4p2e6  12294  4p3e7  12295  4p4e8  12296  5p2e7  12297  5p3e8  12298  5p4e9  12299  6p2e8  12300  6p3e9  12301  7p2e9  12302  1t1e1  12303  3t3e9  12308  neg1mulneg1e1  12354  1mhlfehlf  12361  8th4div3  12362  halfthird  12363  halfpm6th  12364  addltmul  12378  elnn0nn  12444  elz2  12507  zlem1lt  12545  zltlem1  12546  nnaddm1cl  12551  zextlt  12568  zeo  12580  peano5uzi  12583  numsuc  12623  numltc  12635  numsucc  12649  numaddc  12657  6p5lem  12679  5p5e10  12680  6p4e10  12681  7p3e10  12684  8p2e10  12689  10m1e9  12705  4t3lem  12706  7t4e28  12720  9t11e99  12739  decbin2  12750  5recm6rec  12752  uzp1  12794  peano2uzr  12822  uzaddcl  12823  rebtwnz  12866  qbtwnre  13119  iccf1o  13417  fz01en  13473  fztp  13501  fzsuc2  13503  fztpval  13507  fseq1m1p1  13520  elfzp1b  13522  predfz  13574  fzoss2  13608  fzval3  13655  fzosplitsnm1  13661  fzo1to4tp  13675  fldiv4p1lem1div2  13757  ceim1l  13769  fldiv  13782  uzrdgxfr  13892  fzen2  13894  nn0ennn  13904  seqm1  13944  seqshft2  13953  monoord2  13958  sermono  13959  seqf1olem1  13966  seqf1olem2  13967  seqz  13975  ser1const  13983  expcl  14004  expclzlem  14008  m1expcl2  14010  expm1t  14015  1exp  14016  mulexpz  14027  expadd  14029  expaddz  14031  expmul  14032  expubnd  14103  sqrecii  14108  neg1sqe1  14121  irec  14126  i4  14129  binom21  14144  sq01  14150  crreczi  14153  bernneq  14154  bernneq2  14155  nn0opthlem1  14193  facndiv  14213  faclbnd4lem1  14218  faclbnd6  14224  bcnp1n  14239  bcm1k  14240  bcp1nk  14242  bcn2  14244  bcp1m1  14245  bcpasc  14246  hashgadd  14302  hashfz  14352  hashfzo  14354  hashxplem  14358  hashbclem  14377  hashf1  14382  seqcoll  14389  swrds1  14591  swrdlsw  14592  wrdind  14646  wrd2ind  14647  swrds2  14865  relexpaddg  14978  rei  15081  imi  15082  recan  15262  iserex  15582  isercoll2  15594  serf0  15606  iseraltlem2  15608  iseraltlem3  15609  iseralt  15610  sumrblem  15636  fsumm1  15676  telfsumo  15727  fsumparts  15731  hashiun  15747  binomlem  15754  binom  15755  binom1p  15756  binom11  15757  binom1dif  15758  bcxmas  15760  isumsplit  15765  isum1p  15766  climcndslem1  15774  supcvg  15781  harmonic  15784  arisum  15785  arisum2  15786  trireciplem  15787  geoserg  15791  geolim  15795  geolim2  15796  georeclim  15797  geo2sum  15798  geo2sum2  15799  geoisum1c  15805  0.999...  15806  geoihalfsum  15807  cvgrat  15808  mertenslem1  15809  mertenslem2  15810  mertens  15811  prodf1  15816  prodfclim1  15818  prodrblem  15854  fprodcvg  15855  prodmolem2a  15859  zprod  15862  fprodntriv  15867  prodss  15872  fprodss  15873  fprodsplit  15891  fprodn0f  15916  risefaccl  15940  fallfaccl  15941  risefacfac  15960  binomfallfac  15966  bpolycl  15977  bpolysum  15978  bpolydiflem  15979  fsumkthpow  15981  bpoly2  15982  bpoly3  15983  bpoly4  15984  fsumcube  15985  esum  16005  ege2le3  16015  efsub  16027  efexp  16028  efzval  16029  eftlub  16036  effsumlt  16038  ef4p  16040  tanval3  16061  efi4p  16064  tan0  16078  efival  16079  tanadd  16094  cos2t  16105  cos2tsin  16106  ef01bndlem  16111  cos1bnd  16114  cos2bnd  16115  demoivreALT  16128  eirrlem  16131  rpnnen2lem3  16143  rpnnen2lem11  16151  ruclem12  16168  3dvds  16260  3dvdsdec  16261  3dvds2dec  16262  odd2np1lem  16269  odd2np1  16270  opoe  16292  omoe  16293  opeo  16294  omeo  16295  n2dvdsm1  16298  m1exp1  16305  flodddiv4  16344  bitsfzo  16364  sqgcd  16491  expgcd  16492  nn0seqcvgd  16499  prmind2  16614  hashdvds  16704  phiprmpw  16705  phiprm  16706  eulerthlem2  16711  iserodd  16765  sumhash  16826  fldivp1  16827  prmpwdvds  16834  pockthlem  16835  pockthi  16837  prmreclem4  16849  prmreclem6  16851  4sqlem11  16885  4sqlem19  16893  vdwapun  16904  vdwapid1  16905  vdwlem3  16913  vdwlem5  16915  vdwlem6  16916  vdwlem8  16918  vdwlem9  16919  vdwnnlem2  16926  ramub1lem1  16956  ramub1lem2  16957  ramcl  16959  prmo1  16967  dec5nprm  16996  prmlem0  17035  43prm  17051  83prm  17052  139prm  17053  163prm  17054  317prm  17055  631prm  17056  1259lem2  17061  1259lem3  17062  1259lem4  17063  1259lem5  17064  1259prm  17065  2503lem1  17066  2503lem2  17067  2503lem3  17068  2503prm  17069  4001lem1  17070  4001lem2  17071  4001lem3  17072  4001lem4  17073  4001prm  17074  gsumsgrpccat  18732  mulgnndir  19000  mulgneg2  19005  m1expaddsub  19395  sylow1lem1  19495  sylow2a  19516  efgsval2  19630  efgsrel  19631  efgsres  19635  cncrng  21313  cnfld1  21318  cnfld1OLD  21319  zsssubrg  21350  cnmgpid  21354  zringcyg  21394  mulgrhm2  21403  pzriprng1ALT  21421  cnmsgnsubg  21502  cnmsgnbas  21503  cnmsgngrp  21504  psgninv  21507  evpmodpmf1o  21521  psdmplcl  22065  blcvx  24702  iihalf2  24844  icopnfcnv  24856  iccpnfhmeo  24859  xrhmeo  24860  icccvx  24864  lebnumii  24881  reparphti  24912  reparphtiOLD  24913  pcoass  24940  pcorevlem  24942  pcorev2  24944  pi1xfrcnv  24973  cnstrcvs  25057  cncvs  25061  ncvsm1  25070  pjthlem1  25353  divcncf  25364  ovolunlem1a  25413  ovolunlem1  25414  ovolicc2lem4  25437  uniioombllem3  25502  uniioombllem4  25503  dyadovol  25510  vitalilem4  25528  mbf0  25551  iblcnlem1  25705  itgcnlem  25707  dvid  25835  dvexp  25873  dvexp2  25874  dvexp3  25898  dveflem  25899  dvlipcn  25915  dvcvx  25941  dvfsumle  25942  dvfsumleOLD  25943  dvfsumlem1  25948  degltp1le  25994  ply1divex  26058  fta1glem1  26089  plyaddlem1  26134  plymullem1  26135  coeidp  26185  dgrid  26186  dvply1  26207  dvply2g  26208  dvply2gOLD  26209  plyremlem  26228  fta1lem  26231  vieta1lem1  26234  vieta1lem2  26235  qaa  26247  iaa  26249  aalioulem3  26258  geolim3  26263  aaliou3lem2  26267  aaliou3lem7  26273  taylply2  26291  taylply2OLD  26292  dvradcnv  26346  pserdvlem2  26354  pserdv2  26356  abelthlem1  26357  abelthlem2  26358  abelthlem6  26362  abelthlem7  26364  abelth  26367  reeff1olem  26372  reeff1o  26373  efcvx  26375  sinhalfpilem  26388  eulerid  26399  cos2pi  26401  sincosq3sgn  26425  sincosq4sgn  26426  tangtx  26430  sincos4thpi  26438  sincos6thpi  26441  pigt3  26443  pige3ALT  26445  abssinper  26446  coskpi  26448  coseq1  26450  efeq1  26453  tanregt0  26464  logneg2  26540  logdivlti  26545  logcnlem4  26570  dvlog2lem  26577  dvlog2  26578  advlog  26579  advlogexp  26580  logtayl  26585  logtayl2  26587  logccv  26588  cxpval  26589  1cxp  26597  cxpcl  26599  cxpp1  26605  cxpsqrt  26628  dvsqrt  26667  dvcnsqrt  26669  sqrtcn  26676  cxpaddlelem  26677  root1id  26680  root1cj  26682  logrec  26689  logb1  26695  logbmpt  26714  ang180lem1  26735  ang180lem2  26736  ang180lem3  26737  isosctrlem1  26744  isosctrlem2  26745  1cubrlem  26767  1cubr  26768  mcubic  26773  binom4  26776  dquartlem1  26777  quartlem1  26783  asinlem  26794  asinlem2  26795  asinlem3a  26796  asinlem3  26797  asinf  26798  atandm2  26803  atandm4  26805  atanf  26806  asinneg  26812  efiasin  26814  sinasin  26815  asinsin  26818  asin1  26820  acos1  26821  reasinsin  26822  asinbnd  26825  cosasin  26830  atanneg  26833  atancj  26836  efiatan  26838  atanlogaddlem  26839  atanlogadd  26840  atanlogsublem  26841  atanlogsub  26842  efiatan2  26843  2efiatan  26844  tanatan  26845  cosatan  26847  cosatanne0  26848  atantan  26849  atanbndlem  26851  bndatandm  26855  atans2  26857  dvatan  26861  atantayl  26863  atantayl2  26864  atantayl3  26865  leibpilem2  26867  leibpi  26868  log2cnv  26870  log2tlbnd  26871  log2ublem3  26874  log2ub  26875  birthdaylem2  26878  birthday  26880  efrlim  26895  efrlimOLD  26896  dfef2  26897  cvxcl  26911  scvxcvx  26912  emcllem2  26923  emcllem4  26925  emcllem7  26928  harmonicbnd4  26937  fsumharmonic  26938  zetacvg  26941  lgamcvg2  26981  lgam1  26990  gam1  26991  wilthlem1  26994  wilthlem2  26995  wilthlem3  26996  basellem2  27008  basellem5  27011  basellem6  27012  basellem7  27013  basellem8  27014  basellem9  27015  0sgm  27070  mule1  27074  ppiprm  27077  ppinprm  27078  chtprm  27079  chtnprm  27080  chpp1  27081  mumullem2  27106  1sgmprm  27126  1sgm2ppw  27127  ppiub  27131  chtublem  27138  chtub  27139  logfaclbnd  27149  logfacbnd3  27150  logfacrlim  27151  logexprlim  27152  mersenne  27154  perfect1  27155  perfectlem1  27156  perfectlem2  27157  perfect  27158  dchrelbasd  27166  dchrmullid  27179  dchrfi  27182  dchrsum2  27195  sumdchr2  27197  bcp1ctr  27206  bposlem8  27218  zabsle1  27223  lgslem1  27224  lgslem2  27225  lgsfcl2  27230  lgsvalmod  27243  lgsneg  27248  lgsdilem  27251  lgsdir2lem1  27252  lgsdir2lem2  27253  lgsdir2lem3  27254  lgsdir2lem5  27256  lgsdir2  27257  lgsdir  27259  lgsdi  27261  lgsne0  27262  lgseisenlem1  27302  lgseisenlem2  27303  lgseisen  27306  lgsquadlem1  27307  lgsquadlem2  27308  lgsquad2lem1  27311  lgsquad2  27313  m1lgs  27315  2lgslem3c  27325  2lgsoddprmlem3c  27339  2lgsoddprmlem3d  27340  2sqlem10  27355  2sqlem11  27356  2sqblem  27358  addsqn2reu  27368  addsqrexnreu  27369  addsqnreup  27370  chtppilimlem2  27401  chebbnd2  27404  chto1lb  27405  rplogsumlem1  27411  rpvmasumlem  27414  dchrmusumlema  27420  dchrmusum2  27421  dchrisum0flblem1  27435  rpvmasum2  27439  mudivsum  27457  mulogsum  27459  vmalogdivsum2  27465  selberg2lem  27477  logdivbnd  27483  pntrmax  27491  pntrsumo1  27492  pntrsumbnd2  27494  pntrlog2bndlem5  27508  pntpbnd1a  27512  pntpbnd2  27514  pntibndlem2  27518  pntlemd  27521  pntlemc  27522  pntlemr  27529  brbtwn2  28868  colinearalglem4  28872  ax5seglem1  28891  ax5seglem2  28892  ax5seglem3  28894  ax5seglem5  28896  ax5seglem7  28898  ax5seglem9  28900  axbtwnid  28902  axpaschlem  28903  axlowdimlem13  28917  axlowdimlem14  28918  axlowdimlem16  28920  axeuclidlem  28925  axcontlem2  28928  axcontlem4  28930  axcontlem7  28933  axcontlem8  28934  crctcshwlkn0lem6  29778  clwwlkf1  30011  clwwlknonex2lem2  30070  ex-fl  30409  ex-ind-dvds  30423  vc2OLD  30530  vc0  30536  vcm  30538  nvm1  30627  nvmtri  30633  nvge0  30635  ipval2lem3  30667  ipidsq  30672  lnoadd  30720  ip1ilem  30788  ip1i  30789  ip2i  30790  ipdirilem  30791  ipasslem1  30793  ipasslem2  30794  ipasslem10  30801  minvecolem2  30837  hvsubid  30988  hv2times  31023  hisubcomi  31066  normlem9  31080  normlem7tALT  31081  norm-ii-i  31099  normsubi  31103  hhssnv  31226  pjhthlem1  31353  h1de2bi  31516  homullid  31762  ho2times  31781  lnop0  31928  lnopaddi  31933  lnophmlem2  31979  lnfn0i  32004  lnfnaddi  32005  hst1h  32189  sto2i  32199  stadd3i  32210  addltmulALT  32408  sgnneg  32791  dpmul4  32867  psgnid  33052  cnmsgn0g  33101  altgnsg  33104  isarchi3  33139  archirngz  33141  1fldgenq  33271  ply1dg3rt0irred  33527  ccfldextdgrr  33643  constrsscn  33706  constrabscl  33744  cos9thpiminplylem1  33748  cos9thpiminplylem4  33751  cos9thpiminplylem5  33752  lmatfvlem  33781  qqhval2lem  33947  dya2ub  34237  omssubadd  34267  eulerpartlemgs2  34347  fib5  34372  fib6  34373  ballotlem2  34456  signswch  34528  signlem0  34554  itgexpif  34573  reprlt  34586  breprexp  34600  breprexpnat  34601  hgt750lem2  34619  subfacp1lem5  35156  subfacp1lem6  35157  subfacval2  35159  subfaclim  35160  subfacval3  35161  cvxsconn  35215  resconn  35218  cvmliftlem7  35263  cvmliftlem10  35266  problem4  35640  sinccvglem  35644  sqdivzi  35700  faclimlem1  35715  dnibndlem5  36455  dnibndlem10  36460  ltflcei  37587  sin2h  37589  cos2h  37590  tan2h  37591  poimirlem13  37612  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem31  37630  mblfinlem2  37637  mblfinlem3  37638  dvtan  37649  itg2addnclem3  37652  dvasin  37683  dvacos  37684  areacirc  37692  fdc  37724  mettrifi  37736  heiborlem4  37793  heiborlem6  37795  60gcd7e1  41978  lcmineqlem1  42002  lcmineqlem8  42009  lcmineqlem9  42010  lcmineqlem10  42011  lcmineqlem12  42013  3exp7  42026  3lexlogpow5ineq1  42027  3lexlogpow5ineq5  42033  aks4d1p1p4  42044  aks4d1p1p7  42047  aks4d1p1  42049  facp2  42116  1p3e4  42232  sn-1ne2  42238  sqdeccom12  42262  235t711  42278  sin2t3rdpi  42326  cos2t3rdpi  42327  re1m1e0m0  42370  ipiiie0  42411  sn-0tie0  42424  fltnltalem  42635  sum9cubes  42645  3cubeslem3l  42659  3cubeslem3r  42660  eldioph2lem1  42733  lzenom  42743  irrapxlem1  42795  rmspecsqrtnq  42879  rmxm1  42907  rmym1  42908  2nn0ind  42918  jm2.24nn  42932  jm2.17a  42933  jm2.17b  42934  jm2.17c  42935  jm2.24  42936  acongeq  42956  jm2.18  42961  jm2.27c  42980  jm3.1lem2  42991  rngunsnply  43142  flcidc  43143  inductionexd  44128  unitadd  44168  hashnzfzclim  44295  ofdivrec  44299  lhe4.4ex1a  44302  expgrowth  44308  dvradcnv2  44320  binomcxplemrat  44323  binomcxplemnotnn0  44329  isosctrlem1ALT  44907  monoord2xrv  45463  dvsinax  45895  dvnprodlem3  45930  itgsin0pilem1  45932  itgsbtaddcnst  45964  stoweidlem13  45995  stoweidlem26  46008  stoweidlem34  46016  stoweidlem38  46020  wallispilem2  46048  wallispilem4  46050  wallispi2lem1  46053  stirlinglem1  46056  stirlinglem5  46060  stirlinglem10  46065  dirkerper  46078  dirkertrigeqlem1  46080  dirkertrigeqlem3  46082  dirkertrigeq  46083  dirkercncflem4  46088  fourierdlem24  46113  sqwvfoura  46210  sqwvfourb  46211  fourierswlem  46212  lambert0  46872  lamberte  46873  cjnpoly  46874  1t10e1p1e11  47295  ceil5half3  47325  modm2nep1  47351  modm1nep2  47353  modm1nem2  47354  fmtnorec3  47533  fmtno5lem4  47541  fmtno5  47542  257prm  47546  fmtno4nprmfac193  47559  m3prm  47577  139prmALT  47581  127prm  47584  m7prm  47585  lighneallem3  47592  proththd  47599  3exp4mod41  47601  41prothprmlem2  47603  perfectALTVlem2  47707  perfectALTV  47708  11t31e341  47717  evengpop3  47783  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  bgoldbtbndlem1  47790  0nodd  48155  altgsumbcALT  48338  exple2lt6  48349  nn0sumshdiglemB  48606  ackval3  48669  ackval3012  48678  line2ylem  48737  onetansqsecsq  49747  cotsqcscsq  49748  5m4e1  49783