Axiom ax-icn 8127

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

This axiom is referenced by:  0cn  8171  mulrid  8176  cnegexlem2  8355  cnegex  8357  0cnALT  8369  negicn  8380  ine0  8573  ixi  8763  rimul  8765  rereim  8766  apreap  8767  cru  8782  apreim  8783  mulreim  8784  apadd1  8788  apneg  8791  aprcl  8826  aptap  8830  recextlem1  8831  recexaplem2  8832  recexap  8833  crap0  9138  cju  9141  it0e0  9365  2mulicn  9366  iap0  9367  2muliap0  9368  cnref1o  9885  irec  10902  i2  10903  i3  10904  i4  10905  iexpcyc  10907  imval  11428  imre  11429  reim  11430  crre  11435  crim  11436  remim  11438  mulreap  11442  cjreb  11444  recj  11445  reneg  11446  readd  11447  remullem  11449  imcj  11453  imneg  11454  imadd  11455  cjadd  11462  cjneg  11468  imval2  11472  rei  11477  imi  11478  cji  11480  cjreim  11481  cjreim2  11482  cjap  11484  cnrecnv  11488  rennim  11580  absi  11637  absreimsq  11645  absreim  11646  absimle  11662  climcvg1nlem  11927  sinval  12281  cosval  12282  sinf  12283  cosf  12284  tanval2ap  12292  tanval3ap  12293  resinval  12294  recosval  12295  efi4p  12296  resin4p  12297  recos4p  12298  resincl  12299  recoscl  12300  sinneg  12305  cosneg  12306  efival  12311  efmival  12312  efeul  12313  sinadd  12315  cosadd  12316  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  absef  12349  absefib  12350  efieq1re  12351  demoivre  12352  demoivreALT  12353  igz  12965  4sqlem17  12998  cnrehmeocntop  15353  sincn  15512  coscn  15513  efhalfpi  15542  ef2kpi  15549  efper  15550  sinperlem  15551  efimpi  15562  2sqlem2  15863  qdencn  16682