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

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

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 10528 . 2 class i
2 cc 10524 . 2 class
31, 2wcel 2105 1 wff i ∈ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  10622  mulid1  10628  mul02lem2  10806  mul02  10807  addid1  10809  cnegex  10810  cnegex2  10811  0cnALT  10863  0cnALT2  10864  negicn  10876  ine0  11064  ixi  11258  recextlem1  11259  recextlem2  11260  recex  11261  rimul  11618  cru  11619  crne0  11620  cju  11623  it0e0  11848  2mulicn  11849  2muline0  11850  cnref1o  12374  irec  13554  i2  13555  i3  13556  i4  13557  iexpcyc  13559  crreczi  13579  imre  14457  reim  14458  crre  14463  crim  14464  remim  14466  mulre  14470  cjreb  14472  recj  14473  reneg  14474  readd  14475  remullem  14477  imcj  14481  imneg  14482  imadd  14483  cjadd  14490  cjneg  14496  imval2  14500  rei  14505  imi  14506  cji  14508  cjreim  14509  cjreim2  14510  rennim  14588  cnpart  14589  sqrtneglem  14616  sqrtneg  14617  sqrtm1  14625  absi  14636  absreimsq  14642  absreim  14643  absimle  14659  abs1m  14685  sqreulem  14709  sqreu  14710  bhmafibid1  14815  caucvgr  15022  sinf  15467  cosf  15468  tanval2  15476  tanval3  15477  resinval  15478  recosval  15479  efi4p  15480  resin4p  15481  recos4p  15482  resincl  15483  recoscl  15484  sinneg  15489  cosneg  15490  efival  15495  efmival  15496  sinhval  15497  coshval  15498  retanhcl  15502  tanhlt1  15503  tanhbnd  15504  efeul  15505  sinadd  15507  cosadd  15508  ef01bndlem  15527  sin01bnd  15528  cos01bnd  15529  absef  15540  absefib  15541  efieq1re  15542  demoivre  15543  demoivreALT  15544  nthruc  15595  igz  16260  4sqlem17  16287  cnsubrg  20535  cnrehmeo  23486  cmodscexp  23654  ncvspi  23689  cphipval2  23773  4cphipval2  23774  cphipval  23775  itg0  24309  itgz  24310  itgcl  24313  ibl0  24316  iblcnlem1  24317  itgcnlem  24319  itgneg  24333  iblss  24334  iblss2  24335  itgss  24341  itgeqa  24343  iblconst  24347  itgconst  24348  itgadd  24354  iblabs  24358  iblabsr  24359  iblmulc2  24360  itgmulc2  24363  itgsplit  24365  dvsincos  24507  iaa  24843  sincn  24961  coscn  24962  efhalfpi  24986  ef2kpi  24993  efper  24994  sinperlem  24995  efimpi  25006  pige3ALT  25034  sineq0  25038  efeq1  25040  tanregt0  25050  efif1olem4  25056  efifo  25058  eff1olem  25059  circgrp  25063  circsubm  25064  logneg  25098  logm1  25099  lognegb  25100  eflogeq  25112  efiarg  25117  cosargd  25118  logimul  25124  logneg2  25125  abslogle  25128  tanarg  25129  logcn  25157  logf1o2  25160  cxpsqrtlem  25212  cxpsqrt  25213  root1eq1  25263  cxpeq  25265  ang180lem1  25314  ang180lem2  25315  ang180lem3  25316  ang180lem4  25317  1cubrlem  25346  1cubr  25347  asinlem  25373  asinlem2  25374  asinlem3a  25375  asinlem3  25376  asinf  25377  atandm2  25382  atandm3  25383  atanf  25385  asinneg  25391  efiasin  25393  sinasin  25394  asinsinlem  25396  asinsin  25397  asin1  25399  asinbnd  25404  cosasin  25409  atanneg  25412  atancj  25415  efiatan  25417  atanlogaddlem  25418  atanlogadd  25419  atanlogsublem  25420  atanlogsub  25421  efiatan2  25422  2efiatan  25423  tanatan  25424  cosatan  25426  atantan  25428  atanbndlem  25430  atans2  25436  dvatan  25440  atantayl  25442  atantayl2  25443  log2cnv  25450  basellem3  25588  2sqlem2  25922  nvpi  28372  ipval2  28412  4ipval2  28413  ipval3  28414  ipidsq  28415  dipcl  28417  dipcj  28419  dip0r  28422  dipcn  28425  ip1ilem  28531  ipasslem10  28544  ipasslem11  28545  polid2i  28862  polidi  28863  lnopeq0lem1  29710  lnopeq0i  29712  lnophmlem2  29722  ccfldextdgrr  30957  cnre2csqima  31054  efmul2picn  31767  itgexpif  31777  vtscl  31809  vtsprod  31810  circlemeth  31811  logi  32864  iexpire  32865  itgaddnc  34834  iblabsnc  34838  iblmulc2nc  34839  itgmulc2nc  34842  ftc1anclem3  34851  ftc1anclem6  34854  ftc1anclem7  34855  ftc1anclem8  34856  ftc1anc  34857  dvasin  34860  areacirclem4  34867  cntotbnd  34957  sn-1ne2  39038  re1m1e0m0  39107  sn-addid2  39114  proot1ex  39681  sineq0ALT  41151  iblsplit  42131  sqrtnegnre  43388  requad01  43633  sinh-conventional  44736
  Copyright terms: Public domain W3C validator