ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2cn Unicode version

Theorem 2cn 8428
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
StepHypRef Expression
1 2re 8427 . 2  |-  2  e.  RR
21recni 7444 1  |-  2  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1436   CCcc 7292   2c2 8407
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-resscn 7381  ax-1re 7383  ax-addrcl 7386
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-in 2994  df-ss 3001  df-2 8416
This theorem is referenced by:  2ex  8429  2cnd  8430  2m1e1  8474  3m1e2  8476  2p2e4  8477  times2  8479  2div2e1  8482  1p2e3  8484  3p3e6  8492  4p3e7  8494  5p3e8  8497  6p3e9  8500  2t1e2  8503  2t2e4  8504  3t3e9  8507  2t0e0  8509  4d2e2  8510  2cnne0  8558  1mhlfehlf  8567  8th4div3  8568  halfpm6th  8569  2mulicn  8571  2muliap0  8573  halfcl  8575  half0  8577  2halves  8578  halfaddsub  8583  div4p1lem1div2  8602  3halfnz  8776  zneo  8780  nneoor  8781  zeo  8784  7p3e10  8883  4t4e16  8907  6t3e18  8913  7t7e49  8922  8t5e40  8926  9t9e81  8937  decbin0  8948  decbin2  8949  fztpval  9427  fz0tp  9463  fzo0to3tp  9558  2tnp1ge0ge0  9636  expubnd  9910  sq2  9948  cu2  9950  subsq2  9959  binom2sub  9964  binom3  9967  zesq  9968  fac2  10035  fac3  10036  faclbnd2  10046  bcn2  10068  4bc2eq6  10078  crre  10186  addcj  10220  imval2  10223  resqrexlemover  10338  resqrexlemcalc1  10342  resqrexlemnm  10346  resqrexlemcvg  10347  amgm2  10446  odd2np1lem  10747  odd2np1  10748  ltoddhalfle  10768  halfleoddlt  10769  opoe  10770  omoe  10771  opeo  10772  omeo  10773  nno  10781  nn0o  10782  flodddiv4  10809  6gcd4e2  10859  3lcm2e6woprm  10943  6lcm4e12  10944  sqrt2irrlem  11015  oddpwdclemodd  11025  ex-fl  11091  ex-ceil  11092  ex-fac  11093
  Copyright terms: Public domain W3C validator