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

Theorem 2cn 8060
Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
Assertion
Ref Expression
2cn 2 ∈ ℂ

Proof of Theorem 2cn
StepHypRef Expression
1 2re 8059 . 2 2 ∈ ℝ
21recni 7096 1 2 ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 1409  cc 6944  2c2 8039
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-resscn 7033  ax-1re 7035  ax-addrcl 7038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2951  df-ss 2958  df-2 8048
This theorem is referenced by:  2ex  8061  2cnd  8062  2m1e1  8106  3m1e2  8108  2p2e4  8109  times2  8111  2div2e1  8114  1p2e3  8116  3p3e6  8124  4p3e7  8126  5p3e8  8129  6p3e9  8132  2t1e2  8135  2t2e4  8136  3t3e9  8139  2t0e0  8141  4d2e2  8142  2cnne0  8190  1mhlfehlf  8199  8th4div3  8200  halfpm6th  8201  2mulicn  8203  2muliap0  8205  halfcl  8207  half0  8209  2halves  8210  halfaddsub  8215  div4p1lem1div2  8234  3halfnz  8394  zneo  8397  nneoor  8398  zeo  8401  7p3e10  8500  4t4e16  8524  6t3e18  8530  7t7e49  8539  8t5e40  8543  9t9e81  8554  decbin0  8565  decbin2  8566  fztpval  9046  fz0tp  9082  fzo0to3tp  9176  2tnp1ge0ge0  9250  expubnd  9476  sq2  9514  cu2  9516  subsq2  9525  binom2sub  9530  binom3  9533  zesq  9534  fac2  9598  fac3  9599  faclbnd2  9609  bcn2  9631  4bc2eq6  9641  crre  9684  addcj  9718  imval2  9721  resqrexlemover  9836  resqrexlemcalc1  9840  resqrexlemnm  9844  resqrexlemcvg  9845  amgm2  9944  odd2np1lem  10182  odd2np1  10183  ltoddhalfle  10204  halfleoddlt  10205  opoe  10206  omoe  10207  opeo  10208  omeo  10209  nno  10217  nn0o  10218  sqr2irrlem  10236  oddpwdclemodd  10246  ex-fl  10265  ex-ceil  10266  ex-fac  10267
  Copyright terms: Public domain W3C validator