Axiom ax-icn 7739

Description: i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 7695. (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 7646	. 2 class i
2		cc 7642	. 2 class ℂ
3	1, 2	wcel 1481	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  7782  mulid1  7787  cnegexlem2  7962  cnegex  7964  0cnALT  7976  negicn  7987  ine0  8180  ixi  8369  rimul  8371  rereim  8372  apreap  8373  cru  8388  apreim  8389  mulreim  8390  apadd1  8394  apneg  8397  aprcl  8432  recextlem1  8436  recexaplem2  8437  recexap  8438  crap0  8740  cju  8743  it0e0  8965  2mulicn  8966  iap0  8967  2muliap0  8968  cnref1o  9469  irec  10423  i2  10424  i3  10425  i4  10426  iexpcyc  10428  imval  10654  imre  10655  reim  10656  crre  10661  crim  10662  remim  10664  mulreap  10668  cjreb  10670  recj  10671  reneg  10672  readd  10673  remullem  10675  imcj  10679  imneg  10680  imadd  10681  cjadd  10688  cjneg  10694  imval2  10698  rei  10703  imi  10704  cji  10706  cjreim  10707  cjreim2  10708  cjap  10710  cnrecnv  10714  rennim  10806  absi  10863  absreimsq  10871  absreim  10872  absimle  10888  climcvg1nlem  11150  sinval  11445  cosval  11446  sinf  11447  cosf  11448  tanval2ap  11456  tanval3ap  11457  resinval  11458  recosval  11459  efi4p  11460  resin4p  11461  recos4p  11462  resincl  11463  recoscl  11464  sinneg  11469  cosneg  11470  efival  11475  efmival  11476  efeul  11477  sinadd  11479  cosadd  11480  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  absef  11512  absefib  11513  efieq1re  11514  demoivre  11515  demoivreALT  11516  cnrehmeocntop  12801  sincn  12898  coscn  12899  efhalfpi  12928  ef2kpi  12935  efper  12936  sinperlem  12937  efimpi  12948  qdencn  13397