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

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

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 9369 . 2
2 cc 9365 . 2
31, 2wcel 1757 1
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  9463  mulid1  9468  mul02lem2  9631  mul02  9632  addid1  9634  cnegex  9635  cnegex2  9636  0cnALT  9684  negicn  9696  ine0  9865  ixi  10050  recextlem1  10051  recextlem2  10052  recex  10053  rimul  10398  cru  10399  crne0  10400  cju  10403  it0e0  10632  2mulicn  10633  2muline0  10634  cnref1o  11071  irec  12050  i2  12051  i3  12052  i4  12053  iexpcyc  12055  crreczi  12074  imre  12683  reim  12684  crre  12689  crim  12690  remim  12692  mulre  12696  cjreb  12698  recj  12699  reneg  12700  readd  12701  remullem  12703  imcj  12707  imneg  12708  imadd  12709  cjadd  12716  cjneg  12722  imval2  12726  rei  12731  imi  12732  cji  12734  cjreim  12735  cjreim2  12736  rennim  12814  cnpart  12815  sqrneglem  12842  sqrneg  12843  sqrm1  12851  absi  12861  absreimsq  12867  absreim  12868  absimle  12884  abs1m  12909  sqreulem  12933  sqreu  12934  caucvgr  13239  sinf  13494  cosf  13495  tanval2  13503  tanval3  13504  resinval  13505  recosval  13506  efi4p  13507  resin4p  13508  recos4p  13509  resincl  13510  recoscl  13511  sinneg  13516  cosneg  13517  efival  13522  efmival  13523  sinhval  13524  coshval  13525  retanhcl  13529  tanhlt1  13530  tanhbnd  13531  efeul  13532  sinadd  13534  cosadd  13535  ef01bndlem  13554  sin01bnd  13555  cos01bnd  13556  absef  13567  absefib  13568  efieq1re  13569  demoivre  13570  demoivreALT  13571  nthruc  13619  igz  14081  4sqlem17  14108  cnsubrg  17966  cnrehmeo  20625  itg0  21357  itgz  21358  itgcl  21361  ibl0  21364  iblcnlem1  21365  itgcnlem  21367  itgneg  21381  iblss  21382  iblss2  21383  itgss  21389  itgeqa  21391  iblconst  21395  itgconst  21396  itgadd  21402  iblabs  21406  iblabsr  21407  iblmulc2  21408  itgmulc2  21411  itgsplit  21413  dvsincos  21553  iaa  21891  sincn  22009  coscn  22010  efhalfpi  22033  ef2kpi  22040  efper  22041  sinperlem  22042  efimpi  22053  pige3  22079  sineq0  22083  efeq1  22085  tanregt0  22095  efif1olem4  22101  efifo  22103  eff1olem  22104  logneg  22136  logm1  22137  lognegb  22138  eflogeq  22150  efiarg  22156  cosargd  22157  logimul  22163  logneg2  22164  abslogle  22167  tanarg  22168  logcn  22192  logf1o2  22195  cxpsqrlem  22247  cxpsqr  22248  root1eq1  22293  cxpeq  22295  ang180lem1  22305  ang180lem2  22306  ang180lem3  22307  ang180lem4  22308  1cubrlem  22336  1cubr  22337  asinlem  22363  asinlem2  22364  asinlem3a  22365  asinlem3  22366  asinf  22367  atandm2  22372  atandm3  22373  atanf  22375  asinneg  22381  efiasin  22383  sinasin  22384  asinsinlem  22386  asinsin  22387  asin1  22389  asinbnd  22394  cosasin  22399  atanneg  22402  atancj  22405  efiatan  22407  atanlogaddlem  22408  atanlogadd  22409  atanlogsublem  22410  atanlogsub  22411  efiatan2  22412  2efiatan  22413  tanatan  22414  cosatan  22416  atantan  22418  atanbndlem  22420  atans2  22426  dvatan  22430  atantayl  22432  atantayl2  22433  log2cnv  22439  basellem3  22520  2sqlem2  22803  circgrp  23980  nvpi  24173  ipval2  24221  4ipval2  24222  ipval3  24223  4ipval3  24226  ipidsq  24227  dipcl  24229  dipcj  24231  dip0r  24234  dipcn  24237  sspival  24255  ip1ilem  24345  ipasslem10  24358  ipasslem11  24359  polid2i  24678  polidi  24679  lnopeq0lem1  25528  lnopeq0i  25530  lnophmlem2  25540  cnre2csqima  26459  itgaddnc  28574  iblabsnc  28578  iblmulc2nc  28579  itgmulc2nc  28582  ftc1anclem3  28591  ftc1anclem6  28594  ftc1anclem7  28595  ftc1anclem8  28596  ftc1anc  28597  dvasin  28602  areacirclem4  28609  cntotbnd  28817  proot1ex  29691  sinh-conventional  31355
  Copyright terms: Public domain W3C validator