Axiom ax-icn 11134

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

This axiom is referenced by:  0cn  11173  mulrid  11179  mul02lem2  11358  mul02  11359  addrid  11361  cnegex  11362  cnegex2  11363  0cnALT  11416  0cnALT2  11417  negicn  11429  ine0  11620  ixi  11814  recextlem1  11815  recextlem2  11816  recex  11817  rimul  12184  cru  12185  crne0  12186  cju  12189  it0e0  12412  2mulicn  12413  2muline0  12414  cnref1o  12951  irec  14173  i2  14174  i3  14175  i4  14176  iexpcyc  14179  crreczi  14200  imre  15081  reim  15082  crre  15087  crim  15088  remim  15090  mulre  15094  cjreb  15096  recj  15097  reneg  15098  readd  15099  remullem  15101  imcj  15105  imneg  15106  imadd  15107  cjadd  15114  cjneg  15120  imval2  15124  rei  15129  imi  15130  cji  15132  cjreim  15133  cjreim2  15134  rennim  15212  cnpart  15213  sqrtneglem  15239  sqrtneg  15240  sqrtm1  15248  absi  15259  absreimsq  15265  absreim  15266  absimle  15282  abs1m  15309  sqreulem  15333  sqreu  15334  bhmafibid1  15441  caucvgr  15649  sinf  16099  cosf  16100  tanval2  16108  tanval3  16109  resinval  16110  recosval  16111  efi4p  16112  resin4p  16113  recos4p  16114  resincl  16115  recoscl  16116  sinneg  16121  cosneg  16122  efival  16127  efmival  16128  sinhval  16129  coshval  16130  retanhcl  16134  tanhlt1  16135  tanhbnd  16136  efeul  16137  sinadd  16139  cosadd  16140  ef01bndlem  16159  sin01bnd  16160  cos01bnd  16161  absef  16172  absefib  16173  efieq1re  16174  demoivre  16175  demoivreALT  16176  nthruc  16227  igz  16912  4sqlem17  16939  cnsubrg  21351  cnrehmeo  24858  cnrehmeoOLD  24859  cmodscexp  25028  ncvspi  25063  cphipval2  25148  4cphipval2  25149  cphipval  25150  itg0  25688  itgz  25689  itgcl  25692  ibl0  25695  iblcnlem1  25696  itgcnlem  25698  itgneg  25712  iblss  25713  iblss2  25714  itgss  25720  itgeqa  25722  iblconst  25726  itgconst  25727  itgadd  25733  iblabs  25737  iblabsr  25738  iblmulc2  25739  itgmulc2  25742  itgsplit  25744  dvsincos  25892  iaa  26240  sincn  26361  coscn  26362  efhalfpi  26387  ef2kpi  26394  efper  26395  sinperlem  26396  efimpi  26407  pige3ALT  26436  sineq0  26440  efeq1  26444  tanregt0  26455  efif1olem4  26461  efifo  26463  eff1olem  26464  circgrp  26468  circsubm  26469  logi  26503  logneg  26504  logm1  26505  lognegb  26506  eflogeq  26518  efiarg  26523  cosargd  26524  logimul  26530  logneg2  26531  abslogle  26534  tanarg  26535  logcn  26563  logf1o2  26566  cxpsqrtlem  26618  cxpsqrt  26619  root1eq1  26672  cxpeq  26674  ang180lem1  26726  ang180lem2  26727  ang180lem3  26728  ang180lem4  26729  1cubrlem  26758  1cubr  26759  asinlem  26785  asinlem2  26786  asinlem3a  26787  asinlem3  26788  asinf  26789  atandm2  26794  atandm3  26795  atanf  26797  asinneg  26803  efiasin  26805  sinasin  26806  asinsinlem  26808  asinsin  26809  asin1  26811  asinbnd  26816  cosasin  26821  atanneg  26824  atancj  26827  efiatan  26829  atanlogaddlem  26830  atanlogadd  26831  atanlogsublem  26832  atanlogsub  26833  efiatan2  26834  2efiatan  26835  tanatan  26836  cosatan  26838  atantan  26840  atanbndlem  26842  atans2  26848  dvatan  26852  atantayl  26854  atantayl2  26855  log2cnv  26861  basellem3  27000  2sqlem2  27336  nvpi  30603  ipval2  30643  4ipval2  30644  ipval3  30645  ipidsq  30646  dipcl  30648  dipcj  30650  dip0r  30653  dipcn  30656  ip1ilem  30762  ipasslem10  30775  ipasslem11  30776  polid2i  31093  polidi  31094  lnopeq0lem1  31941  lnopeq0i  31943  lnophmlem2  31953  re0cj  32674  pythagreim  32676  ccfldextdgrr  33674  constrelextdg2  33744  iconstr  33763  constrrecl  33766  constrimcl  33767  constrmulcl  33768  constrresqrtcl  33774  cos9thpiminplylem3  33781  cos9thpiminplylem4  33782  cos9thpiminplylem5  33783  cos9thpiminply  33785  cos9thpinconstrlem1  33786  cos9thpinconstrlem2  33787  cos9thpinconstr  33788  cnre2csqima  33908  efmul2picn  34594  itgexpif  34604  vtscl  34636  vtsprod  34637  circlemeth  34638  iexpire  35729  itgaddnc  37681  iblabsnc  37685  iblmulc2nc  37686  itgmulc2nc  37689  ftc1anclem3  37696  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  dvasin  37705  areacirclem4  37712  cntotbnd  37797  sn-1ne2  42260  0tie0  42310  it1ei  42311  1tiei  42312  retire  42314  ef11d  42334  cxp112d  42336  cxp111d  42337  cxpi11d  42338  re1m1e0m0  42392  sn-addlid  42399  sn-it0e0  42411  sn-negex12  42412  reixi  42418  sn-1ticom  42430  sn-mullid  42431  sn-it1ei  42432  ipiiie0  42433  sn-0tie0  42446  sn-mul02  42447  sn-itrere  42483  sn-retire  42484  cnreeu  42485  proot1ex  43192  sqrtcval  43637  sqrtcval2  43638  resqrtvalex  43641  imsqrtvalex  43642  sineq0ALT  44933  iblsplit  45971  sqrtnegnre  47312  requad01  47626  sinh-conventional  49732