Theorem 2cn 8110

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

Syntax hints:   ∈ wcel 1433  ℂcc 6979  2c2 8089

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-resscn 7068  ax-1re 7070  ax-addrcl 7073

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-in 2979  df-ss 2986  df-2 8098

This theorem is referenced by:  2ex  8111  2cnd  8112  2m1e1  8156  3m1e2  8158  2p2e4  8159  times2  8161  2div2e1  8164  1p2e3  8166  3p3e6  8174  4p3e7  8176  5p3e8  8179  6p3e9  8182  2t1e2  8185  2t2e4  8186  3t3e9  8189  2t0e0  8191  4d2e2  8192  2cnne0  8240  1mhlfehlf  8249  8th4div3  8250  halfpm6th  8251  2mulicn  8253  2muliap0  8255  halfcl  8257  half0  8259  2halves  8260  halfaddsub  8265  div4p1lem1div2  8284  3halfnz  8444  zneo  8448  nneoor  8449  zeo  8452  7p3e10  8551  4t4e16  8575  6t3e18  8581  7t7e49  8590  8t5e40  8594  9t9e81  8605  decbin0  8616  decbin2  8617  fztpval  9100  fz0tp  9135  fzo0to3tp  9228  2tnp1ge0ge0  9303  expubnd  9533  sq2  9571  cu2  9573  subsq2  9582  binom2sub  9587  binom3  9590  zesq  9591  fac2  9658  fac3  9659  faclbnd2  9669  bcn2  9691  4bc2eq6  9701  crre  9744  addcj  9778  imval2  9781  resqrexlemover  9896  resqrexlemcalc1  9900  resqrexlemnm  9904  resqrexlemcvg  9905  amgm2  10004  odd2np1lem  10271  odd2np1  10272  ltoddhalfle  10293  halfleoddlt  10294  opoe  10295  omoe  10296  opeo  10297  omeo  10298  nno  10306  nn0o  10307  flodddiv4  10334  6gcd4e2  10384  3lcm2e6woprm  10468  6lcm4e12  10469  sqrt2irrlem  10540  oddpwdclemodd  10550  ex-fl  10563  ex-ceil  10564  ex-fac  10565