Theorem 2cn 9214

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

Syntax hints:   ∈ wcel 2202  ℂcc 8030  2c2 9194

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213  df-2 9202

This theorem is referenced by:  2ex  9215  2cnd  9216  2m1e1  9261  3m1e2  9263  2p2e4  9270  times2  9272  2div2e1  9276  1p2e3  9278  3p3e6  9286  4p3e7  9288  5p3e8  9291  6p3e9  9294  2t1e2  9297  2t2e4  9298  3t3e9  9301  2t0e0  9303  4d2e2  9304  2cnne0  9353  1mhlfehlf  9362  8th4div3  9363  halfpm6th  9364  2mulicn  9366  2muliap0  9368  halfcl  9370  half0  9372  2halves  9373  halfaddsub  9378  div4p1lem1div2  9398  3halfnz  9577  zneo  9581  nneoor  9582  zeo  9585  7p3e10  9685  4t4e16  9709  6t3e18  9715  7t7e49  9724  8t5e40  9728  9t9e81  9739  decbin0  9750  decbin2  9751  halfthird  9753  fztpval  10318  fz0tp  10357  fz0to4untppr  10359  fzo0to3tp  10465  2tnp1ge0ge0  10562  fldiv4lem1div2  10568  expubnd  10859  sq2  10898  sq4e2t8  10900  cu2  10901  subsq2  10910  binom2sub  10916  binom3  10920  zesq  10921  fac2  10994  fac3  10995  faclbnd2  11005  bcn2  11027  4bc2eq6  11037  crre  11419  addcj  11453  imval2  11456  resqrexlemover  11572  resqrexlemcalc1  11576  resqrexlemnm  11580  resqrexlemcvg  11581  amgm2  11680  arisum  12061  arisum2  12062  geo2sum2  12078  geo2lim  12079  geoihalfsum  12085  efcllemp  12221  ege2le3  12234  tanval2ap  12276  tanval3ap  12277  efi4p  12280  efival  12295  sinadd  12299  cosadd  12300  sinmul  12307  cosmul  12308  cos2tsin  12314  ef01bndlem  12319  sin01bnd  12320  cos01bnd  12321  cos1bnd  12322  cos2bnd  12323  cos01gt0  12326  sin02gt0  12327  sin4lt0  12330  cos12dec  12331  egt2lt3  12343  odd2np1lem  12435  odd2np1  12436  ltoddhalfle  12456  halfleoddlt  12457  opoe  12458  omoe  12459  opeo  12460  omeo  12461  nno  12469  nn0o  12470  flodddiv4  12499  bits0  12511  bitsfzolem  12517  0bits  12522  bitsinv1  12525  6gcd4e2  12568  3lcm2e6woprm  12660  6lcm4e12  12661  sqrt2irrlem  12735  oddpwdclemodd  12746  pythagtriplem1  12840  pythagtriplem12  12850  pythagtriplem14  12852  4sqlem11  12976  4sqlem12  12977  dec5dvds  12987  dec2nprm  12990  2exp5  13007  2exp6  13008  2exp7  13009  2exp8  13010  2exp11  13011  2exp16  13012  maxcncf  15342  mincncf  15343  coscn  15497  sinhalfpilem  15518  cospi  15527  ef2pi  15532  ef2kpi  15533  efper  15534  sinperlem  15535  sin2kpi  15538  cos2kpi  15539  sin2pim  15540  cos2pim  15541  ptolemy  15551  sincosq3sgn  15555  sincosq4sgn  15556  sinq12gt0  15557  cosq23lt0  15560  coseq00topi  15562  tangtx  15565  sincos4thpi  15567  sincos6thpi  15569  sincos3rdpi  15570  pigt3  15571  abssinper  15573  coskpi  15575  cosq34lt1  15577  logsqrt  15650  2logb9irrALT  15701  1sgm2ppw  15722  perfect1  15725  perfectlem1  15726  perfectlem2  15727  perfect  15728  lgsdir2lem2  15761  gausslemma2dlem6  15799  lgsquadlem1  15809  lgsquadlem2  15810  lgsquad2lem2  15814  m1lgs  15817  2lgslem3a  15825  2lgslem3b  15826  2lgslem3c  15827  2lgslem3d  15828  2lgsoddprmlem2  15838  2lgsoddprmlem3c  15841  2lgsoddprmlem3d  15842  clwwlknonex2  16293  ex-fl  16338  ex-ceil  16339  ex-exp  16340  ex-fac  16341