Axiom ax-icn 11259

Description: i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by Theorem axicn 11235. (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 11202	. 2 class i
2		cc 11198	. 2 class ℂ
3	1, 2	wcel 2144	1 wff i ∈ ℂ

This axiom is used by:  0cn  11298  mulrid  11306  mul02lem2  11487  mul02  11488  addrid  11490  cnegex  11491  cnegex2  11492  0cnALT  11545  0cnALT2  11546  negicn  11558  ine0  11751  ixi  11945  recextlem1  11946  recextlem2  11947  recex  11948  rimul  12311  cru  12312  crne0  12313  cju  12316  it0e0  12569  2mulicn  12570  2muline0  12571  cnref1o  13113  irec  14345  i2  14346  i3  14347  i4  14348  iexpcyc  14351  crreczi  14372  imre  15275  reim  15276  crre  15281  crim  15282  remim  15284  mulre  15288  cjreb  15290  recj  15291  reneg  15292  readd  15293  remullem  15295  imcj  15299  imneg  15300  imadd  15301  cjadd  15308  cjneg  15314  imval2  15318  rei  15323  imi  15324  cji  15326  cjreim  15327  cjreim2  15328  rennim  15406  cnpart  15407  sqrtneglem  15433  sqrtneg  15434  sqrtm1  15442  absi  15453  absreimsq  15459  absreim  15460  absimle  15476  abs1m  15503  sqreulem  15527  sqreu  15528  bhmafibid1  15635  caucvgr  15843  sinf  16292  cosf  16293  tanval2  16301  tanval3  16302  resinval  16303  recosval  16304  efi4p  16305  resin4p  16306  recos4p  16307  resincl  16308  recoscl  16309  sinneg  16314  cosneg  16315  efival  16320  efmival  16321  sinhval  16322  coshval  16323  retanhcl  16327  tanhlt1  16328  tanhbnd  16329  efeul  16330  sinadd  16332  cosadd  16333  ef01bndlem  16352  sin01bnd  16353  cos01bnd  16354  absef  16365  absefib  16366  efieq1re  16367  demoivre  16368  demoivreALT  16369  nthruc  16420  igz  17112  4sqlem17  17139  cnsubrg  21733  cnrehmeo  25274  cmodscexp  25442  ncvspi  25477  cphipval2  25562  4cphipval2  25563  cphipval  25564  itg0  26100  itgz  26101  itgcl  26104  ibl0  26107  iblcnlem1  26108  itgcnlem  26110  itgneg  26124  iblss  26125  iblss2  26126  itgss  26132  itgeqa  26134  iblconst  26138  itgconst  26139  itgadd  26145  iblabs  26149  iblabsr  26150  iblmulc2  26151  itgmulc2  26154  itgsplit  26156  dvsincos  26301  iaa  26651  iaaOLD  26652  sincn  26771  coscn  26772  efhalfpi  26800  ef2kpi  26807  efper  26808  sinperlem  26809  efimpi  26820  pige3ALT  26848  sineq0  26852  efeq1  26856  tanregt0  26867  efif1olem4  26873  efifo  26875  eff1olem  26876  circgrp  26880  circsubm  26881  logi  26915  logneg  26916  logm1  26917  lognegb  26918  eflogeq  26930  efiarg  26935  cosargd  26936  logimul  26942  logneg2  26943  abslogle  26946  tanarg  26947  logcn  26975  logf1o2  26978  cxpsqrtlem  27030  cxpsqrt  27031  root1eq1  27083  cxpeq  27085  ang180lem1  27137  ang180lem2  27138  ang180lem3  27139  ang180lem4  27140  1cubrlem  27169  1cubr  27170  asinlem  27196  asinlem2  27197  asinlem3a  27198  asinlem3  27199  asinf  27200  atandm2  27205  atandm3  27206  atanf  27208  asinneg  27214  efiasin  27216  sinasin  27217  asinsinlem  27219  asinsin  27220  asin1  27222  asinbnd  27227  cosasin  27232  atanneg  27235  atancj  27238  efiatan  27240  atanlogaddlem  27241  atanlogadd  27242  atanlogsublem  27243  atanlogsub  27244  efiatan2  27245  2efiatan  27246  tanatan  27247  cosatan  27249  atantan  27251  atanbndlem  27253  atans2  27259  dvatan  27263  atantayl  27265  atantayl2  27266  log2cnv  27272  basellem3  27410  2sqlem2  27745  nvpi  31269  ipval2  31309  4ipval2  31310  ipval3  31311  ipidsq  31312  dipcl  31314  dipcj  31316  dip0r  31319  dipcn  31322  ip1ilem  31428  ipasslem10  31441  ipasslem11  31442  polid2i  31759  polidi  31760  lnopeq0lem1  32607  lnopeq0i  32609  lnophmlem2  32619  re0cj  33377  pythagreim  33379  ccfldextdgrr  34346  constrelextdg2  34421  iconstr  34440  constrrecl  34443  constrimcl  34444  constrmulcl  34445  constrresqrtcl  34451  cos9thpiminplylem3  34458  cos9thpiminplylem4  34459  cos9thpiminplylem5  34460  cos9thpiminply  34462  cos9thpinconstrlem1  34463  cos9thpinconstrlem2  34464  cos9thpinconstr  34465  cnre2csqima  34585  efmul2picn  35267  itgexpif  35277  vtscl  35309  vtsprod  35310  circlemeth  35311  iexpire  36542  itgaddnc  38641  iblabsnc  38645  iblmulc2nc  38646  itgmulc2nc  38649  ftc1anclem3  38656  ftc1anclem6  38659  ftc1anclem7  38660  ftc1anclem8  38661  ftc1anc  38662  dvasin  38665  areacirclem4  38672  cntotbnd  38773  sn-1ne2  43373  0tie0  43415  it1ei  43416  1tiei  43417  retire  43419  ef11d  43433  cxp112d  43435  cxp111d  43436  cxpi11d  43437  re1m1e0m0  43491  sn-addlid  43498  sn-it0e0  43510  sn-negex12  43511  reixi  43517  sn-1ticom  43529  sn-mullid  43530  sn-it1ei  43531  ipiiie0  43532  sn-0tie0  43558  sn-mul02  43559  sn-itrere  43595  sn-retire  43596  cnreeu  43597  proot1ex  44240  sqrtcval  44683  sqrtcval2  44684  resqrtvalex  44687  imsqrtvalex  44688  sineq0ALT  45961  iblsplit  47018  sqrtnegnre  48419  requad01  48761  sinh-conventional  50874