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

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

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 9515 . 2
2 cc 9511 . 2
31, 2wcel 1818 1
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  9609  mulid1  9614  mul02lem2  9778  mul02  9779  addid1  9781  cnegex  9782  cnegex2  9783  0cnALT  9832  negicn  9844  ine0  10017  ixi  10203  recextlem1  10204  recextlem2  10205  recex  10206  rimul  10552  cru  10553  crne0  10554  cju  10557  it0e0  10786  2mulicn  10787  2muline0  10788  cnref1o  11244  irec  12267  i2  12268  i3  12269  i4  12270  iexpcyc  12272  crreczi  12291  imre  12941  reim  12942  crre  12947  crim  12948  remim  12950  mulre  12954  cjreb  12956  recj  12957  reneg  12958  readd  12959  remullem  12961  imcj  12965  imneg  12966  imadd  12967  cjadd  12974  cjneg  12980  imval2  12984  rei  12989  imi  12990  cji  12992  cjreim  12993  cjreim2  12994  rennim  13072  cnpart  13073  sqrtneglem  13100  sqrtneg  13101  sqrtm1  13109  absi  13119  absreimsq  13125  absreim  13126  absimle  13142  abs1m  13168  sqreulem  13192  sqreu  13193  caucvgr  13498  sinf  13859  cosf  13860  tanval2  13868  tanval3  13869  resinval  13870  recosval  13871  efi4p  13872  resin4p  13873  recos4p  13874  resincl  13875  recoscl  13876  sinneg  13881  cosneg  13882  efival  13887  efmival  13888  sinhval  13889  coshval  13890  retanhcl  13894  tanhlt1  13895  tanhbnd  13896  efeul  13897  sinadd  13899  cosadd  13900  ef01bndlem  13919  sin01bnd  13920  cos01bnd  13921  absef  13932  absefib  13933  efieq1re  13934  demoivre  13935  demoivreALT  13936  nthruc  13984  igz  14452  4sqlem17  14479  cnsubrg  18478  cnrehmeo  21453  itg0  22186  itgz  22187  itgcl  22190  ibl0  22193  iblcnlem1  22194  itgcnlem  22196  itgneg  22210  iblss  22211  iblss2  22212  itgss  22218  itgeqa  22220  iblconst  22224  itgconst  22225  itgadd  22231  iblabs  22235  iblabsr  22236  iblmulc2  22237  itgmulc2  22240  itgsplit  22242  dvsincos  22382  iaa  22721  sincn  22839  coscn  22840  efhalfpi  22864  ef2kpi  22871  efper  22872  sinperlem  22873  efimpi  22884  pige3  22910  sineq0  22914  efeq1  22916  tanregt0  22926  efif1olem4  22932  efifo  22934  eff1olem  22935  circgrp  22939  circsubm  22940  logneg  22972  logm1  22973  lognegb  22974  eflogeq  22986  efiarg  22992  cosargd  22993  logimul  22999  logneg2  23000  abslogle  23003  tanarg  23004  logcn  23028  logf1o2  23031  cxpsqrtlem  23083  cxpsqrt  23084  root1eq1  23129  cxpeq  23131  ang180lem1  23141  ang180lem2  23142  ang180lem3  23143  ang180lem4  23144  1cubrlem  23172  1cubr  23173  asinlem  23199  asinlem2  23200  asinlem3a  23201  asinlem3  23202  asinf  23203  atandm2  23208  atandm3  23209  atanf  23211  asinneg  23217  efiasin  23219  sinasin  23220  asinsinlem  23222  asinsin  23223  asin1  23225  asinbnd  23230  cosasin  23235  atanneg  23238  atancj  23241  efiatan  23243  atanlogaddlem  23244  atanlogadd  23245  atanlogsublem  23246  atanlogsub  23247  efiatan2  23248  2efiatan  23249  tanatan  23250  cosatan  23252  atantan  23254  atanbndlem  23256  atans2  23262  dvatan  23266  atantayl  23268  atantayl2  23269  log2cnv  23275  basellem3  23356  2sqlem2  23639  circgrpOLD  25376  nvpi  25569  ipval2  25617  4ipval2  25618  ipval3  25619  4ipval3  25622  ipidsq  25623  dipcl  25625  dipcj  25627  dip0r  25630  dipcn  25633  sspival  25651  ip1ilem  25741  ipasslem10  25754  ipasslem11  25755  polid2i  26074  polidi  26075  lnopeq0lem1  26924  lnopeq0i  26926  lnophmlem2  26936  bhmafibid1  27632  cnre2csqima  27893  logi  29121  iexpire  29122  itgaddnc  30075  iblabsnc  30079  iblmulc2nc  30080  itgmulc2nc  30083  ftc1anclem3  30092  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  dvasin  30103  areacirclem4  30110  cntotbnd  30292  proot1ex  31161  iblsplit  31765  sinh-conventional  33133
  Copyright terms: Public domain W3C validator