Axiom ax-icn 11186

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

This axiom is used by:  0cn  11225  mulrid  11233  mul02lem2  11414  mul02  11415  addrid  11417  cnegex  11418  cnegex2  11419  0cnALT  11472  0cnALT2  11473  negicn  11485  ine0  11676  ixi  11870  recextlem1  11871  recextlem2  11872  recex  11873  rimul  12236  cru  12237  crne0  12238  cju  12241  it0e0  12494  2mulicn  12495  2muline0  12496  cnref1o  13037  irec  14267  i2  14268  i3  14269  i4  14270  iexpcyc  14273  crreczi  14294  imre  15197  reim  15198  crre  15203  crim  15204  remim  15206  mulre  15210  cjreb  15212  recj  15213  reneg  15214  readd  15215  remullem  15217  imcj  15221  imneg  15222  imadd  15223  cjadd  15230  cjneg  15236  imval2  15240  rei  15245  imi  15246  cji  15248  cjreim  15249  cjreim2  15250  rennim  15328  cnpart  15329  sqrtneglem  15355  sqrtneg  15356  sqrtm1  15364  absi  15375  absreimsq  15381  absreim  15382  absimle  15398  abs1m  15425  sqreulem  15449  sqreu  15450  bhmafibid1  15557  caucvgr  15765  sinf  16216  cosf  16217  tanval2  16225  tanval3  16226  resinval  16227  recosval  16228  efi4p  16229  resin4p  16230  recos4p  16231  resincl  16232  recoscl  16233  sinneg  16238  cosneg  16239  efival  16244  efmival  16245  sinhval  16246  coshval  16247  retanhcl  16251  tanhlt1  16252  tanhbnd  16253  efeul  16254  sinadd  16256  cosadd  16257  ef01bndlem  16276  sin01bnd  16277  cos01bnd  16278  absef  16289  absefib  16290  efieq1re  16291  demoivre  16292  demoivreALT  16293  nthruc  16344  igz  17030  4sqlem17  17057  cnsubrg  21641  cnrehmeo  25182  cmodscexp  25350  ncvspi  25385  cphipval2  25470  4cphipval2  25471  cphipval  25472  itg0  26009  itgz  26010  itgcl  26013  ibl0  26016  iblcnlem1  26017  itgcnlem  26019  itgneg  26033  iblss  26034  iblss2  26035  itgss  26041  itgeqa  26043  iblconst  26047  itgconst  26048  itgadd  26054  iblabs  26058  iblabsr  26059  iblmulc2  26060  itgmulc2  26063  itgsplit  26065  dvsincos  26210  iaa  26558  sincn  26677  coscn  26678  efhalfpi  26706  ef2kpi  26713  efper  26714  sinperlem  26715  efimpi  26726  pige3ALT  26755  sineq0  26759  efeq1  26763  tanregt0  26774  efif1olem4  26780  efifo  26782  eff1olem  26783  circgrp  26787  circsubm  26788  logi  26822  logneg  26823  logm1  26824  lognegb  26825  eflogeq  26837  efiarg  26842  cosargd  26843  logimul  26849  logneg2  26850  abslogle  26853  tanarg  26854  logcn  26882  logf1o2  26885  cxpsqrtlem  26937  cxpsqrt  26938  root1eq1  26990  cxpeq  26992  ang180lem1  27044  ang180lem2  27045  ang180lem3  27046  ang180lem4  27047  1cubrlem  27076  1cubr  27077  asinlem  27103  asinlem2  27104  asinlem3a  27105  asinlem3  27106  asinf  27107  atandm2  27112  atandm3  27113  atanf  27115  asinneg  27121  efiasin  27123  sinasin  27124  asinsinlem  27126  asinsin  27127  asin1  27129  asinbnd  27134  cosasin  27139  atanneg  27142  atancj  27145  efiatan  27147  atanlogaddlem  27148  atanlogadd  27149  atanlogsublem  27150  atanlogsub  27151  efiatan2  27152  2efiatan  27153  tanatan  27154  cosatan  27156  atantan  27158  atanbndlem  27160  atans2  27166  dvatan  27170  atantayl  27172  atantayl2  27173  log2cnv  27179  basellem3  27317  2sqlem2  27652  nvpi  31134  ipval2  31174  4ipval2  31175  ipval3  31176  ipidsq  31177  dipcl  31179  dipcj  31181  dip0r  31184  dipcn  31187  ip1ilem  31293  ipasslem10  31306  ipasslem11  31307  polid2i  31624  polidi  31625  lnopeq0lem1  32472  lnopeq0i  32474  lnophmlem2  32484  re0cj  33201  pythagreim  33203  ccfldextdgrr  34169  constrelextdg2  34244  iconstr  34263  constrrecl  34266  constrimcl  34267  constrmulcl  34268  constrresqrtcl  34274  cos9thpiminplylem3  34281  cos9thpiminplylem4  34282  cos9thpiminplylem5  34283  cos9thpiminply  34285  cos9thpinconstrlem1  34286  cos9thpinconstrlem2  34287  cos9thpinconstr  34288  cnre2csqima  34408  efmul2picn  35091  itgexpif  35101  vtscl  35133  vtsprod  35134  circlemeth  35135  iexpire  36301  itgaddnc  38416  iblabsnc  38420  iblmulc2nc  38421  itgmulc2nc  38424  ftc1anclem3  38431  ftc1anclem6  38434  ftc1anclem7  38435  ftc1anclem8  38436  ftc1anc  38437  dvasin  38440  areacirclem4  38447  cntotbnd  38533  sn-1ne2  43133  0tie0  43177  it1ei  43178  1tiei  43179  retire  43181  ef11d  43201  cxp112d  43203  cxp111d  43204  cxpi11d  43205  re1m1e0m0  43259  sn-addlid  43266  sn-it0e0  43278  sn-negex12  43279  reixi  43285  sn-1ticom  43297  sn-mullid  43298  sn-it1ei  43299  ipiiie0  43300  sn-0tie0  43326  sn-mul02  43327  sn-itrere  43363  sn-retire  43364  cnreeu  43365  proot1ex  44024  sqrtcval  44468  sqrtcval2  44469  resqrtvalex  44472  imsqrtvalex  44473  sineq0ALT  45746  iblsplit  46781  sqrtnegnre  48182  requad01  48524  sinh-conventional  50652