Axiom ax-icn 9595

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

Assertion

Ref	Expression
ax-icn	|- _i e. CC

Detailed syntax breakdown of Axiom ax-icn

Step	Hyp	Ref	Expression
1		ci 9538	. 2 class _i
2		cc 9534	. 2 class CC
3	1, 2	wcel 1886	1 wff _i e. CC

This axiom is referenced by:  0cn  9632  mulid1  9637  mul02lem2  9807  mul02  9808  addid1  9810  cnegex  9811  cnegex2  9812  0cnALT  9861  negicn  9873  ine0  10051  ixi  10238  recextlem1  10239  recextlem2  10240  recex  10241  rimul  10597  cru  10598  crne0  10599  cju  10602  it0e0  10832  2mulicn  10833  2muline0  10834  cnref1o  11294  irec  12371  i2  12372  i3  12373  i4  12374  iexpcyc  12376  crreczi  12394  imre  13164  reim  13165  crre  13170  crim  13171  remim  13173  mulre  13177  cjreb  13179  recj  13180  reneg  13181  readd  13182  remullem  13184  imcj  13188  imneg  13189  imadd  13190  cjadd  13197  cjneg  13203  imval2  13207  rei  13212  imi  13213  cji  13215  cjreim  13216  cjreim2  13217  rennim  13295  cnpart  13296  sqrtneglem  13323  sqrtneg  13324  sqrtm1  13332  absi  13342  absreimsq  13348  absreim  13349  absimle  13365  abs1m  13391  sqreulem  13415  sqreu  13416  caucvgr  13734  sinf  14171  cosf  14172  tanval2  14180  tanval3  14181  resinval  14182  recosval  14183  efi4p  14184  resin4p  14185  recos4p  14186  resincl  14187  recoscl  14188  sinneg  14193  cosneg  14194  efival  14199  efmival  14200  sinhval  14201  coshval  14202  retanhcl  14206  tanhlt1  14207  tanhbnd  14208  efeul  14209  sinadd  14211  cosadd  14212  ef01bndlem  14231  sin01bnd  14232  cos01bnd  14233  absef  14244  absefib  14245  efieq1re  14246  demoivre  14247  demoivreALT  14248  nthruc  14296  igz  14871  4sqlem17OLD  14898  4sqlem17  14904  cnsubrg  19021  cnrehmeo  21974  itg0  22730  itgz  22731  itgcl  22734  ibl0  22737  iblcnlem1  22738  itgcnlem  22740  itgneg  22754  iblss  22755  iblss2  22756  itgss  22762  itgeqa  22764  iblconst  22768  itgconst  22769  itgadd  22775  iblabs  22779  iblabsr  22780  iblmulc2  22781  itgmulc2  22784  itgsplit  22786  dvsincos  22926  iaa  23274  sincn  23392  coscn  23393  efhalfpi  23419  ef2kpi  23426  efper  23427  sinperlem  23428  efimpi  23439  pige3  23465  sineq0  23469  efeq1  23471  tanregt0  23481  efif1olem4  23487  efifo  23489  eff1olem  23490  circgrp  23494  circsubm  23495  logneg  23530  logm1  23531  lognegb  23532  eflogeq  23544  efiarg  23549  cosargd  23550  logimul  23556  logneg2  23557  abslogle  23560  tanarg  23561  logcn  23585  logf1o2  23588  cxpsqrtlem  23640  cxpsqrt  23641  root1eq1  23688  cxpeq  23690  ang180lem1  23731  ang180lem2  23732  ang180lem3  23733  ang180lem4  23734  1cubrlem  23760  1cubr  23761  asinlem  23787  asinlem2  23788  asinlem3a  23789  asinlem3  23790  asinf  23791  atandm2  23796  atandm3  23797  atanf  23799  asinneg  23805  efiasin  23807  sinasin  23808  asinsinlem  23810  asinsin  23811  asin1  23813  asinbnd  23818  cosasin  23823  atanneg  23826  atancj  23829  efiatan  23831  atanlogaddlem  23832  atanlogadd  23833  atanlogsublem  23834  atanlogsub  23835  efiatan2  23836  2efiatan  23837  tanatan  23838  cosatan  23840  atantan  23842  atanbndlem  23844  atans2  23850  dvatan  23854  atantayl  23856  atantayl2  23857  log2cnv  23863  basellem3  24002  2sqlem2  24285  circgrpOLD  26095  nvpi  26288  ipval2  26336  4ipval2  26337  ipval3  26338  4ipval3  26341  ipidsq  26342  dipcl  26344  dipcj  26346  dip0r  26349  dipcn  26352  sspival  26370  ip1ilem  26460  ipasslem10  26473  ipasslem11  26474  polid2i  26803  polidi  26804  lnopeq0lem1  27651  lnopeq0i  27653  lnophmlem2  27663  bhmafibid1  28398  cnre2csqima  28710  logi  30363  iexpire  30364  itgaddnc  31995  iblabsnc  31999  iblmulc2nc  32000  itgmulc2nc  32003  ftc1anclem3  32012  ftc1anclem6  32015  ftc1anclem7  32016  ftc1anclem8  32017  ftc1anc  32018  dvasin  32021  areacirclem4  32028  cntotbnd  32121  proot1ex  36072  iblsplit  37837  sinh-conventional  40446