MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3cn Unicode version

Theorem 3cn 9834
Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
Assertion
Ref Expression
3cn  |-  3  e.  CC

Proof of Theorem 3cn
StepHypRef Expression
1 3re 9833 . 2  |-  3  e.  RR
21recni 8865 1  |-  3  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   CCcc 8751   3c3 9812
This theorem is referenced by:  3p2e5  9871  3p3e6  9872  4p4e8  9875  5p4e9  9878  6p4e10  9882  3t2e6  9888  3t3e9  9889  8th4div3  9951  halfpm6th  9952  9t8e72  10241  sq3  11216  expnass  11224  fac3  11311  sqrlem7  11750  caurcvgr  12162  sin01bnd  12481  cos01bnd  12482  cos1bnd  12483  cos2bnd  12484  cos01gt0  12487  rpnnen2lem3  12511  rpnnen2lem11  12519  3prm  12791  2exp16  13119  5prm  13126  7prm  13128  13prm  13133  17prm  13134  19prm  13135  37prm  13138  43prm  13139  83prm  13140  139prm  13141  163prm  13142  317prm  13143  631prm  13144  1259lem1  13145  1259lem2  13146  1259lem3  13147  1259lem4  13148  1259lem5  13149  1259prm  13150  2503lem1  13151  2503lem2  13152  2503lem3  13153  2503prm  13154  4001lem1  13155  4001lem2  13156  4001lem3  13157  4001lem4  13158  4001prm  13159  iblitg  19139  tangtx  19889  sincos6thpi  19899  sincos3rdpi  19900  pige3  19901  ang180lem2  20124  1cubrlem  20153  1cubr  20154  dcubic1lem  20155  dcubic2  20156  dcubic1  20157  dcubic  20158  mcubic  20159  cubic2  20160  cubic  20161  binom4  20162  quart1cl  20166  quart1lem  20167  quart1  20168  quartlem1  20169  quartlem3  20171  log2cnv  20256  log2tlbnd  20257  log2ublem2  20259  log2ublem3  20260  log2ub  20261  basellem5  20338  basellem8  20341  basellem9  20342  cht3  20427  ppiub  20459  chtub  20467  bclbnd  20535  bposlem6  20544  bposlem8  20546  bposlem9  20547  lgsdir2lem1  20578  lgsdir2lem5  20582  pntibndlem1  20754  pntlemk  20771  ex-opab  20835  ex-dvds  20851  sinccvglem  24020  4bc3eq4  24113  halfthird  24115  axlowdimlem16  24657  bpoly2  24864  bpoly3  24865  bpoly4  24866  itg2addnclem2  25004  itg2addnc  25005  2eq3m1  25282  cntrset  25705  heiborlem6  26643  heiborlem7  26644  jm2.23  27192  lhe4.4ex1a  27649  stoweidlem13  27865  stoweidlem26  27878  stoweidlem34  27886  wallispilem4  27920  wallispi2lem1  27923  fzo0to3tp  28210  fzo0to42pr  28211
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-i2m1 8821  ax-1ne0 8822  ax-rrecex 8825  ax-cnre 8826
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-2 9820  df-3 9821
  Copyright terms: Public domain W3C validator