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

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

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 8739 . 2  class  _i
2 cc 8735 . 2  class  CC
31, 2wcel 1684 1  wff  _i  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  8831  mulid1  8835  mul02lem2  8989  mul02  8990  addid1  8992  cnegex  8993  cnegex2  8994  0cnALT  9041  ine0  9215  ixi  9397  recextlem1  9398  recextlem2  9399  recex  9400  rimul  9737  cru  9738  crne0  9739  cju  9742  cnref1o  10349  irec  11202  i2  11203  i3  11204  i4  11205  iexpcyc  11207  crreczi  11226  imre  11593  reim  11594  imcl  11596  crre  11599  crim  11600  remim  11602  reim0  11603  reim0b  11604  rereb  11605  mulre  11606  cjreb  11608  recj  11609  reneg  11610  readd  11611  remullem  11613  imcj  11617  imneg  11618  imadd  11619  cjadd  11626  cjneg  11632  imval2  11636  rei  11641  imi  11642  cji  11644  cjreim  11645  cjreim2  11646  rennim  11724  cnpart  11725  sqrneglem  11752  sqrneg  11753  sqrm1  11761  absi  11771  absreimsq  11777  absreim  11778  absimle  11794  abs1m  11819  recan  11820  sqreulem  11843  sqreu  11844  caucvgr  12148  sinf  12404  cosf  12405  tanval2  12413  tanval3  12414  resinval  12415  recosval  12416  efi4p  12417  resin4p  12418  recos4p  12419  resincl  12420  recoscl  12421  sinneg  12426  cosneg  12427  cos0  12430  efival  12432  efmival  12433  sinhval  12434  coshval  12435  retanhcl  12439  tanhlt1  12440  tanhbnd  12441  efeul  12442  sinadd  12444  cosadd  12445  ef01bndlem  12464  sin01bnd  12465  cos01bnd  12466  absef  12477  absefib  12478  efieq1re  12479  demoivre  12480  demoivreALT  12481  nthruc  12529  igz  12981  4sqlem17  13008  cnsubrg  16432  cnrehmeo  18451  itg0  19134  itgz  19135  itgcl  19138  ibl0  19141  iblcnlem1  19142  itgcnlem  19144  itgrevallem1  19149  itgneg  19158  iblss  19159  iblss2  19160  itgss  19166  itgeqa  19168  iblconst  19172  itgconst  19173  itgadd  19179  iblabs  19183  iblabsr  19184  iblmulc2  19185  itgmulc2  19188  itgsplit  19190  dvmptim  19319  dvsincos  19328  iaa  19705  sincn  19820  coscn  19821  efhalfpi  19839  efipi  19841  ef2pi  19845  ef2kpi  19846  efper  19847  sinperlem  19848  efimpi  19859  pige3  19885  sineq0  19889  efeq1  19891  tanregt0  19901  efif1olem4  19907  efifo  19909  eff1olem  19910  logneg  19941  logm1  19942  lognegb  19943  eflogeq  19955  efiarg  19961  cosargd  19962  logimul  19968  logneg2  19969  tanarg  19970  logcn  19994  logf1o2  19997  cxpsqrlem  20049  cxpsqr  20050  root1eq1  20095  cxpeq  20097  ang180lem1  20107  ang180lem2  20108  ang180lem3  20109  ang180lem4  20110  1cubrlem  20137  1cubr  20138  asinlem  20164  asinlem2  20165  asinlem3a  20166  asinlem3  20167  asinf  20168  atandm2  20173  atandm3  20174  atanf  20176  asinneg  20182  efiasin  20184  sinasin  20185  asinsinlem  20187  asinsin  20188  asin1  20190  asinbnd  20195  cosasin  20200  atanneg  20203  atancj  20206  efiatan  20208  atanlogaddlem  20209  atanlogadd  20210  atanlogsublem  20211  atanlogsub  20212  efiatan2  20213  2efiatan  20214  tanatan  20215  cosatan  20217  atantan  20219  atanbndlem  20221  atans2  20227  dvatan  20231  atantayl  20233  atantayl2  20234  log2cnv  20240  basellem3  20320  2sqlem2  20603  circgrp  21041  nvpi  21232  ipval2  21280  4ipval2  21281  ipval3  21282  4ipval3  21285  ipidsq  21286  dipcl  21288  dipcj  21290  dip0r  21293  dipcn  21296  sspival  21314  ip1ilem  21404  ipasslem10  21417  ipasslem11  21418  polid2i  21736  polidi  21737  lnopeq0lem1  22585  lnopeq0i  22587  lnophmlem2  22597  cnre2csqima  23295  dvreasin  24923  areacirclem5  24929  cnegvex2  25660  cntotbnd  26520  proot1ex  27520  sinh-conventional  28209
  Copyright terms: Public domain W3C validator