Axiom ax-icn 7869

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

This axiom is referenced by:  0cn  7912  mulid1  7917  cnegexlem2  8095  cnegex  8097  0cnALT  8109  negicn  8120  ine0  8313  ixi  8502  rimul  8504  rereim  8505  apreap  8506  cru  8521  apreim  8522  mulreim  8523  apadd1  8527  apneg  8530  aprcl  8565  recextlem1  8569  recexaplem2  8570  recexap  8571  crap0  8874  cju  8877  it0e0  9099  2mulicn  9100  iap0  9101  2muliap0  9102  cnref1o  9609  irec  10575  i2  10576  i3  10577  i4  10578  iexpcyc  10580  imval  10814  imre  10815  reim  10816  crre  10821  crim  10822  remim  10824  mulreap  10828  cjreb  10830  recj  10831  reneg  10832  readd  10833  remullem  10835  imcj  10839  imneg  10840  imadd  10841  cjadd  10848  cjneg  10854  imval2  10858  rei  10863  imi  10864  cji  10866  cjreim  10867  cjreim2  10868  cjap  10870  cnrecnv  10874  rennim  10966  absi  11023  absreimsq  11031  absreim  11032  absimle  11048  climcvg1nlem  11312  sinval  11665  cosval  11666  sinf  11667  cosf  11668  tanval2ap  11676  tanval3ap  11677  resinval  11678  recosval  11679  efi4p  11680  resin4p  11681  recos4p  11682  resincl  11683  recoscl  11684  sinneg  11689  cosneg  11690  efival  11695  efmival  11696  efeul  11697  sinadd  11699  cosadd  11700  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  absef  11732  absefib  11733  efieq1re  11734  demoivre  11735  demoivreALT  11736  igz  12326  cnrehmeocntop  13387  sincn  13484  coscn  13485  efhalfpi  13514  ef2kpi  13521  efper  13522  sinperlem  13523  efimpi  13534  2sqlem2  13745  qdencn  14059