Axiom ax-icn 7715

Description: i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 7671. (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 7622	. 2 class i
2		cc 7618	. 2 class ℂ
3	1, 2	wcel 1480	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  7758  mulid1  7763  cnegexlem2  7938  cnegex  7940  0cnALT  7952  negicn  7963  ine0  8156  ixi  8345  rimul  8347  rereim  8348  apreap  8349  cru  8364  apreim  8365  mulreim  8366  apadd1  8370  apneg  8373  aprcl  8408  recextlem1  8412  recexaplem2  8413  recexap  8414  crap0  8716  cju  8719  it0e0  8941  2mulicn  8942  iap0  8943  2muliap0  8944  cnref1o  9440  irec  10392  i2  10393  i3  10394  i4  10395  iexpcyc  10397  imval  10622  imre  10623  reim  10624  crre  10629  crim  10630  remim  10632  mulreap  10636  cjreb  10638  recj  10639  reneg  10640  readd  10641  remullem  10643  imcj  10647  imneg  10648  imadd  10649  cjadd  10656  cjneg  10662  imval2  10666  rei  10671  imi  10672  cji  10674  cjreim  10675  cjreim2  10676  cjap  10678  cnrecnv  10682  rennim  10774  absi  10831  absreimsq  10839  absreim  10840  absimle  10856  climcvg1nlem  11118  sinval  11409  cosval  11410  sinf  11411  cosf  11412  tanval2ap  11420  tanval3ap  11421  resinval  11422  recosval  11423  efi4p  11424  resin4p  11425  recos4p  11426  resincl  11427  recoscl  11428  sinneg  11433  cosneg  11434  efival  11439  efmival  11440  efeul  11441  sinadd  11443  cosadd  11444  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  absef  11476  absefib  11477  efieq1re  11478  demoivre  11479  demoivreALT  11480  cnrehmeocntop  12762  sincn  12858  coscn  12859  efhalfpi  12880  ef2kpi  12887  efper  12888  sinperlem  12889  efimpi  12900  qdencn  13222