Theorem 2cn 9189

Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)

Assertion

Ref	Expression
2cn	⊢ 2 ∈ ℂ

Proof of Theorem 2cn

Step	Hyp	Ref	Expression
1		2re 9188	. 2 ⊢ 2 ∈ ℝ
2	1	recni 8166	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2200  ℂcc 8005  2c2 9169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8099  ax-1re 8101  ax-addrcl 8104

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-2 9177

This theorem is referenced by:  2ex  9190  2cnd  9191  2m1e1  9236  3m1e2  9238  2p2e4  9245  times2  9247  2div2e1  9251  1p2e3  9253  3p3e6  9261  4p3e7  9263  5p3e8  9266  6p3e9  9269  2t1e2  9272  2t2e4  9273  3t3e9  9276  2t0e0  9278  4d2e2  9279  2cnne0  9328  1mhlfehlf  9337  8th4div3  9338  halfpm6th  9339  2mulicn  9341  2muliap0  9343  halfcl  9345  half0  9347  2halves  9348  halfaddsub  9353  div4p1lem1div2  9373  3halfnz  9552  zneo  9556  nneoor  9557  zeo  9560  7p3e10  9660  4t4e16  9684  6t3e18  9690  7t7e49  9699  8t5e40  9703  9t9e81  9714  decbin0  9725  decbin2  9726  halfthird  9728  fztpval  10287  fz0tp  10326  fz0to4untppr  10328  fzo0to3tp  10433  2tnp1ge0ge0  10529  fldiv4lem1div2  10535  expubnd  10826  sq2  10865  sq4e2t8  10867  cu2  10868  subsq2  10877  binom2sub  10883  binom3  10887  zesq  10888  fac2  10961  fac3  10962  faclbnd2  10972  bcn2  10994  4bc2eq6  11004  crre  11376  addcj  11410  imval2  11413  resqrexlemover  11529  resqrexlemcalc1  11533  resqrexlemnm  11537  resqrexlemcvg  11538  amgm2  11637  arisum  12017  arisum2  12018  geo2sum2  12034  geo2lim  12035  geoihalfsum  12041  efcllemp  12177  ege2le3  12190  tanval2ap  12232  tanval3ap  12233  efi4p  12236  efival  12251  sinadd  12255  cosadd  12256  sinmul  12263  cosmul  12264  cos2tsin  12270  ef01bndlem  12275  sin01bnd  12276  cos01bnd  12277  cos1bnd  12278  cos2bnd  12279  cos01gt0  12282  sin02gt0  12283  sin4lt0  12286  cos12dec  12287  egt2lt3  12299  odd2np1lem  12391  odd2np1  12392  ltoddhalfle  12412  halfleoddlt  12413  opoe  12414  omoe  12415  opeo  12416  omeo  12417  nno  12425  nn0o  12426  flodddiv4  12455  bits0  12467  bitsfzolem  12473  0bits  12478  bitsinv1  12481  6gcd4e2  12524  3lcm2e6woprm  12616  6lcm4e12  12617  sqrt2irrlem  12691  oddpwdclemodd  12702  pythagtriplem1  12796  pythagtriplem12  12806  pythagtriplem14  12808  4sqlem11  12932  4sqlem12  12933  dec5dvds  12943  dec2nprm  12946  2exp5  12963  2exp6  12964  2exp7  12965  2exp8  12966  2exp11  12967  2exp16  12968  maxcncf  15297  mincncf  15298  coscn  15452  sinhalfpilem  15473  cospi  15482  ef2pi  15487  ef2kpi  15488  efper  15489  sinperlem  15490  sin2kpi  15493  cos2kpi  15494  sin2pim  15495  cos2pim  15496  ptolemy  15506  sincosq3sgn  15510  sincosq4sgn  15511  sinq12gt0  15512  cosq23lt0  15515  coseq00topi  15517  tangtx  15520  sincos4thpi  15522  sincos6thpi  15524  sincos3rdpi  15525  pigt3  15526  abssinper  15528  coskpi  15530  cosq34lt1  15532  logsqrt  15605  2logb9irrALT  15656  1sgm2ppw  15677  perfect1  15680  perfectlem1  15681  perfectlem2  15682  perfect  15683  lgsdir2lem2  15716  gausslemma2dlem6  15754  lgsquadlem1  15764  lgsquadlem2  15765  lgsquad2lem2  15769  m1lgs  15772  2lgslem3a  15780  2lgslem3b  15781  2lgslem3c  15782  2lgslem3d  15783  2lgsoddprmlem2  15793  2lgsoddprmlem3c  15796  2lgsoddprmlem3d  15797  ex-fl  16113  ex-ceil  16114  ex-exp  16115  ex-fac  16116