Theorem 2cn 9149

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 9148	. 2 ⊢ 2 ∈ ℝ
2	1	recni 8126	1 ⊢ 2 ∈ ℂ

Syntax hints:   ∈ wcel 2180  ℂcc 7965  2c2 9129

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191  ax-resscn 8059  ax-1re 8061  ax-addrcl 8064

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-in 3183  df-ss 3190  df-2 9137

This theorem is referenced by:  2ex  9150  2cnd  9151  2m1e1  9196  3m1e2  9198  2p2e4  9205  times2  9207  2div2e1  9211  1p2e3  9213  3p3e6  9221  4p3e7  9223  5p3e8  9226  6p3e9  9229  2t1e2  9232  2t2e4  9233  3t3e9  9236  2t0e0  9238  4d2e2  9239  2cnne0  9288  1mhlfehlf  9297  8th4div3  9298  halfpm6th  9299  2mulicn  9301  2muliap0  9303  halfcl  9305  half0  9307  2halves  9308  halfaddsub  9313  div4p1lem1div2  9333  3halfnz  9512  zneo  9516  nneoor  9517  zeo  9520  7p3e10  9620  4t4e16  9644  6t3e18  9650  7t7e49  9659  8t5e40  9663  9t9e81  9674  decbin0  9685  decbin2  9686  halfthird  9688  fztpval  10247  fz0tp  10286  fz0to4untppr  10288  fzo0to3tp  10392  2tnp1ge0ge0  10488  fldiv4lem1div2  10494  expubnd  10785  sq2  10824  sq4e2t8  10826  cu2  10827  subsq2  10836  binom2sub  10842  binom3  10846  zesq  10847  fac2  10920  fac3  10921  faclbnd2  10931  bcn2  10953  4bc2eq6  10963  crre  11334  addcj  11368  imval2  11371  resqrexlemover  11487  resqrexlemcalc1  11491  resqrexlemnm  11495  resqrexlemcvg  11496  amgm2  11595  arisum  11975  arisum2  11976  geo2sum2  11992  geo2lim  11993  geoihalfsum  11999  efcllemp  12135  ege2le3  12148  tanval2ap  12190  tanval3ap  12191  efi4p  12194  efival  12209  sinadd  12213  cosadd  12214  sinmul  12221  cosmul  12222  cos2tsin  12228  ef01bndlem  12233  sin01bnd  12234  cos01bnd  12235  cos1bnd  12236  cos2bnd  12237  cos01gt0  12240  sin02gt0  12241  sin4lt0  12244  cos12dec  12245  egt2lt3  12257  odd2np1lem  12349  odd2np1  12350  ltoddhalfle  12370  halfleoddlt  12371  opoe  12372  omoe  12373  opeo  12374  omeo  12375  nno  12383  nn0o  12384  flodddiv4  12413  bits0  12425  bitsfzolem  12431  0bits  12436  bitsinv1  12439  6gcd4e2  12482  3lcm2e6woprm  12574  6lcm4e12  12575  sqrt2irrlem  12649  oddpwdclemodd  12660  pythagtriplem1  12754  pythagtriplem12  12764  pythagtriplem14  12766  4sqlem11  12890  4sqlem12  12891  dec5dvds  12901  dec2nprm  12904  2exp5  12921  2exp6  12922  2exp7  12923  2exp8  12924  2exp11  12925  2exp16  12926  maxcncf  15254  mincncf  15255  coscn  15409  sinhalfpilem  15430  cospi  15439  ef2pi  15444  ef2kpi  15445  efper  15446  sinperlem  15447  sin2kpi  15450  cos2kpi  15451  sin2pim  15452  cos2pim  15453  ptolemy  15463  sincosq3sgn  15467  sincosq4sgn  15468  sinq12gt0  15469  cosq23lt0  15472  coseq00topi  15474  tangtx  15477  sincos4thpi  15479  sincos6thpi  15481  sincos3rdpi  15482  pigt3  15483  abssinper  15485  coskpi  15487  cosq34lt1  15489  logsqrt  15562  2logb9irrALT  15613  1sgm2ppw  15634  perfect1  15637  perfectlem1  15638  perfectlem2  15639  perfect  15640  lgsdir2lem2  15673  gausslemma2dlem6  15711  lgsquadlem1  15721  lgsquadlem2  15722  lgsquad2lem2  15726  m1lgs  15729  2lgslem3a  15737  2lgslem3b  15738  2lgslem3c  15739  2lgslem3d  15740  2lgsoddprmlem2  15750  2lgsoddprmlem3c  15753  2lgsoddprmlem3d  15754  ex-fl  15999  ex-ceil  16000  ex-exp  16001  ex-fac  16002