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

Theorem 3cn 10077
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 10076 . 2  |-  3  e.  RR
21recni 9107 1  |-  3  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   CCcc 8993   3c3 10055
This theorem is referenced by:  3m1e2  10101  3m1e2OLD  10102  3p2e5  10116  3p3e6  10117  4p4e8  10120  5p4e9  10123  6p4e10  10127  3t2e6  10133  3t3e9  10134  8th4div3  10196  halfpm6th  10197  9t8e72  10488  fzo0to42pr  11191  sq3  11483  expnass  11491  fac3  11578  sqrlem7  12059  caurcvgr  12472  sin01bnd  12791  cos01bnd  12792  cos1bnd  12793  cos2bnd  12794  cos01gt0  12797  rpnnen2lem3  12821  rpnnen2lem11  12829  2exp16  13429  5prm  13436  7prm  13438  13prm  13443  17prm  13444  19prm  13445  37prm  13448  43prm  13449  83prm  13450  139prm  13451  163prm  13452  317prm  13453  631prm  13454  1259lem1  13455  1259lem2  13456  1259lem3  13457  1259lem4  13458  1259lem5  13459  1259prm  13460  2503lem1  13461  2503lem2  13462  2503lem3  13463  2503prm  13464  4001lem1  13465  4001lem2  13466  4001lem3  13467  4001lem4  13468  4001prm  13469  iblitg  19663  tangtx  20418  sincos6thpi  20428  sincos3rdpi  20429  pige3  20430  ang180lem2  20657  1cubr  20687  dcubic1lem  20688  dcubic2  20689  dcubic1  20690  dcubic  20691  mcubic  20692  cubic2  20693  cubic  20694  binom4  20695  quart1cl  20699  quart1lem  20700  quart1  20701  quartlem1  20702  quartlem3  20704  log2cnv  20789  log2tlbnd  20790  log2ublem2  20792  log2ublem3  20793  log2ub  20794  basellem5  20872  basellem8  20875  basellem9  20876  cht3  20961  ppiub  20993  chtub  21001  bclbnd  21069  bposlem6  21078  bposlem8  21080  bposlem9  21081  lgsdir2lem1  21112  lgsdir2lem5  21116  pntibndlem1  21288  pntlemk  21305  ex-opab  21745  ex-dvds  21761  sinccvglem  25114  4bc3eq4  25208  halfthird  25210  bpoly2  26108  bpoly3  26109  bpoly4  26110  mblfinlem3  26257  itg2addnclem2  26271  itg2addnclem3  26272  heiborlem6  26539  heiborlem7  26540  jm2.23  27081  lhe4.4ex1a  27537  stoweidlem13  27752  stoweidlem26  27765  stoweidlem34  27773  wallispilem4  27807  wallispi2lem1  27810
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-i2m1 9063  ax-1ne0 9064  ax-rrecex 9067  ax-cnre 9068
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465  df-ov 6087  df-2 10063  df-3 10064
  Copyright terms: Public domain W3C validator