Axiom ax-icn 8224

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

This axiom is referenced by:  0cn  8268  mulrid  8273  cnegexlem2  8451  cnegex  8453  0cnALT  8465  negicn  8476  ine0  8669  ixi  8859  rimul  8861  rereim  8862  apreap  8863  cru  8878  apreim  8879  mulreim  8880  apadd1  8884  apneg  8887  aprcl  8922  aptap  8926  recextlem1  8927  recexaplem2  8928  recexap  8929  crap0  9234  cju  9237  it0e0  9461  2mulicn  9462  iap0  9463  2muliap0  9464  cnref1o  9986  irec  11005  i2  11006  i3  11007  i4  11008  iexpcyc  11010  imval  11539  imre  11540  reim  11541  crre  11546  crim  11547  remim  11549  mulreap  11553  cjreb  11555  recj  11556  reneg  11557  readd  11558  remullem  11560  imcj  11564  imneg  11565  imadd  11566  cjadd  11573  cjneg  11579  imval2  11583  rei  11588  imi  11589  cji  11591  cjreim  11592  cjreim2  11593  cjap  11595  cnrecnv  11599  rennim  11691  absi  11748  absreimsq  11756  absreim  11757  absimle  11773  climcvg1nlem  12038  sinval  12392  cosval  12393  sinf  12394  cosf  12395  tanval2ap  12403  tanval3ap  12404  resinval  12405  recosval  12406  efi4p  12407  resin4p  12408  recos4p  12409  resincl  12410  recoscl  12411  sinneg  12416  cosneg  12417  efival  12422  efmival  12423  efeul  12424  sinadd  12426  cosadd  12427  ef01bndlem  12446  sin01bnd  12447  cos01bnd  12448  absef  12460  absefib  12461  efieq1re  12462  demoivre  12463  demoivreALT  12464  igz  13076  4sqlem17  13109  cnrehmeocntop  15492  sincn  15651  coscn  15652  efhalfpi  15681  ef2kpi  15688  efper  15689  sinperlem  15690  efimpi  15701  2sqlem2  16005  qdencn  16824