Theorem 2cn 8992

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

Syntax hints:   ∈ wcel 2148  ℂcc 7811  2c2 8972

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7905  ax-1re 7907  ax-addrcl 7910

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144  df-2 8980

This theorem is referenced by:  2ex  8993  2cnd  8994  2m1e1  9039  3m1e2  9041  2p2e4  9048  times2  9050  2div2e1  9053  1p2e3  9055  3p3e6  9063  4p3e7  9065  5p3e8  9068  6p3e9  9071  2t1e2  9074  2t2e4  9075  3t3e9  9078  2t0e0  9080  4d2e2  9081  2cnne0  9130  1mhlfehlf  9139  8th4div3  9140  halfpm6th  9141  2mulicn  9143  2muliap0  9145  halfcl  9147  half0  9149  2halves  9150  halfaddsub  9155  div4p1lem1div2  9174  3halfnz  9352  zneo  9356  nneoor  9357  zeo  9360  7p3e10  9460  4t4e16  9484  6t3e18  9490  7t7e49  9499  8t5e40  9503  9t9e81  9514  decbin0  9525  decbin2  9526  halfthird  9528  fztpval  10085  fz0tp  10124  fz0to4untppr  10126  fzo0to3tp  10221  2tnp1ge0ge0  10303  expubnd  10579  sq2  10618  sq4e2t8  10620  cu2  10621  subsq2  10630  binom2sub  10636  binom3  10640  zesq  10641  fac2  10713  fac3  10714  faclbnd2  10724  bcn2  10746  4bc2eq6  10756  crre  10868  addcj  10902  imval2  10905  resqrexlemover  11021  resqrexlemcalc1  11025  resqrexlemnm  11029  resqrexlemcvg  11030  amgm2  11129  arisum  11508  arisum2  11509  geo2sum2  11525  geo2lim  11526  geoihalfsum  11532  efcllemp  11668  ege2le3  11681  tanval2ap  11723  tanval3ap  11724  efi4p  11727  efival  11742  sinadd  11746  cosadd  11747  sinmul  11754  cosmul  11755  cos2tsin  11761  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  cos1bnd  11769  cos2bnd  11770  cos01gt0  11772  sin02gt0  11773  sin4lt0  11776  cos12dec  11777  egt2lt3  11789  odd2np1lem  11879  odd2np1  11880  ltoddhalfle  11900  halfleoddlt  11901  opoe  11902  omoe  11903  opeo  11904  omeo  11905  nno  11913  nn0o  11914  flodddiv4  11941  6gcd4e2  11998  3lcm2e6woprm  12088  6lcm4e12  12089  sqrt2irrlem  12163  oddpwdclemodd  12174  pythagtriplem1  12267  pythagtriplem12  12277  pythagtriplem14  12279  coscn  14276  sinhalfpilem  14297  cospi  14306  ef2pi  14311  ef2kpi  14312  efper  14313  sinperlem  14314  sin2kpi  14317  cos2kpi  14318  sin2pim  14319  cos2pim  14320  ptolemy  14330  sincosq3sgn  14334  sincosq4sgn  14335  sinq12gt0  14336  cosq23lt0  14339  coseq00topi  14341  tangtx  14344  sincos4thpi  14346  sincos6thpi  14348  sincos3rdpi  14349  pigt3  14350  abssinper  14352  coskpi  14354  cosq34lt1  14356  logsqrt  14428  2logb9irrALT  14477  lgsdir2lem2  14515  m1lgs  14537  2lgsoddprmlem2  14539  2lgsoddprmlem3c  14542  2lgsoddprmlem3d  14543  ex-fl  14562  ex-ceil  14563  ex-exp  14564  ex-fac  14565