Axiom ax-icn 8040

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

This axiom is referenced by:  0cn  8084  mulrid  8089  cnegexlem2  8268  cnegex  8270  0cnALT  8282  negicn  8293  ine0  8486  ixi  8676  rimul  8678  rereim  8679  apreap  8680  cru  8695  apreim  8696  mulreim  8697  apadd1  8701  apneg  8704  aprcl  8739  aptap  8743  recextlem1  8744  recexaplem2  8745  recexap  8746  crap0  9051  cju  9054  it0e0  9278  2mulicn  9279  iap0  9280  2muliap0  9281  cnref1o  9792  irec  10806  i2  10807  i3  10808  i4  10809  iexpcyc  10811  imval  11236  imre  11237  reim  11238  crre  11243  crim  11244  remim  11246  mulreap  11250  cjreb  11252  recj  11253  reneg  11254  readd  11255  remullem  11257  imcj  11261  imneg  11262  imadd  11263  cjadd  11270  cjneg  11276  imval2  11280  rei  11285  imi  11286  cji  11288  cjreim  11289  cjreim2  11290  cjap  11292  cnrecnv  11296  rennim  11388  absi  11445  absreimsq  11453  absreim  11454  absimle  11470  climcvg1nlem  11735  sinval  12088  cosval  12089  sinf  12090  cosf  12091  tanval2ap  12099  tanval3ap  12100  resinval  12101  recosval  12102  efi4p  12103  resin4p  12104  recos4p  12105  resincl  12106  recoscl  12107  sinneg  12112  cosneg  12113  efival  12118  efmival  12119  efeul  12120  sinadd  12122  cosadd  12123  ef01bndlem  12142  sin01bnd  12143  cos01bnd  12144  absef  12156  absefib  12157  efieq1re  12158  demoivre  12159  demoivreALT  12160  igz  12772  4sqlem17  12805  cnrehmeocntop  15157  sincn  15316  coscn  15317  efhalfpi  15346  ef2kpi  15353  efper  15354  sinperlem  15355  efimpi  15366  2sqlem2  15667  qdencn  16107