Axiom ax-icn 11068

Description: i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by Theorem axicn 11044. (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 11011	. 2 class i
2		cc 11007	. 2 class ℂ
3	1, 2	wcel 2109	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  11107  mulrid  11113  mul02lem2  11293  mul02  11294  addrid  11296  cnegex  11297  cnegex2  11298  0cnALT  11351  0cnALT2  11352  negicn  11364  ine0  11555  ixi  11749  recextlem1  11750  recextlem2  11751  recex  11752  rimul  12119  cru  12120  crne0  12121  cju  12124  it0e0  12347  2mulicn  12348  2muline0  12349  cnref1o  12886  irec  14108  i2  14109  i3  14110  i4  14111  iexpcyc  14114  crreczi  14135  imre  15015  reim  15016  crre  15021  crim  15022  remim  15024  mulre  15028  cjreb  15030  recj  15031  reneg  15032  readd  15033  remullem  15035  imcj  15039  imneg  15040  imadd  15041  cjadd  15048  cjneg  15054  imval2  15058  rei  15063  imi  15064  cji  15066  cjreim  15067  cjreim2  15068  rennim  15146  cnpart  15147  sqrtneglem  15173  sqrtneg  15174  sqrtm1  15182  absi  15193  absreimsq  15199  absreim  15200  absimle  15216  abs1m  15243  sqreulem  15267  sqreu  15268  bhmafibid1  15375  caucvgr  15583  sinf  16033  cosf  16034  tanval2  16042  tanval3  16043  resinval  16044  recosval  16045  efi4p  16046  resin4p  16047  recos4p  16048  resincl  16049  recoscl  16050  sinneg  16055  cosneg  16056  efival  16061  efmival  16062  sinhval  16063  coshval  16064  retanhcl  16068  tanhlt1  16069  tanhbnd  16070  efeul  16071  sinadd  16073  cosadd  16074  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  absef  16106  absefib  16107  efieq1re  16108  demoivre  16109  demoivreALT  16110  nthruc  16161  igz  16846  4sqlem17  16873  cnsubrg  21334  cnrehmeo  24849  cnrehmeoOLD  24850  cmodscexp  25019  ncvspi  25054  cphipval2  25139  4cphipval2  25140  cphipval  25141  itg0  25679  itgz  25680  itgcl  25683  ibl0  25686  iblcnlem1  25687  itgcnlem  25689  itgneg  25703  iblss  25704  iblss2  25705  itgss  25711  itgeqa  25713  iblconst  25717  itgconst  25718  itgadd  25724  iblabs  25728  iblabsr  25729  iblmulc2  25730  itgmulc2  25733  itgsplit  25735  dvsincos  25883  iaa  26231  sincn  26352  coscn  26353  efhalfpi  26378  ef2kpi  26385  efper  26386  sinperlem  26387  efimpi  26398  pige3ALT  26427  sineq0  26431  efeq1  26435  tanregt0  26446  efif1olem4  26452  efifo  26454  eff1olem  26455  circgrp  26459  circsubm  26460  logi  26494  logneg  26495  logm1  26496  lognegb  26497  eflogeq  26509  efiarg  26514  cosargd  26515  logimul  26521  logneg2  26522  abslogle  26525  tanarg  26526  logcn  26554  logf1o2  26557  cxpsqrtlem  26609  cxpsqrt  26610  root1eq1  26663  cxpeq  26665  ang180lem1  26717  ang180lem2  26718  ang180lem3  26719  ang180lem4  26720  1cubrlem  26749  1cubr  26750  asinlem  26776  asinlem2  26777  asinlem3a  26778  asinlem3  26779  asinf  26780  atandm2  26785  atandm3  26786  atanf  26788  asinneg  26794  efiasin  26796  sinasin  26797  asinsinlem  26799  asinsin  26800  asin1  26802  asinbnd  26807  cosasin  26812  atanneg  26815  atancj  26818  efiatan  26820  atanlogaddlem  26821  atanlogadd  26822  atanlogsublem  26823  atanlogsub  26824  efiatan2  26825  2efiatan  26826  tanatan  26827  cosatan  26829  atantan  26831  atanbndlem  26833  atans2  26839  dvatan  26843  atantayl  26845  atantayl2  26846  log2cnv  26852  basellem3  26991  2sqlem2  27327  nvpi  30611  ipval2  30651  4ipval2  30652  ipval3  30653  ipidsq  30654  dipcl  30656  dipcj  30658  dip0r  30661  dipcn  30664  ip1ilem  30770  ipasslem10  30783  ipasslem11  30784  polid2i  31101  polidi  31102  lnopeq0lem1  31949  lnopeq0i  31951  lnophmlem2  31961  re0cj  32687  pythagreim  32689  ccfldextdgrr  33639  constrelextdg2  33714  iconstr  33733  constrrecl  33736  constrimcl  33737  constrmulcl  33738  constrresqrtcl  33744  cos9thpiminplylem3  33751  cos9thpiminplylem4  33752  cos9thpiminplylem5  33753  cos9thpiminply  33755  cos9thpinconstrlem1  33756  cos9thpinconstrlem2  33757  cos9thpinconstr  33758  cnre2csqima  33878  efmul2picn  34564  itgexpif  34574  vtscl  34606  vtsprod  34607  circlemeth  34608  iexpire  35708  itgaddnc  37660  iblabsnc  37664  iblmulc2nc  37665  itgmulc2nc  37668  ftc1anclem3  37675  ftc1anclem6  37678  ftc1anclem7  37679  ftc1anclem8  37680  ftc1anc  37681  dvasin  37684  areacirclem4  37691  cntotbnd  37776  sn-1ne2  42238  0tie0  42288  it1ei  42289  1tiei  42290  retire  42292  ef11d  42312  cxp112d  42314  cxp111d  42315  cxpi11d  42316  re1m1e0m0  42370  sn-addlid  42377  sn-it0e0  42389  sn-negex12  42390  reixi  42396  sn-1ticom  42408  sn-mullid  42409  sn-it1ei  42410  ipiiie0  42411  sn-0tie0  42424  sn-mul02  42425  sn-itrere  42461  sn-retire  42462  cnreeu  42463  proot1ex  43169  sqrtcval  43614  sqrtcval2  43615  resqrtvalex  43618  imsqrtvalex  43619  sineq0ALT  44910  iblsplit  45947  sqrtnegnre  47291  requad01  47605  sinh-conventional  49724