Axiom ax-icn 11093

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

This axiom is referenced by:  0cn  11132  mulrid  11138  mul02lem2  11319  mul02  11320  addrid  11322  cnegex  11323  cnegex2  11324  0cnALT  11377  0cnALT2  11378  negicn  11390  ine0  11581  ixi  11775  recextlem1  11776  recextlem2  11777  recex  11778  rimul  12145  cru  12146  crne0  12147  cju  12150  it0e0  12395  2mulicn  12396  2muline0  12397  cnref1o  12930  irec  14158  i2  14159  i3  14160  i4  14161  iexpcyc  14164  crreczi  14185  imre  15065  reim  15066  crre  15071  crim  15072  remim  15074  mulre  15078  cjreb  15080  recj  15081  reneg  15082  readd  15083  remullem  15085  imcj  15089  imneg  15090  imadd  15091  cjadd  15098  cjneg  15104  imval2  15108  rei  15113  imi  15114  cji  15116  cjreim  15117  cjreim2  15118  rennim  15196  cnpart  15197  sqrtneglem  15223  sqrtneg  15224  sqrtm1  15232  absi  15243  absreimsq  15249  absreim  15250  absimle  15266  abs1m  15293  sqreulem  15317  sqreu  15318  bhmafibid1  15425  caucvgr  15633  sinf  16086  cosf  16087  tanval2  16095  tanval3  16096  resinval  16097  recosval  16098  efi4p  16099  resin4p  16100  recos4p  16101  resincl  16102  recoscl  16103  sinneg  16108  cosneg  16109  efival  16114  efmival  16115  sinhval  16116  coshval  16117  retanhcl  16121  tanhlt1  16122  tanhbnd  16123  efeul  16124  sinadd  16126  cosadd  16127  ef01bndlem  16146  sin01bnd  16147  cos01bnd  16148  absef  16159  absefib  16160  efieq1re  16161  demoivre  16162  demoivreALT  16163  nthruc  16214  igz  16900  4sqlem17  16927  cnsubrg  21405  cnrehmeo  24941  cmodscexp  25109  ncvspi  25144  cphipval2  25229  4cphipval2  25230  cphipval  25231  itg0  25768  itgz  25769  itgcl  25772  ibl0  25775  iblcnlem1  25776  itgcnlem  25778  itgneg  25792  iblss  25793  iblss2  25794  itgss  25800  itgeqa  25802  iblconst  25806  itgconst  25807  itgadd  25813  iblabs  25817  iblabsr  25818  iblmulc2  25819  itgmulc2  25822  itgsplit  25824  dvsincos  25969  iaa  26312  sincn  26430  coscn  26431  efhalfpi  26456  ef2kpi  26463  efper  26464  sinperlem  26465  efimpi  26476  pige3ALT  26505  sineq0  26509  efeq1  26513  tanregt0  26524  efif1olem4  26530  efifo  26532  eff1olem  26533  circgrp  26537  circsubm  26538  logi  26572  logneg  26573  logm1  26574  lognegb  26575  eflogeq  26587  efiarg  26592  cosargd  26593  logimul  26599  logneg2  26600  abslogle  26603  tanarg  26604  logcn  26632  logf1o2  26635  cxpsqrtlem  26687  cxpsqrt  26688  root1eq1  26740  cxpeq  26742  ang180lem1  26794  ang180lem2  26795  ang180lem3  26796  ang180lem4  26797  1cubrlem  26826  1cubr  26827  asinlem  26853  asinlem2  26854  asinlem3a  26855  asinlem3  26856  asinf  26857  atandm2  26862  atandm3  26863  atanf  26865  asinneg  26871  efiasin  26873  sinasin  26874  asinsinlem  26876  asinsin  26877  asin1  26879  asinbnd  26884  cosasin  26889  atanneg  26892  atancj  26895  efiatan  26897  atanlogaddlem  26898  atanlogadd  26899  atanlogsublem  26900  atanlogsub  26901  efiatan2  26902  2efiatan  26903  tanatan  26904  cosatan  26906  atantan  26908  atanbndlem  26910  atans2  26916  dvatan  26920  atantayl  26922  atantayl2  26923  log2cnv  26929  basellem3  27067  2sqlem2  27402  nvpi  30758  ipval2  30798  4ipval2  30799  ipval3  30800  ipidsq  30801  dipcl  30803  dipcj  30805  dip0r  30808  dipcn  30811  ip1ilem  30917  ipasslem10  30930  ipasslem11  30931  polid2i  31248  polidi  31249  lnopeq0lem1  32096  lnopeq0i  32098  lnophmlem2  32108  re0cj  32837  pythagreim  32839  ccfldextdgrr  33866  constrelextdg2  33941  iconstr  33960  constrrecl  33963  constrimcl  33964  constrmulcl  33965  constrresqrtcl  33971  cos9thpiminplylem3  33978  cos9thpiminplylem4  33979  cos9thpiminplylem5  33980  cos9thpiminply  33982  cos9thpinconstrlem1  33983  cos9thpinconstrlem2  33984  cos9thpinconstr  33985  cnre2csqima  34105  efmul2picn  34790  itgexpif  34800  vtscl  34832  vtsprod  34833  circlemeth  34834  iexpire  35976  itgaddnc  38060  iblabsnc  38064  iblmulc2nc  38065  itgmulc2nc  38068  ftc1anclem3  38075  ftc1anclem6  38078  ftc1anclem7  38079  ftc1anclem8  38080  ftc1anc  38081  dvasin  38084  areacirclem4  38091  cntotbnd  38176  sn-1ne2  42761  0tie0  42805  it1ei  42806  1tiei  42807  retire  42809  ef11d  42829  cxp112d  42831  cxp111d  42832  cxpi11d  42833  re1m1e0m0  42887  sn-addlid  42894  sn-it0e0  42906  sn-negex12  42907  reixi  42913  sn-1ticom  42925  sn-mullid  42926  sn-it1ei  42927  ipiiie0  42928  sn-0tie0  42954  sn-mul02  42955  sn-itrere  42991  sn-retire  42992  cnreeu  42993  proot1ex  43654  sqrtcval  44098  sqrtcval2  44099  resqrtvalex  44102  imsqrtvalex  44103  sineq0ALT  45393  iblsplit  46421  sqrtnegnre  47782  requad01  48124  sinh-conventional  50241