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

Theorem 3cn 9908
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 9907 . 2  |-  3  e.  RR
21recni 8939 1  |-  3  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1710   CCcc 8825   3c3 9886
This theorem is referenced by:  3m1e2  9932  3m1e2OLD  9933  3p2e5  9947  3p3e6  9948  4p4e8  9951  5p4e9  9954  6p4e10  9958  3t2e6  9964  3t3e9  9965  8th4div3  10027  halfpm6th  10028  9t8e72  10317  sq3  11293  expnass  11301  fac3  11388  sqrlem7  11830  caurcvgr  12243  sin01bnd  12562  cos01bnd  12563  cos1bnd  12564  cos2bnd  12565  cos01gt0  12568  rpnnen2lem3  12592  rpnnen2lem11  12600  3prm  12872  2exp16  13200  5prm  13207  7prm  13209  13prm  13214  17prm  13215  19prm  13216  37prm  13219  43prm  13220  83prm  13221  139prm  13222  163prm  13223  317prm  13224  631prm  13225  1259lem1  13226  1259lem2  13227  1259lem3  13228  1259lem4  13229  1259lem5  13230  1259prm  13231  2503lem1  13232  2503lem2  13233  2503lem3  13234  2503prm  13235  4001lem1  13236  4001lem2  13237  4001lem3  13238  4001lem4  13239  4001prm  13240  iblitg  19227  tangtx  19980  sincos6thpi  19990  sincos3rdpi  19991  pige3  19992  ang180lem2  20219  1cubrlem  20248  1cubr  20249  dcubic1lem  20250  dcubic2  20251  dcubic1  20252  dcubic  20253  mcubic  20254  cubic2  20255  cubic  20256  binom4  20257  quart1cl  20261  quart1lem  20262  quart1  20263  quartlem1  20264  quartlem3  20266  log2cnv  20351  log2tlbnd  20352  log2ublem2  20354  log2ublem3  20355  log2ub  20356  basellem5  20434  basellem8  20437  basellem9  20438  cht3  20523  ppiub  20555  chtub  20563  bclbnd  20631  bposlem6  20640  bposlem8  20642  bposlem9  20643  lgsdir2lem1  20674  lgsdir2lem5  20678  pntibndlem1  20850  pntlemk  20867  ex-opab  20931  ex-dvds  20947  sinccvglem  24409  4bc3eq4  24504  halfthird  24506  axlowdimlem16  25144  bpoly2  25351  bpoly3  25352  bpoly4  25353  itg2addnclem2  25493  itg2addnc  25494  heiborlem6  25863  heiborlem7  25864  jm2.23  26412  lhe4.4ex1a  26869  stoweidlem13  27085  stoweidlem26  27098  stoweidlem34  27106  wallispilem4  27140  wallispi2lem1  27143  fzo0to3tp  27459  fzo0to42pr  27460
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-resscn 8884  ax-1cn 8885  ax-icn 8886  ax-addcl 8887  ax-addrcl 8888  ax-mulcl 8889  ax-mulrcl 8890  ax-i2m1 8895  ax-1ne0 8896  ax-rrecex 8899  ax-cnre 8900
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-iota 5301  df-fv 5345  df-ov 5948  df-2 9894  df-3 9895
  Copyright terms: Public domain W3C validator