Axiom ax-icn 11243

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

This axiom is referenced by:  0cn  11282  mulrid  11288  mul02lem2  11467  mul02  11468  addrid  11470  cnegex  11471  cnegex2  11472  0cnALT  11524  0cnALT2  11525  negicn  11537  ine0  11725  ixi  11919  recextlem1  11920  recextlem2  11921  recex  11922  rimul  12284  cru  12285  crne0  12286  cju  12289  it0e0  12515  2mulicn  12516  2muline0  12517  cnref1o  13050  irec  14250  i2  14251  i3  14252  i4  14253  iexpcyc  14256  crreczi  14277  imre  15157  reim  15158  crre  15163  crim  15164  remim  15166  mulre  15170  cjreb  15172  recj  15173  reneg  15174  readd  15175  remullem  15177  imcj  15181  imneg  15182  imadd  15183  cjadd  15190  cjneg  15196  imval2  15200  rei  15205  imi  15206  cji  15208  cjreim  15209  cjreim2  15210  rennim  15288  cnpart  15289  sqrtneglem  15315  sqrtneg  15316  sqrtm1  15324  absi  15335  absreimsq  15341  absreim  15342  absimle  15358  abs1m  15384  sqreulem  15408  sqreu  15409  bhmafibid1  15514  caucvgr  15724  sinf  16172  cosf  16173  tanval2  16181  tanval3  16182  resinval  16183  recosval  16184  efi4p  16185  resin4p  16186  recos4p  16187  resincl  16188  recoscl  16189  sinneg  16194  cosneg  16195  efival  16200  efmival  16201  sinhval  16202  coshval  16203  retanhcl  16207  tanhlt1  16208  tanhbnd  16209  efeul  16210  sinadd  16212  cosadd  16213  ef01bndlem  16232  sin01bnd  16233  cos01bnd  16234  absef  16245  absefib  16246  efieq1re  16247  demoivre  16248  demoivreALT  16249  nthruc  16300  igz  16981  4sqlem17  17008  cnsubrg  21468  cnrehmeo  25003  cnrehmeoOLD  25004  cmodscexp  25173  ncvspi  25209  cphipval2  25294  4cphipval2  25295  cphipval  25296  itg0  25835  itgz  25836  itgcl  25839  ibl0  25842  iblcnlem1  25843  itgcnlem  25845  itgneg  25859  iblss  25860  iblss2  25861  itgss  25867  itgeqa  25869  iblconst  25873  itgconst  25874  itgadd  25880  iblabs  25884  iblabsr  25885  iblmulc2  25886  itgmulc2  25889  itgsplit  25891  dvsincos  26039  iaa  26385  sincn  26506  coscn  26507  efhalfpi  26531  ef2kpi  26538  efper  26539  sinperlem  26540  efimpi  26551  pige3ALT  26580  sineq0  26584  efeq1  26588  tanregt0  26599  efif1olem4  26605  efifo  26607  eff1olem  26608  circgrp  26612  circsubm  26613  logi  26647  logneg  26648  logm1  26649  lognegb  26650  eflogeq  26662  efiarg  26667  cosargd  26668  logimul  26674  logneg2  26675  abslogle  26678  tanarg  26679  logcn  26707  logf1o2  26710  cxpsqrtlem  26762  cxpsqrt  26763  root1eq1  26816  cxpeq  26818  ang180lem1  26870  ang180lem2  26871  ang180lem3  26872  ang180lem4  26873  1cubrlem  26902  1cubr  26903  asinlem  26929  asinlem2  26930  asinlem3a  26931  asinlem3  26932  asinf  26933  atandm2  26938  atandm3  26939  atanf  26941  asinneg  26947  efiasin  26949  sinasin  26950  asinsinlem  26952  asinsin  26953  asin1  26955  asinbnd  26960  cosasin  26965  atanneg  26968  atancj  26971  efiatan  26973  atanlogaddlem  26974  atanlogadd  26975  atanlogsublem  26976  atanlogsub  26977  efiatan2  26978  2efiatan  26979  tanatan  26980  cosatan  26982  atantan  26984  atanbndlem  26986  atans2  26992  dvatan  26996  atantayl  26998  atantayl2  26999  log2cnv  27005  basellem3  27144  2sqlem2  27480  nvpi  30699  ipval2  30739  4ipval2  30740  ipval3  30741  ipidsq  30742  dipcl  30744  dipcj  30746  dip0r  30749  dipcn  30752  ip1ilem  30858  ipasslem10  30871  ipasslem11  30872  polid2i  31189  polidi  31190  lnopeq0lem1  32037  lnopeq0i  32039  lnophmlem2  32049  re0cj  32756  ccfldextdgrr  33682  constrelextdg2  33737  cnre2csqima  33857  efmul2picn  34573  itgexpif  34583  vtscl  34615  vtsprod  34616  circlemeth  34617  iexpire  35697  itgaddnc  37640  iblabsnc  37644  iblmulc2nc  37645  itgmulc2nc  37648  ftc1anclem3  37655  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  dvasin  37664  areacirclem4  37671  cntotbnd  37756  sn-1ne2  42254  0tie0  42304  it1ei  42305  1tiei  42306  itrere  42307  retire  42308  ef11d  42327  cxp112d  42329  cxp111d  42330  cxpi11d  42331  re1m1e0m0  42373  sn-addlid  42380  sn-it0e0  42391  sn-negex12  42392  reixi  42398  sn-1ticom  42410  sn-mullid  42411  sn-it1ei  42412  ipiiie0  42413  sn-0tie0  42415  sn-mul02  42416  sn-inelr  42443  sn-itrere  42444  sn-retire  42445  cnreeu  42446  proot1ex  43157  sqrtcval  43603  sqrtcval2  43604  resqrtvalex  43607  imsqrtvalex  43608  sineq0ALT  44908  iblsplit  45887  sqrtnegnre  47222  requad01  47495  sinh-conventional  48831