Axiom ax-icn 11211

Description: i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by Theorem axicn 11187. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-icn	⊢ i ∈ ℂ

Detailed syntax breakdown of Axiom ax-icn

Step	Hyp	Ref	Expression
1		ci 11154	. 2 class i
2		cc 11150	. 2 class ℂ
3	1, 2	wcel 2105	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  11250  mulrid  11256  mul02lem2  11435  mul02  11436  addrid  11438  cnegex  11439  cnegex2  11440  0cnALT  11493  0cnALT2  11494  negicn  11506  ine0  11695  ixi  11889  recextlem1  11890  recextlem2  11891  recex  11892  rimul  12254  cru  12255  crne0  12256  cju  12259  it0e0  12485  2mulicn  12486  2muline0  12487  cnref1o  13024  irec  14236  i2  14237  i3  14238  i4  14239  iexpcyc  14242  crreczi  14263  imre  15143  reim  15144  crre  15149  crim  15150  remim  15152  mulre  15156  cjreb  15158  recj  15159  reneg  15160  readd  15161  remullem  15163  imcj  15167  imneg  15168  imadd  15169  cjadd  15176  cjneg  15182  imval2  15186  rei  15191  imi  15192  cji  15194  cjreim  15195  cjreim2  15196  rennim  15274  cnpart  15275  sqrtneglem  15301  sqrtneg  15302  sqrtm1  15310  absi  15321  absreimsq  15327  absreim  15328  absimle  15344  abs1m  15370  sqreulem  15394  sqreu  15395  bhmafibid1  15500  caucvgr  15708  sinf  16156  cosf  16157  tanval2  16165  tanval3  16166  resinval  16167  recosval  16168  efi4p  16169  resin4p  16170  recos4p  16171  resincl  16172  recoscl  16173  sinneg  16178  cosneg  16179  efival  16184  efmival  16185  sinhval  16186  coshval  16187  retanhcl  16191  tanhlt1  16192  tanhbnd  16193  efeul  16194  sinadd  16196  cosadd  16197  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  absef  16229  absefib  16230  efieq1re  16231  demoivre  16232  demoivreALT  16233  nthruc  16284  igz  16967  4sqlem17  16994  cnsubrg  21462  cnrehmeo  24997  cnrehmeoOLD  24998  cmodscexp  25167  ncvspi  25203  cphipval2  25288  4cphipval2  25289  cphipval  25290  itg0  25829  itgz  25830  itgcl  25833  ibl0  25836  iblcnlem1  25837  itgcnlem  25839  itgneg  25853  iblss  25854  iblss2  25855  itgss  25861  itgeqa  25863  iblconst  25867  itgconst  25868  itgadd  25874  iblabs  25878  iblabsr  25879  iblmulc2  25880  itgmulc2  25883  itgsplit  25885  dvsincos  26033  iaa  26381  sincn  26502  coscn  26503  efhalfpi  26527  ef2kpi  26534  efper  26535  sinperlem  26536  efimpi  26547  pige3ALT  26576  sineq0  26580  efeq1  26584  tanregt0  26595  efif1olem4  26601  efifo  26603  eff1olem  26604  circgrp  26608  circsubm  26609  logi  26643  logneg  26644  logm1  26645  lognegb  26646  eflogeq  26658  efiarg  26663  cosargd  26664  logimul  26670  logneg2  26671  abslogle  26674  tanarg  26675  logcn  26703  logf1o2  26706  cxpsqrtlem  26758  cxpsqrt  26759  root1eq1  26812  cxpeq  26814  ang180lem1  26866  ang180lem2  26867  ang180lem3  26868  ang180lem4  26869  1cubrlem  26898  1cubr  26899  asinlem  26925  asinlem2  26926  asinlem3a  26927  asinlem3  26928  asinf  26929  atandm2  26934  atandm3  26935  atanf  26937  asinneg  26943  efiasin  26945  sinasin  26946  asinsinlem  26948  asinsin  26949  asin1  26951  asinbnd  26956  cosasin  26961  atanneg  26964  atancj  26967  efiatan  26969  atanlogaddlem  26970  atanlogadd  26971  atanlogsublem  26972  atanlogsub  26973  efiatan2  26974  2efiatan  26975  tanatan  26976  cosatan  26978  atantan  26980  atanbndlem  26982  atans2  26988  dvatan  26992  atantayl  26994  atantayl2  26995  log2cnv  27001  basellem3  27140  2sqlem2  27476  nvpi  30695  ipval2  30735  4ipval2  30736  ipval3  30737  ipidsq  30738  dipcl  30740  dipcj  30742  dip0r  30745  dipcn  30748  ip1ilem  30854  ipasslem10  30867  ipasslem11  30868  polid2i  31185  polidi  31186  lnopeq0lem1  32033  lnopeq0i  32035  lnophmlem2  32045  re0cj  32759  ccfldextdgrr  33696  constrelextdg2  33751  cnre2csqima  33871  efmul2picn  34589  itgexpif  34599  vtscl  34631  vtsprod  34632  circlemeth  34633  iexpire  35714  itgaddnc  37666  iblabsnc  37670  iblmulc2nc  37671  itgmulc2nc  37674  ftc1anclem3  37681  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  dvasin  37690  areacirclem4  37697  cntotbnd  37782  sn-1ne2  42278  0tie0  42328  it1ei  42329  1tiei  42330  itrere  42331  retire  42332  ef11d  42353  cxp112d  42355  cxp111d  42356  cxpi11d  42357  re1m1e0m0  42403  sn-addlid  42410  sn-it0e0  42421  sn-negex12  42422  reixi  42428  sn-1ticom  42440  sn-mullid  42441  sn-it1ei  42442  ipiiie0  42443  sn-0tie0  42445  sn-mul02  42446  sn-inelr  42473  sn-itrere  42474  sn-retire  42475  cnreeu  42476  proot1ex  43184  sqrtcval  43630  sqrtcval2  43631  resqrtvalex  43634  imsqrtvalex  43635  sineq0ALT  44934  iblsplit  45921  sqrtnegnre  47256  requad01  47545  sinh-conventional  48969