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 10590
Description: i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 10566. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-icn i ∈ ℂ

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 10533 . 2 class i
2 cc 10529 . 2 class
31, 2wcel 2107 1 wff i ∈ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  10627  mulid1  10633  mul02lem2  10811  mul02  10812  addid1  10814  cnegex  10815  cnegex2  10816  0cnALT  10868  0cnALT2  10869  negicn  10881  ine0  11069  ixi  11263  recextlem1  11264  recextlem2  11265  recex  11266  rimul  11623  cru  11624  crne0  11625  cju  11628  it0e0  11853  2mulicn  11854  2muline0  11855  cnref1o  12379  irec  13559  i2  13560  i3  13561  i4  13562  iexpcyc  13564  crreczi  13584  imre  14462  reim  14463  crre  14468  crim  14469  remim  14471  mulre  14475  cjreb  14477  recj  14478  reneg  14479  readd  14480  remullem  14482  imcj  14486  imneg  14487  imadd  14488  cjadd  14495  cjneg  14501  imval2  14505  rei  14510  imi  14511  cji  14513  cjreim  14514  cjreim2  14515  rennim  14593  cnpart  14594  sqrtneglem  14621  sqrtneg  14622  sqrtm1  14630  absi  14641  absreimsq  14647  absreim  14648  absimle  14664  abs1m  14690  sqreulem  14714  sqreu  14715  bhmafibid1  14820  caucvgr  15027  sinf  15472  cosf  15473  tanval2  15481  tanval3  15482  resinval  15483  recosval  15484  efi4p  15485  resin4p  15486  recos4p  15487  resincl  15488  recoscl  15489  sinneg  15494  cosneg  15495  efival  15500  efmival  15501  sinhval  15502  coshval  15503  retanhcl  15507  tanhlt1  15508  tanhbnd  15509  efeul  15510  sinadd  15512  cosadd  15513  ef01bndlem  15532  sin01bnd  15533  cos01bnd  15534  absef  15545  absefib  15546  efieq1re  15547  demoivre  15548  demoivreALT  15549  nthruc  15600  igz  16265  4sqlem17  16292  cnsubrg  20540  cnrehmeo  23491  cmodscexp  23659  ncvspi  23694  cphipval2  23778  4cphipval2  23779  cphipval  23780  itg0  24314  itgz  24315  itgcl  24318  ibl0  24321  iblcnlem1  24322  itgcnlem  24324  itgneg  24338  iblss  24339  iblss2  24340  itgss  24346  itgeqa  24348  iblconst  24352  itgconst  24353  itgadd  24359  iblabs  24363  iblabsr  24364  iblmulc2  24365  itgmulc2  24368  itgsplit  24370  dvsincos  24512  iaa  24848  sincn  24966  coscn  24967  efhalfpi  24991  ef2kpi  24998  efper  24999  sinperlem  25000  efimpi  25011  pige3ALT  25039  sineq0  25043  efeq1  25045  tanregt0  25055  efif1olem4  25061  efifo  25063  eff1olem  25064  circgrp  25068  circsubm  25069  logneg  25103  logm1  25104  lognegb  25105  eflogeq  25117  efiarg  25122  cosargd  25123  logimul  25129  logneg2  25130  abslogle  25133  tanarg  25134  logcn  25162  logf1o2  25165  cxpsqrtlem  25217  cxpsqrt  25218  root1eq1  25268  cxpeq  25270  ang180lem1  25319  ang180lem2  25320  ang180lem3  25321  ang180lem4  25322  1cubrlem  25351  1cubr  25352  asinlem  25378  asinlem2  25379  asinlem3a  25380  asinlem3  25381  asinf  25382  atandm2  25387  atandm3  25388  atanf  25390  asinneg  25396  efiasin  25398  sinasin  25399  asinsinlem  25401  asinsin  25402  asin1  25404  asinbnd  25409  cosasin  25414  atanneg  25417  atancj  25420  efiatan  25422  atanlogaddlem  25423  atanlogadd  25424  atanlogsublem  25425  atanlogsub  25426  efiatan2  25427  2efiatan  25428  tanatan  25429  cosatan  25431  atantan  25433  atanbndlem  25435  atans2  25441  dvatan  25445  atantayl  25447  atantayl2  25448  log2cnv  25455  basellem3  25593  2sqlem2  25927  nvpi  28377  ipval2  28417  4ipval2  28418  ipval3  28419  ipidsq  28420  dipcl  28422  dipcj  28424  dip0r  28427  dipcn  28430  ip1ilem  28536  ipasslem10  28549  ipasslem11  28550  polid2i  28867  polidi  28868  lnopeq0lem1  29715  lnopeq0i  29717  lnophmlem2  29727  ccfldextdgrr  30962  cnre2csqima  31059  efmul2picn  31772  itgexpif  31782  vtscl  31814  vtsprod  31815  circlemeth  31816  logi  32869  iexpire  32870  itgaddnc  34838  iblabsnc  34842  iblmulc2nc  34843  itgmulc2nc  34846  ftc1anclem3  34855  ftc1anclem6  34858  ftc1anclem7  34859  ftc1anclem8  34860  ftc1anc  34861  dvasin  34864  areacirclem4  34871  cntotbnd  34961  sn-1ne2  39042  re1m1e0m0  39111  sn-addid2  39118  proot1ex  39685  sineq0ALT  41155  iblsplit  42135  sqrtnegnre  43392  requad01  43637  sinh-conventional  44740
  Copyright terms: Public domain W3C validator