Axiom ax-icn 11158

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

This axiom is referenced by:  0cn  11197  mulrid  11205  mul02lem2  11386  mul02  11387  addrid  11389  cnegex  11390  cnegex2  11391  0cnALT  11444  0cnALT2  11445  negicn  11457  ine0  11648  ixi  11842  recextlem1  11843  recextlem2  11844  recex  11845  rimul  12208  cru  12209  crne0  12210  cju  12213  it0e0  12466  2mulicn  12467  2muline0  12468  cnref1o  13008  irec  14236  i2  14237  i3  14238  i4  14239  iexpcyc  14242  crreczi  14263  imre  15158  reim  15159  crre  15164  crim  15165  remim  15167  mulre  15171  cjreb  15173  recj  15174  reneg  15175  readd  15176  remullem  15178  imcj  15182  imneg  15183  imadd  15184  cjadd  15191  cjneg  15197  imval2  15201  rei  15206  imi  15207  cji  15209  cjreim  15210  cjreim2  15211  rennim  15289  cnpart  15290  sqrtneglem  15316  sqrtneg  15317  sqrtm1  15325  absi  15336  absreimsq  15342  absreim  15343  absimle  15359  abs1m  15386  sqreulem  15410  sqreu  15411  bhmafibid1  15518  caucvgr  15726  sinf  16179  cosf  16180  tanval2  16188  tanval3  16189  resinval  16190  recosval  16191  efi4p  16192  resin4p  16193  recos4p  16194  resincl  16195  recoscl  16196  sinneg  16201  cosneg  16202  efival  16207  efmival  16208  sinhval  16209  coshval  16210  retanhcl  16214  tanhlt1  16215  tanhbnd  16216  efeul  16217  sinadd  16219  cosadd  16220  ef01bndlem  16239  sin01bnd  16240  cos01bnd  16241  absef  16252  absefib  16253  efieq1re  16254  demoivre  16255  demoivreALT  16256  nthruc  16307  igz  16993  4sqlem17  17020  cnsubrg  21556  cnrehmeo  25091  cmodscexp  25259  ncvspi  25294  cphipval2  25379  4cphipval2  25380  cphipval  25381  itg0  25918  itgz  25919  itgcl  25922  ibl0  25925  iblcnlem1  25926  itgcnlem  25928  itgneg  25942  iblss  25943  iblss2  25944  itgss  25950  itgeqa  25952  iblconst  25956  itgconst  25957  itgadd  25963  iblabs  25967  iblabsr  25968  iblmulc2  25969  itgmulc2  25972  itgsplit  25974  dvsincos  26119  iaa  26465  sincn  26583  coscn  26584  efhalfpi  26612  ef2kpi  26619  efper  26620  sinperlem  26621  efimpi  26632  pige3ALT  26661  sineq0  26665  efeq1  26669  tanregt0  26680  efif1olem4  26686  efifo  26688  eff1olem  26689  circgrp  26693  circsubm  26694  logi  26728  logneg  26729  logm1  26730  lognegb  26731  eflogeq  26743  efiarg  26748  cosargd  26749  logimul  26755  logneg2  26756  abslogle  26759  tanarg  26760  logcn  26788  logf1o2  26791  cxpsqrtlem  26843  cxpsqrt  26844  root1eq1  26896  cxpeq  26898  ang180lem1  26950  ang180lem2  26951  ang180lem3  26952  ang180lem4  26953  1cubrlem  26982  1cubr  26983  asinlem  27009  asinlem2  27010  asinlem3a  27011  asinlem3  27012  asinf  27013  atandm2  27018  atandm3  27019  atanf  27021  asinneg  27027  efiasin  27029  sinasin  27030  asinsinlem  27032  asinsin  27033  asin1  27035  asinbnd  27040  cosasin  27045  atanneg  27048  atancj  27051  efiatan  27053  atanlogaddlem  27054  atanlogadd  27055  atanlogsublem  27056  atanlogsub  27057  efiatan2  27058  2efiatan  27059  tanatan  27060  cosatan  27062  atantan  27064  atanbndlem  27066  atans2  27072  dvatan  27076  atantayl  27078  atantayl2  27079  log2cnv  27085  basellem3  27223  2sqlem2  27558  nvpi  30985  ipval2  31025  4ipval2  31026  ipval3  31027  ipidsq  31028  dipcl  31030  dipcj  31032  dip0r  31035  dipcn  31038  ip1ilem  31144  ipasslem10  31157  ipasslem11  31158  polid2i  31475  polidi  31476  lnopeq0lem1  32323  lnopeq0i  32325  lnophmlem2  32335  re0cj  33054  pythagreim  33056  ccfldextdgrr  34028  constrelextdg2  34103  iconstr  34122  constrrecl  34125  constrimcl  34126  constrmulcl  34127  constrresqrtcl  34133  cos9thpiminplylem3  34140  cos9thpiminplylem4  34141  cos9thpiminplylem5  34142  cos9thpiminply  34144  cos9thpinconstrlem1  34145  cos9thpinconstrlem2  34146  cos9thpinconstr  34147  cnre2csqima  34267  efmul2picn  34949  itgexpif  34959  vtscl  34991  vtsprod  34992  circlemeth  34993  iexpire  36181  itgaddnc  38275  iblabsnc  38279  iblmulc2nc  38280  itgmulc2nc  38283  ftc1anclem3  38290  ftc1anclem6  38293  ftc1anclem7  38294  ftc1anclem8  38295  ftc1anc  38296  dvasin  38299  areacirclem4  38306  cntotbnd  38391  sn-1ne2  42978  0tie0  43022  it1ei  43023  1tiei  43024  retire  43026  ef11d  43046  cxp112d  43048  cxp111d  43049  cxpi11d  43050  re1m1e0m0  43104  sn-addlid  43111  sn-it0e0  43123  sn-negex12  43124  reixi  43130  sn-1ticom  43142  sn-mullid  43143  sn-it1ei  43144  ipiiie0  43145  sn-0tie0  43171  sn-mul02  43172  sn-itrere  43208  sn-retire  43209  cnreeu  43210  proot1ex  43871  sqrtcval  44315  sqrtcval2  44316  resqrtvalex  44319  imsqrtvalex  44320  sineq0ALT  45593  iblsplit  46628  sqrtnegnre  47989  requad01  48331  sinh-conventional  50462