Axiom ax-icn 11089

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

This axiom is referenced by:  0cn  11128  mulrid  11134  mul02lem2  11314  mul02  11315  addrid  11317  cnegex  11318  cnegex2  11319  0cnALT  11372  0cnALT2  11373  negicn  11385  ine0  11576  ixi  11770  recextlem1  11771  recextlem2  11772  recex  11773  rimul  12140  cru  12141  crne0  12142  cju  12145  it0e0  12368  2mulicn  12369  2muline0  12370  cnref1o  12902  irec  14128  i2  14129  i3  14130  i4  14131  iexpcyc  14134  crreczi  14155  imre  15035  reim  15036  crre  15041  crim  15042  remim  15044  mulre  15048  cjreb  15050  recj  15051  reneg  15052  readd  15053  remullem  15055  imcj  15059  imneg  15060  imadd  15061  cjadd  15068  cjneg  15074  imval2  15078  rei  15083  imi  15084  cji  15086  cjreim  15087  cjreim2  15088  rennim  15166  cnpart  15167  sqrtneglem  15193  sqrtneg  15194  sqrtm1  15202  absi  15213  absreimsq  15219  absreim  15220  absimle  15236  abs1m  15263  sqreulem  15287  sqreu  15288  bhmafibid1  15395  caucvgr  15603  sinf  16053  cosf  16054  tanval2  16062  tanval3  16063  resinval  16064  recosval  16065  efi4p  16066  resin4p  16067  recos4p  16068  resincl  16069  recoscl  16070  sinneg  16075  cosneg  16076  efival  16081  efmival  16082  sinhval  16083  coshval  16084  retanhcl  16088  tanhlt1  16089  tanhbnd  16090  efeul  16091  sinadd  16093  cosadd  16094  ef01bndlem  16113  sin01bnd  16114  cos01bnd  16115  absef  16126  absefib  16127  efieq1re  16128  demoivre  16129  demoivreALT  16130  nthruc  16181  igz  16866  4sqlem17  16893  cnsubrg  21386  cnrehmeo  24911  cnrehmeoOLD  24912  cmodscexp  25081  ncvspi  25116  cphipval2  25201  4cphipval2  25202  cphipval  25203  itg0  25741  itgz  25742  itgcl  25745  ibl0  25748  iblcnlem1  25749  itgcnlem  25751  itgneg  25765  iblss  25766  iblss2  25767  itgss  25773  itgeqa  25775  iblconst  25779  itgconst  25780  itgadd  25786  iblabs  25790  iblabsr  25791  iblmulc2  25792  itgmulc2  25795  itgsplit  25797  dvsincos  25945  iaa  26293  sincn  26414  coscn  26415  efhalfpi  26440  ef2kpi  26447  efper  26448  sinperlem  26449  efimpi  26460  pige3ALT  26489  sineq0  26493  efeq1  26497  tanregt0  26508  efif1olem4  26514  efifo  26516  eff1olem  26517  circgrp  26521  circsubm  26522  logi  26556  logneg  26557  logm1  26558  lognegb  26559  eflogeq  26571  efiarg  26576  cosargd  26577  logimul  26583  logneg2  26584  abslogle  26587  tanarg  26588  logcn  26616  logf1o2  26619  cxpsqrtlem  26671  cxpsqrt  26672  root1eq1  26725  cxpeq  26727  ang180lem1  26779  ang180lem2  26780  ang180lem3  26781  ang180lem4  26782  1cubrlem  26811  1cubr  26812  asinlem  26838  asinlem2  26839  asinlem3a  26840  asinlem3  26841  asinf  26842  atandm2  26847  atandm3  26848  atanf  26850  asinneg  26856  efiasin  26858  sinasin  26859  asinsinlem  26861  asinsin  26862  asin1  26864  asinbnd  26869  cosasin  26874  atanneg  26877  atancj  26880  efiatan  26882  atanlogaddlem  26883  atanlogadd  26884  atanlogsublem  26885  atanlogsub  26886  efiatan2  26887  2efiatan  26888  tanatan  26889  cosatan  26891  atantan  26893  atanbndlem  26895  atans2  26901  dvatan  26905  atantayl  26907  atantayl2  26908  log2cnv  26914  basellem3  27053  2sqlem2  27389  nvpi  30746  ipval2  30786  4ipval2  30787  ipval3  30788  ipidsq  30789  dipcl  30791  dipcj  30793  dip0r  30796  dipcn  30799  ip1ilem  30905  ipasslem10  30918  ipasslem11  30919  polid2i  31236  polidi  31237  lnopeq0lem1  32084  lnopeq0i  32086  lnophmlem2  32096  re0cj  32825  pythagreim  32827  ccfldextdgrr  33831  constrelextdg2  33906  iconstr  33925  constrrecl  33928  constrimcl  33929  constrmulcl  33930  constrresqrtcl  33936  cos9thpiminplylem3  33943  cos9thpiminplylem4  33944  cos9thpiminplylem5  33945  cos9thpiminply  33947  cos9thpinconstrlem1  33948  cos9thpinconstrlem2  33949  cos9thpinconstr  33950  cnre2csqima  34070  efmul2picn  34755  itgexpif  34765  vtscl  34797  vtsprod  34798  circlemeth  34799  iexpire  35931  itgaddnc  37883  iblabsnc  37887  iblmulc2nc  37888  itgmulc2nc  37891  ftc1anclem3  37898  ftc1anclem6  37901  ftc1anclem7  37902  ftc1anclem8  37903  ftc1anc  37904  dvasin  37907  areacirclem4  37914  cntotbnd  37999  sn-1ne2  42587  0tie0  42637  it1ei  42638  1tiei  42639  retire  42641  ef11d  42661  cxp112d  42663  cxp111d  42664  cxpi11d  42665  re1m1e0m0  42719  sn-addlid  42726  sn-it0e0  42738  sn-negex12  42739  reixi  42745  sn-1ticom  42757  sn-mullid  42758  sn-it1ei  42759  ipiiie0  42760  sn-0tie0  42773  sn-mul02  42774  sn-itrere  42810  sn-retire  42811  cnreeu  42812  proot1ex  43505  sqrtcval  43949  sqrtcval2  43950  resqrtvalex  43953  imsqrtvalex  43954  sineq0ALT  45244  iblsplit  46277  sqrtnegnre  47620  requad01  47934  sinh-conventional  50051