Axiom ax-icn 8274

Description: _i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 8230. (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 8181	. 2 class _i
2		cc 8177	. 2 class CC
3	1, 2	wcel 2209	1 wff _i e. CC

This axiom is used by:  0cn  8318  mulrid  8323  cnegexlem2  8503  cnegex  8505  0cnALT  8517  negicn  8528  ine0  8722  ixi  8913  rimul  8915  rereim  8916  apreap  8917  cru  8932  apreim  8933  mulreim  8934  apadd1  8938  apneg  8941  aprcl  8976  aptap  8980  recextlem1  8981  recexaplem2  8982  recexap  8983  crap0  9290  cju  9293  it0e0  9530  2mulicn  9531  iap0  9532  2muliap0  9533  cnref1o  10061  irec  11089  i2  11090  i3  11091  i4  11092  iexpcyc  11094  imval  11629  imre  11630  reim  11631  crre  11636  crim  11637  remim  11639  mulreap  11643  cjreb  11645  recj  11646  reneg  11647  readd  11648  remullem  11650  imcj  11654  imneg  11655  imadd  11656  cjadd  11663  cjneg  11669  imval2  11673  sq01  11674  rei  11679  imi  11680  cji  11682  cjreim  11683  cjreim2  11684  cjap  11686  cnrecnv  11690  rennim  11782  absi  11839  absreimsq  11847  absreim  11848  absimle  11865  climcvg1nlem  12131  sinval  12485  cosval  12486  sinf  12487  cosf  12488  tanval2ap  12496  tanval3ap  12497  resinval  12498  recosval  12499  efi4p  12500  resin4p  12501  recos4p  12502  resincl  12503  recoscl  12504  sinneg  12509  cosneg  12510  efival  12515  efmival  12516  efeul  12517  sinadd  12519  cosadd  12520  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  absef  12553  absefib  12554  efieq1re  12555  demoivre  12556  demoivreALT  12557  igz  13173  4sqlem17  13206  cnrehmeocntop  15760  sincn  15919  coscn  15920  efhalfpi  15950  ef2kpi  15957  efper  15958  sinperlem  15959  efimpi  15970  2sqlem2  16332  qdencn  17170