Axiom ax-icn 8267

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

This axiom is referenced by:  0cn  8311  mulrid  8316  cnegexlem2  8495  cnegex  8497  0cnALT  8509  negicn  8520  ine0  8714  ixi  8904  rimul  8906  rereim  8907  apreap  8908  cru  8923  apreim  8924  mulreim  8925  apadd1  8929  apneg  8932  aprcl  8967  aptap  8971  recextlem1  8972  recexaplem2  8973  recexap  8974  crap0  9281  cju  9284  it0e0  9508  2mulicn  9509  iap0  9510  2muliap0  9511  cnref1o  10033  irec  11057  i2  11058  i3  11059  i4  11060  iexpcyc  11062  imval  11596  imre  11597  reim  11598  crre  11603  crim  11604  remim  11606  mulreap  11610  cjreb  11612  recj  11613  reneg  11614  readd  11615  remullem  11617  imcj  11621  imneg  11622  imadd  11623  cjadd  11630  cjneg  11636  imval2  11640  sq01  11641  rei  11646  imi  11647  cji  11649  cjreim  11650  cjreim2  11651  cjap  11653  cnrecnv  11657  rennim  11749  absi  11806  absreimsq  11814  absreim  11815  absimle  11831  climcvg1nlem  12096  sinval  12450  cosval  12451  sinf  12452  cosf  12453  tanval2ap  12461  tanval3ap  12462  resinval  12463  recosval  12464  efi4p  12465  resin4p  12466  recos4p  12467  resincl  12468  recoscl  12469  sinneg  12474  cosneg  12475  efival  12480  efmival  12481  efeul  12482  sinadd  12484  cosadd  12485  ef01bndlem  12504  sin01bnd  12505  cos01bnd  12506  absef  12518  absefib  12519  efieq1re  12520  demoivre  12521  demoivreALT  12522  igz  13134  4sqlem17  13167  cnrehmeocntop  15637  sincn  15796  coscn  15797  efhalfpi  15826  ef2kpi  15833  efper  15834  sinperlem  15835  efimpi  15846  2sqlem2  16151  qdencn  16980