MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-icn Unicode version

Axiom ax-icn 9287
Description: is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 9263. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-icn

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 9230 . 2
2 cc 9226 . 2
31, 2wcel 1749 1
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  9324  mulid1  9329  mul02lem2  9492  mul02  9493  addid1  9495  cnegex  9496  cnegex2  9497  0cnALT  9545  negicn  9557  ine0  9726  ixi  9911  recextlem1  9912  recextlem2  9913  recex  9914  rimul  10259  cru  10260  crne0  10261  cju  10264  it0e0  10493  2mulicn  10494  2muline0  10495  cnref1o  10931  irec  11906  i2  11907  i3  11908  i4  11909  iexpcyc  11911  crreczi  11930  imre  12538  reim  12539  crre  12544  crim  12545  remim  12547  mulre  12551  cjreb  12553  recj  12554  reneg  12555  readd  12556  remullem  12558  imcj  12562  imneg  12563  imadd  12564  cjadd  12571  cjneg  12577  imval2  12581  rei  12586  imi  12587  cji  12589  cjreim  12590  cjreim2  12591  rennim  12669  cnpart  12670  sqrneglem  12697  sqrneg  12698  sqrm1  12706  absi  12716  absreimsq  12722  absreim  12723  absimle  12739  abs1m  12764  sqreulem  12788  sqreu  12789  caucvgr  13094  sinf  13348  cosf  13349  tanval2  13357  tanval3  13358  resinval  13359  recosval  13360  efi4p  13361  resin4p  13362  recos4p  13363  resincl  13364  recoscl  13365  sinneg  13370  cosneg  13371  efival  13376  efmival  13377  sinhval  13378  coshval  13379  retanhcl  13383  tanhlt1  13384  tanhbnd  13385  efeul  13386  sinadd  13388  cosadd  13389  ef01bndlem  13408  sin01bnd  13409  cos01bnd  13410  absef  13421  absefib  13422  efieq1re  13423  demoivre  13424  demoivreALT  13425  nthruc  13473  igz  13935  4sqlem17  13962  cnsubrg  17583  cnrehmeo  20225  itg0  20957  itgz  20958  itgcl  20961  ibl0  20964  iblcnlem1  20965  itgcnlem  20967  itgneg  20981  iblss  20982  iblss2  20983  itgss  20989  itgeqa  20991  iblconst  20995  itgconst  20996  itgadd  21002  iblabs  21006  iblabsr  21007  iblmulc2  21008  itgmulc2  21011  itgsplit  21013  dvsincos  21153  iaa  21532  sincn  21650  coscn  21651  efhalfpi  21674  ef2kpi  21681  efper  21682  sinperlem  21683  efimpi  21694  pige3  21720  sineq0  21724  efeq1  21726  tanregt0  21736  efif1olem4  21742  efifo  21744  eff1olem  21745  logneg  21777  logm1  21778  lognegb  21779  eflogeq  21791  efiarg  21797  cosargd  21798  logimul  21804  logneg2  21805  abslogle  21808  tanarg  21809  logcn  21833  logf1o2  21836  cxpsqrlem  21888  cxpsqr  21889  root1eq1  21934  cxpeq  21936  ang180lem1  21946  ang180lem2  21947  ang180lem3  21948  ang180lem4  21949  1cubrlem  21977  1cubr  21978  asinlem  22004  asinlem2  22005  asinlem3a  22006  asinlem3  22007  asinf  22008  atandm2  22013  atandm3  22014  atanf  22016  asinneg  22022  efiasin  22024  sinasin  22025  asinsinlem  22027  asinsin  22028  asin1  22030  asinbnd  22035  cosasin  22040  atanneg  22043  atancj  22046  efiatan  22048  atanlogaddlem  22049  atanlogadd  22050  atanlogsublem  22051  atanlogsub  22052  efiatan2  22053  2efiatan  22054  tanatan  22055  cosatan  22057  atantan  22059  atanbndlem  22061  atans2  22067  dvatan  22071  atantayl  22073  atantayl2  22074  log2cnv  22080  basellem3  22161  2sqlem2  22444  circgrp  23540  nvpi  23733  ipval2  23781  4ipval2  23782  ipval3  23783  4ipval3  23786  ipidsq  23787  dipcl  23789  dipcj  23791  dip0r  23794  dipcn  23797  sspival  23815  ip1ilem  23905  ipasslem10  23918  ipasslem11  23919  polid2i  24238  polidi  24239  lnopeq0lem1  25088  lnopeq0i  25090  lnophmlem2  25100  cnre2csqima  26050  itgaddnc  28123  iblabsnc  28127  iblmulc2nc  28128  itgmulc2nc  28131  ftc1anclem3  28140  ftc1anclem6  28143  ftc1anclem7  28144  ftc1anclem8  28145  ftc1anc  28146  dvasin  28151  areacirclem4  28158  cntotbnd  28366  proot1ex  29242  sinh-conventional  30658
  Copyright terms: Public domain W3C validator