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 ∈ ℂ

Detailed syntax breakdown of Axiom ax-icn

Step	Hyp	Ref	Expression
1		ci 8181	. 2 class i
2		cc 8177	. 2 class ℂ
3	1, 2	wcel 2209	1 wff i ∈ ℂ

This axiom is used by:  0cn  8318  mulrid  8323  cnegexlem2  8502  cnegex  8504  0cnALT  8516  negicn  8527  ine0  8721  ixi  8911  rimul  8913  rereim  8914  apreap  8915  cru  8930  apreim  8931  mulreim  8932  apadd1  8936  apneg  8939  aprcl  8974  aptap  8978  recextlem1  8979  recexaplem2  8980  recexap  8981  crap0  9288  cju  9291  it0e0  9526  2mulicn  9527  iap0  9528  2muliap0  9529  cnref1o  10051  irec  11076  i2  11077  i3  11078  i4  11079  iexpcyc  11081  imval  11615  imre  11616  reim  11617  crre  11622  crim  11623  remim  11625  mulreap  11629  cjreb  11631  recj  11632  reneg  11633  readd  11634  remullem  11636  imcj  11640  imneg  11641  imadd  11642  cjadd  11649  cjneg  11655  imval2  11659  sq01  11660  rei  11665  imi  11666  cji  11668  cjreim  11669  cjreim2  11670  cjap  11672  cnrecnv  11676  rennim  11768  absi  11825  absreimsq  11833  absreim  11834  absimle  11850  climcvg1nlem  12115  sinval  12469  cosval  12470  sinf  12471  cosf  12472  tanval2ap  12480  tanval3ap  12481  resinval  12482  recosval  12483  efi4p  12484  resin4p  12485  recos4p  12486  resincl  12487  recoscl  12488  sinneg  12493  cosneg  12494  efival  12499  efmival  12500  efeul  12501  sinadd  12503  cosadd  12504  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  absef  12537  absefib  12538  efieq1re  12539  demoivre  12540  demoivreALT  12541  igz  13153  4sqlem17  13186  cnrehmeocntop  15711  sincn  15870  coscn  15871  efhalfpi  15900  ef2kpi  15907  efper  15908  sinperlem  15909  efimpi  15920  2sqlem2  16234  qdencn  17072