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

Theorem 3cn 10036
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 10035 . 2  |-  3  e.  RR
21recni 9066 1  |-  3  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   CCcc 8952   3c3 10014
This theorem is referenced by:  3m1e2  10060  3m1e2OLD  10061  3p2e5  10075  3p3e6  10076  4p4e8  10079  5p4e9  10082  6p4e10  10086  3t2e6  10092  3t3e9  10093  8th4div3  10155  halfpm6th  10156  9t8e72  10447  fzo0to42pr  11149  sq3  11441  expnass  11449  fac3  11536  sqrlem7  12017  caurcvgr  12430  sin01bnd  12749  cos01bnd  12750  cos1bnd  12751  cos2bnd  12752  cos01gt0  12755  rpnnen2lem3  12779  rpnnen2lem11  12787  2exp16  13387  5prm  13394  7prm  13396  13prm  13401  17prm  13402  19prm  13403  37prm  13406  43prm  13407  83prm  13408  139prm  13409  163prm  13410  317prm  13411  631prm  13412  1259lem1  13413  1259lem2  13414  1259lem3  13415  1259lem4  13416  1259lem5  13417  1259prm  13418  2503lem1  13419  2503lem2  13420  2503lem3  13421  2503prm  13422  4001lem1  13423  4001lem2  13424  4001lem3  13425  4001lem4  13426  4001prm  13427  iblitg  19621  tangtx  20374  sincos6thpi  20384  sincos3rdpi  20385  pige3  20386  ang180lem2  20613  1cubr  20643  dcubic1lem  20644  dcubic2  20645  dcubic1  20646  dcubic  20647  mcubic  20648  cubic2  20649  cubic  20650  binom4  20651  quart1cl  20655  quart1lem  20656  quart1  20657  quartlem1  20658  quartlem3  20660  log2cnv  20745  log2tlbnd  20746  log2ublem2  20748  log2ublem3  20749  log2ub  20750  basellem5  20828  basellem8  20831  basellem9  20832  cht3  20917  ppiub  20949  chtub  20957  bclbnd  21025  bposlem6  21034  bposlem8  21036  bposlem9  21037  lgsdir2lem1  21068  lgsdir2lem5  21072  pntibndlem1  21244  pntlemk  21261  ex-opab  21701  ex-dvds  21717  sinccvglem  25070  4bc3eq4  25164  halfthird  25166  bpoly2  26015  bpoly3  26016  bpoly4  26017  mblfinlem2  26152  itg2addnclem2  26164  itg2addnclem3  26165  heiborlem6  26423  heiborlem7  26424  jm2.23  26965  lhe4.4ex1a  27422  stoweidlem13  27637  stoweidlem26  27650  stoweidlem34  27658  wallispilem4  27692  wallispi2lem1  27695
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-resscn 9011  ax-1cn 9012  ax-icn 9013  ax-addcl 9014  ax-addrcl 9015  ax-mulcl 9016  ax-mulrcl 9017  ax-i2m1 9022  ax-1ne0 9023  ax-rrecex 9026  ax-cnre 9027
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-iota 5385  df-fv 5429  df-ov 6051  df-2 10022  df-3 10023
  Copyright terms: Public domain W3C validator