Axiom ax-icn 8105

Description: i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 8061. (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 8012	. 2 class i
2		cc 8008	. 2 class ℂ
3	1, 2	wcel 2200	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  8149  mulrid  8154  cnegexlem2  8333  cnegex  8335  0cnALT  8347  negicn  8358  ine0  8551  ixi  8741  rimul  8743  rereim  8744  apreap  8745  cru  8760  apreim  8761  mulreim  8762  apadd1  8766  apneg  8769  aprcl  8804  aptap  8808  recextlem1  8809  recexaplem2  8810  recexap  8811  crap0  9116  cju  9119  it0e0  9343  2mulicn  9344  iap0  9345  2muliap0  9346  cnref1o  9858  irec  10873  i2  10874  i3  10875  i4  10876  iexpcyc  10878  imval  11376  imre  11377  reim  11378  crre  11383  crim  11384  remim  11386  mulreap  11390  cjreb  11392  recj  11393  reneg  11394  readd  11395  remullem  11397  imcj  11401  imneg  11402  imadd  11403  cjadd  11410  cjneg  11416  imval2  11420  rei  11425  imi  11426  cji  11428  cjreim  11429  cjreim2  11430  cjap  11432  cnrecnv  11436  rennim  11528  absi  11585  absreimsq  11593  absreim  11594  absimle  11610  climcvg1nlem  11875  sinval  12228  cosval  12229  sinf  12230  cosf  12231  tanval2ap  12239  tanval3ap  12240  resinval  12241  recosval  12242  efi4p  12243  resin4p  12244  recos4p  12245  resincl  12246  recoscl  12247  sinneg  12252  cosneg  12253  efival  12258  efmival  12259  efeul  12260  sinadd  12262  cosadd  12263  ef01bndlem  12282  sin01bnd  12283  cos01bnd  12284  absef  12296  absefib  12297  efieq1re  12298  demoivre  12299  demoivreALT  12300  igz  12912  4sqlem17  12945  cnrehmeocntop  15299  sincn  15458  coscn  15459  efhalfpi  15488  ef2kpi  15495  efper  15496  sinperlem  15497  efimpi  15508  2sqlem2  15809  qdencn  16455