Axiom ax-icn 7905

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

This axiom is referenced by:  0cn  7948  mulrid  7953  cnegexlem2  8132  cnegex  8134  0cnALT  8146  negicn  8157  ine0  8350  ixi  8539  rimul  8541  rereim  8542  apreap  8543  cru  8558  apreim  8559  mulreim  8560  apadd1  8564  apneg  8567  aprcl  8602  aptap  8606  recextlem1  8607  recexaplem2  8608  recexap  8609  crap0  8914  cju  8917  it0e0  9139  2mulicn  9140  iap0  9141  2muliap0  9142  cnref1o  9649  irec  10619  i2  10620  i3  10621  i4  10622  iexpcyc  10624  imval  10858  imre  10859  reim  10860  crre  10865  crim  10866  remim  10868  mulreap  10872  cjreb  10874  recj  10875  reneg  10876  readd  10877  remullem  10879  imcj  10883  imneg  10884  imadd  10885  cjadd  10892  cjneg  10898  imval2  10902  rei  10907  imi  10908  cji  10910  cjreim  10911  cjreim2  10912  cjap  10914  cnrecnv  10918  rennim  11010  absi  11067  absreimsq  11075  absreim  11076  absimle  11092  climcvg1nlem  11356  sinval  11709  cosval  11710  sinf  11711  cosf  11712  tanval2ap  11720  tanval3ap  11721  resinval  11722  recosval  11723  efi4p  11724  resin4p  11725  recos4p  11726  resincl  11727  recoscl  11728  sinneg  11733  cosneg  11734  efival  11739  efmival  11740  efeul  11741  sinadd  11743  cosadd  11744  ef01bndlem  11763  sin01bnd  11764  cos01bnd  11765  absef  11776  absefib  11777  efieq1re  11778  demoivre  11779  demoivreALT  11780  igz  12371  cnrehmeocntop  14063  sincn  14160  coscn  14161  efhalfpi  14190  ef2kpi  14197  efper  14198  sinperlem  14199  efimpi  14210  2sqlem2  14432  qdencn  14745