Axiom ax-icn 11165

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

This axiom is used by:  0cn  11204  mulrid  11212  mul02lem2  11393  mul02  11394  addrid  11396  cnegex  11397  cnegex2  11398  0cnALT  11451  0cnALT2  11452  negicn  11464  ine0  11655  ixi  11849  recextlem1  11850  recextlem2  11851  recex  11852  rimul  12215  cru  12216  crne0  12217  cju  12220  it0e0  12473  2mulicn  12474  2muline0  12475  cnref1o  13015  irec  14244  i2  14245  i3  14246  i4  14247  iexpcyc  14250  crreczi  14271  imre  15166  reim  15167  crre  15172  crim  15173  remim  15175  mulre  15179  cjreb  15181  recj  15182  reneg  15183  readd  15184  remullem  15186  imcj  15190  imneg  15191  imadd  15192  cjadd  15199  cjneg  15205  imval2  15209  rei  15214  imi  15215  cji  15217  cjreim  15218  cjreim2  15219  rennim  15297  cnpart  15298  sqrtneglem  15324  sqrtneg  15325  sqrtm1  15333  absi  15344  absreimsq  15350  absreim  15351  absimle  15367  abs1m  15394  sqreulem  15418  sqreu  15419  bhmafibid1  15526  caucvgr  15734  sinf  16186  cosf  16187  tanval2  16195  tanval3  16196  resinval  16197  recosval  16198  efi4p  16199  resin4p  16200  recos4p  16201  resincl  16202  recoscl  16203  sinneg  16208  cosneg  16209  efival  16214  efmival  16215  sinhval  16216  coshval  16217  retanhcl  16221  tanhlt1  16222  tanhbnd  16223  efeul  16224  sinadd  16226  cosadd  16227  ef01bndlem  16246  sin01bnd  16247  cos01bnd  16248  absef  16259  absefib  16260  efieq1re  16261  demoivre  16262  demoivreALT  16263  nthruc  16314  igz  17000  4sqlem17  17027  cnsubrg  21588  cnrehmeo  25123  cmodscexp  25291  ncvspi  25326  cphipval2  25411  4cphipval2  25412  cphipval  25413  itg0  25950  itgz  25951  itgcl  25954  ibl0  25957  iblcnlem1  25958  itgcnlem  25960  itgneg  25974  iblss  25975  iblss2  25976  itgss  25982  itgeqa  25984  iblconst  25988  itgconst  25989  itgadd  25995  iblabs  25999  iblabsr  26000  iblmulc2  26001  itgmulc2  26004  itgsplit  26006  dvsincos  26151  iaa  26499  sincn  26618  coscn  26619  efhalfpi  26647  ef2kpi  26654  efper  26655  sinperlem  26656  efimpi  26667  pige3ALT  26696  sineq0  26700  efeq1  26704  tanregt0  26715  efif1olem4  26721  efifo  26723  eff1olem  26724  circgrp  26728  circsubm  26729  logi  26763  logneg  26764  logm1  26765  lognegb  26766  eflogeq  26778  efiarg  26783  cosargd  26784  logimul  26790  logneg2  26791  abslogle  26794  tanarg  26795  logcn  26823  logf1o2  26826  cxpsqrtlem  26878  cxpsqrt  26879  root1eq1  26931  cxpeq  26933  ang180lem1  26985  ang180lem2  26986  ang180lem3  26987  ang180lem4  26988  1cubrlem  27017  1cubr  27018  asinlem  27044  asinlem2  27045  asinlem3a  27046  asinlem3  27047  asinf  27048  atandm2  27053  atandm3  27054  atanf  27056  asinneg  27062  efiasin  27064  sinasin  27065  asinsinlem  27067  asinsin  27068  asin1  27070  asinbnd  27075  cosasin  27080  atanneg  27083  atancj  27086  efiatan  27088  atanlogaddlem  27089  atanlogadd  27090  atanlogsublem  27091  atanlogsub  27092  efiatan2  27093  2efiatan  27094  tanatan  27095  cosatan  27097  atantan  27099  atanbndlem  27101  atans2  27107  dvatan  27111  atantayl  27113  atantayl2  27114  log2cnv  27120  basellem3  27258  2sqlem2  27593  nvpi  31030  ipval2  31070  4ipval2  31071  ipval3  31072  ipidsq  31073  dipcl  31075  dipcj  31077  dip0r  31080  dipcn  31083  ip1ilem  31189  ipasslem10  31202  ipasslem11  31203  polid2i  31520  polidi  31521  lnopeq0lem1  32368  lnopeq0i  32370  lnophmlem2  32380  re0cj  33099  pythagreim  33101  ccfldextdgrr  34071  constrelextdg2  34146  iconstr  34165  constrrecl  34168  constrimcl  34169  constrmulcl  34170  constrresqrtcl  34176  cos9thpiminplylem3  34183  cos9thpiminplylem4  34184  cos9thpiminplylem5  34185  cos9thpiminply  34187  cos9thpinconstrlem1  34188  cos9thpinconstrlem2  34189  cos9thpinconstr  34190  cnre2csqima  34310  efmul2picn  34992  itgexpif  35002  vtscl  35034  vtsprod  35035  circlemeth  35036  iexpire  36235  itgaddnc  38359  iblabsnc  38363  iblmulc2nc  38364  itgmulc2nc  38367  ftc1anclem3  38374  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  dvasin  38383  areacirclem4  38390  cntotbnd  38475  sn-1ne2  43060  0tie0  43104  it1ei  43105  1tiei  43106  retire  43108  ef11d  43128  cxp112d  43130  cxp111d  43131  cxpi11d  43132  re1m1e0m0  43186  sn-addlid  43193  sn-it0e0  43205  sn-negex12  43206  reixi  43212  sn-1ticom  43224  sn-mullid  43225  sn-it1ei  43226  ipiiie0  43227  sn-0tie0  43253  sn-mul02  43254  sn-itrere  43290  sn-retire  43291  cnreeu  43292  proot1ex  43951  sqrtcval  44395  sqrtcval2  44396  resqrtvalex  44399  imsqrtvalex  44400  sineq0ALT  45673  iblsplit  46708  sqrtnegnre  48072  requad01  48414  sinh-conventional  50545