Theorem 2cn 7986

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 7985	. 2 |- 2 e. RR
2	1	recni 7039	1 |- 2 e. CC

Syntax hints:   e. wcel 1393   CCcc 6887   2c2 7964

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-resscn 6976  ax-1re 6978  ax-addrcl 6981

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-in 2924  df-ss 2931  df-2 7973

This theorem is referenced by:  2ex  7987  2cnd  7988  2m1e1  8034  3m1e2  8036  2p2e4  8037  times2  8039  2div2e1  8042  1p2e3  8044  3p3e6  8053  4p3e7  8055  5p3e8  8058  6p3e9  8062  7p3e10  8065  2t1e2  8068  2t2e4  8069  3t3e9  8072  2t0e0  8075  4d2e2  8076  2cnne0  8134  1mhlfehlf  8143  8th4div3  8144  halfpm6th  8145  2mulicn  8147  2muliap0  8149  halfcl  8151  half0  8153  2halves  8154  halfaddsub  8159  div4p1lem1div2  8177  zneo  8339  nneoor  8340  zeo  8343  4t4e16  8440  6t3e18  8445  7t7e49  8454  8t5e40  8458  9t9e81  8469  decbin0  8470  decbin2  8471  fztpval  8945  fz0tp  8981  fzo0to3tp  9075  2tnp1ge0ge0  9143  expubnd  9311  sq2  9349  cu2  9351  subsq2  9359  binom2sub  9364  binom3  9366  zesq  9367  crre  9457  addcj  9491  imval2  9494  resqrexlemover  9608  resqrexlemcalc1  9612  resqrexlemnm  9616  resqrexlemcvg  9617  amgm2  9714  sqr2irrlem  9877  ex-fl  9895  ex-ceil  9896