Theorem 2cn 8213

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

Assertion

Ref	Expression
2cn	|- 2 e. CC

Proof of Theorem 2cn

Step	Hyp	Ref	Expression
1		2re 8212	. 2 |- 2 e. RR
2	1	recni 7229	1 |- 2 e. CC

Syntax hints:   e. wcel 1434   CCcc 7077   2c2 8192

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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-resscn 7166  ax-1re 7168  ax-addrcl 7171

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-in 2989  df-ss 2996  df-2 8201

This theorem is referenced by:  2ex  8214  2cnd  8215  2m1e1  8259  3m1e2  8261  2p2e4  8262  times2  8264  2div2e1  8267  1p2e3  8269  3p3e6  8277  4p3e7  8279  5p3e8  8282  6p3e9  8285  2t1e2  8288  2t2e4  8289  3t3e9  8292  2t0e0  8294  4d2e2  8295  2cnne0  8343  1mhlfehlf  8352  8th4div3  8353  halfpm6th  8354  2mulicn  8356  2muliap0  8358  halfcl  8360  half0  8362  2halves  8363  halfaddsub  8368  div4p1lem1div2  8387  3halfnz  8561  zneo  8565  nneoor  8566  zeo  8569  7p3e10  8668  4t4e16  8692  6t3e18  8698  7t7e49  8707  8t5e40  8711  9t9e81  8722  decbin0  8733  decbin2  8734  fztpval  9212  fz0tp  9248  fzo0to3tp  9341  2tnp1ge0ge0  9419  expubnd  9666  sq2  9704  cu2  9706  subsq2  9715  binom2sub  9720  binom3  9723  zesq  9724  fac2  9791  fac3  9792  faclbnd2  9802  bcn2  9824  4bc2eq6  9834  crre  9929  addcj  9963  imval2  9966  resqrexlemover  10081  resqrexlemcalc1  10085  resqrexlemnm  10089  resqrexlemcvg  10090  amgm2  10189  odd2np1lem  10463  odd2np1  10464  ltoddhalfle  10484  halfleoddlt  10485  opoe  10486  omoe  10487  opeo  10488  omeo  10489  nno  10497  nn0o  10498  flodddiv4  10525  6gcd4e2  10575  3lcm2e6woprm  10659  6lcm4e12  10660  sqrt2irrlem  10731  oddpwdclemodd  10741  ex-fl  10807  ex-ceil  10808  ex-fac  10809