Axiom ax-icn 8126

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

This axiom is referenced by:  0cn  8170  mulrid  8175  cnegexlem2  8354  cnegex  8356  0cnALT  8368  negicn  8379  ine0  8572  ixi  8762  rimul  8764  rereim  8765  apreap  8766  cru  8781  apreim  8782  mulreim  8783  apadd1  8787  apneg  8790  aprcl  8825  aptap  8829  recextlem1  8830  recexaplem2  8831  recexap  8832  crap0  9137  cju  9140  it0e0  9364  2mulicn  9365  iap0  9366  2muliap0  9367  cnref1o  9884  irec  10900  i2  10901  i3  10902  i4  10903  iexpcyc  10905  imval  11410  imre  11411  reim  11412  crre  11417  crim  11418  remim  11420  mulreap  11424  cjreb  11426  recj  11427  reneg  11428  readd  11429  remullem  11431  imcj  11435  imneg  11436  imadd  11437  cjadd  11444  cjneg  11450  imval2  11454  rei  11459  imi  11460  cji  11462  cjreim  11463  cjreim2  11464  cjap  11466  cnrecnv  11470  rennim  11562  absi  11619  absreimsq  11627  absreim  11628  absimle  11644  climcvg1nlem  11909  sinval  12262  cosval  12263  sinf  12264  cosf  12265  tanval2ap  12273  tanval3ap  12274  resinval  12275  recosval  12276  efi4p  12277  resin4p  12278  recos4p  12279  resincl  12280  recoscl  12281  sinneg  12286  cosneg  12287  efival  12292  efmival  12293  efeul  12294  sinadd  12296  cosadd  12297  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  absef  12330  absefib  12331  efieq1re  12332  demoivre  12333  demoivreALT  12334  igz  12946  4sqlem17  12979  cnrehmeocntop  15333  sincn  15492  coscn  15493  efhalfpi  15522  ef2kpi  15529  efper  15530  sinperlem  15531  efimpi  15542  2sqlem2  15843  qdencn  16631