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

Theorem 3cn 10972
Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
Assertion
Ref Expression
3cn 3 ∈ ℂ

Proof of Theorem 3cn
StepHypRef Expression
1 3re 10971 . 2 3 ∈ ℝ
21recni 9931 1 3 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  cc 9813  3c3 10948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rrecex 9887  ax-cnre 9888
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-2 10956  df-3 10957
This theorem is referenced by:  3ex  10973  4m1e3  11015  3p2e5  11037  3p3e6  11038  4p4e8  11041  5p4e9  11044  6p4e10OLD  11048  3t1e3  11055  3t2e6  11056  3t3e9  11057  8th4div3  11129  halfpm6th  11130  6p4e10  11474  9t8e72  11545  halfthird  11561  fzo0to42pr  12422  sq3  12823  expnass  12832  fac3  12929  4bc3eq4  12977  sqrlem7  13837  caurcvgr  14252  bpoly2  14627  bpoly3  14628  bpoly4  14629  sin01bnd  14754  cos01bnd  14755  cos1bnd  14756  cos2bnd  14757  cos01gt0  14760  rpnnen2lem3  14784  rpnnen2lem11  14792  3dvdsdec  14892  3dvdsdecOLD  14893  3dvds2dec  14894  3dvds2decOLD  14895  3lcm2e6woprm  15166  prmo3  15583  2exp6  15633  2exp16  15635  7prm  15655  13prm  15661  17prm  15662  19prm  15663  37prm  15666  43prm  15667  83prm  15668  139prm  15669  163prm  15670  317prm  15671  631prm  15672  prmo4  15673  1259lem1  15676  1259lem2  15677  1259lem3  15678  1259lem4  15679  1259lem5  15680  1259prm  15681  2503lem1  15682  2503lem2  15683  2503lem3  15684  2503prm  15685  4001lem1  15686  4001lem2  15687  4001lem3  15688  4001lem4  15689  4001prm  15690  iblitg  23341  tangtx  24061  sincos6thpi  24071  sincos3rdpi  24072  pige3  24073  ang180lem2  24340  1cubr  24369  dcubic1lem  24370  dcubic2  24371  dcubic1  24372  dcubic  24373  mcubic  24374  cubic2  24375  cubic  24376  binom4  24377  quart1cl  24381  quart1lem  24382  quart1  24383  quartlem1  24384  quartlem3  24386  log2cnv  24471  log2tlbnd  24472  log2ublem2  24474  log2ublem3  24475  log2ub  24476  basellem5  24611  basellem8  24614  basellem9  24615  cht3  24699  ppiub  24729  chtub  24737  bclbnd  24805  bposlem6  24814  bposlem8  24816  bposlem9  24817  lgsdir2lem1  24850  lgsdir2lem5  24854  2lgslem3b  24922  2lgslem3d  24924  2lgsoddprmlem3c  24937  2lgsoddprmlem3d  24938  pntibndlem1  25078  pntlemk  25095  extwwlkfablem2  26605  ex-opab  26681  ex-exp  26699  ex-dvds  26705  ex-gcd  26706  ex-lcm  26707  ex-prmo  26708  ex-ind-dvds  26710  fib5  29794  fib6  29795  problem4  30816  problem5  30817  sinccvglem  30820  pigt3  32572  mblfinlem3  32618  itg2addnclem2  32632  itg2addnclem3  32633  heiborlem6  32785  heiborlem7  32786  jm2.23  36581  inductionexd  37473  lhe4.4ex1a  37550  stoweidlem13  38906  stoweidlem26  38919  stoweidlem34  38927  wallispilem4  38961  wallispi2lem1  38964  fmtno5lem1  40003  fmtno5lem2  40004  257prm  40011  fmtno4prmfac  40022  fmtno4nprmfac193  40024  139prmALT  40049  127prm  40053  mod42tp1mod8  40057  3exp4mod41  40071  41prothprmlem2  40073  6even  40158  gbpart8  40190  bgoldbwt  40199  bgoldbst  40200  evengpop3  40214  evengpoap3  40215  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  av-extwwlkfablem2  41510  2t6m3t4e0  41919  linevalexample  41978  zlmodzxzequa  42079  zlmodzxzequap  42082
  Copyright terms: Public domain W3C validator