Axiom ax-icn 7969

Description: _i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 7925. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-icn	|- _i e. CC

Detailed syntax breakdown of Axiom ax-icn

Step	Hyp	Ref	Expression
1		ci 7876	. 2 class _i
2		cc 7872	. 2 class CC
3	1, 2	wcel 2164	1 wff _i e. CC

This axiom is referenced by:  0cn  8013  mulrid  8018  cnegexlem2  8197  cnegex  8199  0cnALT  8211  negicn  8222  ine0  8415  ixi  8604  rimul  8606  rereim  8607  apreap  8608  cru  8623  apreim  8624  mulreim  8625  apadd1  8629  apneg  8632  aprcl  8667  aptap  8671  recextlem1  8672  recexaplem2  8673  recexap  8674  crap0  8979  cju  8982  it0e0  9206  2mulicn  9207  iap0  9208  2muliap0  9209  cnref1o  9719  irec  10713  i2  10714  i3  10715  i4  10716  iexpcyc  10718  imval  10997  imre  10998  reim  10999  crre  11004  crim  11005  remim  11007  mulreap  11011  cjreb  11013  recj  11014  reneg  11015  readd  11016  remullem  11018  imcj  11022  imneg  11023  imadd  11024  cjadd  11031  cjneg  11037  imval2  11041  rei  11046  imi  11047  cji  11049  cjreim  11050  cjreim2  11051  cjap  11053  cnrecnv  11057  rennim  11149  absi  11206  absreimsq  11214  absreim  11215  absimle  11231  climcvg1nlem  11495  sinval  11848  cosval  11849  sinf  11850  cosf  11851  tanval2ap  11859  tanval3ap  11860  resinval  11861  recosval  11862  efi4p  11863  resin4p  11864  recos4p  11865  resincl  11866  recoscl  11867  sinneg  11872  cosneg  11873  efival  11878  efmival  11879  efeul  11880  sinadd  11882  cosadd  11883  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  absef  11916  absefib  11917  efieq1re  11918  demoivre  11919  demoivreALT  11920  igz  12515  4sqlem17  12548  cnrehmeocntop  14789  sincn  14945  coscn  14946  efhalfpi  14975  ef2kpi  14982  efper  14983  sinperlem  14984  efimpi  14995  2sqlem2  15272  qdencn  15587