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

Theorem 3cn 11047
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 11046 . 2 3 ∈ ℝ
21recni 10004 1 3 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  cc 9886  3c3 11023
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-i2m1 9956  ax-1ne0 9957  ax-rrecex 9960  ax-cnre 9961
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5815  df-fv 5860  df-ov 6613  df-2 11031  df-3 11032
This theorem is referenced by:  3ex  11048  4m1e3  11090  3p2e5  11112  3p3e6  11113  4p4e8  11116  5p4e9  11119  6p4e10OLD  11123  3t1e3  11130  3t2e6  11131  3t3e9  11132  8th4div3  11204  halfpm6th  11205  6p4e10  11550  9t8e72  11621  halfthird  11637  fzo0to42pr  12504  sq3  12909  expnass  12918  fac3  13015  4bc3eq4  13063  sqrlem7  13931  caurcvgr  14346  bpoly2  14724  bpoly3  14725  bpoly4  14726  sin01bnd  14851  cos01bnd  14852  cos1bnd  14853  cos2bnd  14854  cos01gt0  14857  rpnnen2lem3  14881  rpnnen2lem11  14889  3dvdsdec  14989  3dvdsdecOLD  14990  3dvds2dec  14991  3dvds2decOLD  14992  3lcm2e6woprm  15263  prmo3  15680  2exp6  15730  2exp16  15732  7prm  15752  13prm  15758  17prm  15759  19prm  15760  37prm  15763  43prm  15764  83prm  15765  139prm  15766  163prm  15767  317prm  15768  631prm  15769  prmo4  15770  1259lem1  15773  1259lem2  15774  1259lem3  15775  1259lem4  15776  1259lem5  15777  1259prm  15778  2503lem1  15779  2503lem2  15780  2503lem3  15781  2503prm  15782  4001lem1  15783  4001lem2  15784  4001lem3  15785  4001lem4  15786  4001prm  15787  iblitg  23458  tangtx  24178  sincos6thpi  24188  sincos3rdpi  24189  pige3  24190  ang180lem2  24457  1cubr  24486  dcubic1lem  24487  dcubic2  24488  dcubic1  24489  dcubic  24490  mcubic  24491  cubic2  24492  cubic  24493  binom4  24494  quart1cl  24498  quart1lem  24499  quart1  24500  quartlem1  24501  quartlem3  24503  log2cnv  24588  log2tlbnd  24589  log2ublem2  24591  log2ublem3  24592  log2ub  24593  basellem5  24728  basellem8  24731  basellem9  24732  cht3  24816  ppiub  24846  chtub  24854  bclbnd  24922  bposlem6  24931  bposlem8  24933  bposlem9  24934  lgsdir2lem1  24967  lgsdir2lem5  24971  2lgslem3b  25039  2lgslem3d  25041  2lgsoddprmlem3c  25054  2lgsoddprmlem3d  25055  pntibndlem1  25195  pntlemk  25212  extwwlkfablem2  27085  ex-opab  27160  ex-exp  27178  ex-dvds  27184  ex-gcd  27185  ex-lcm  27186  ex-prmo  27187  ex-ind-dvds  27189  fib5  30272  fib6  30273  problem4  31305  problem5  31306  sinccvglem  31309  pigt3  33069  mblfinlem3  33115  itg2addnclem2  33129  itg2addnclem3  33130  heiborlem6  33282  heiborlem7  33283  jm2.23  37078  inductionexd  37970  lhe4.4ex1a  38045  stoweidlem13  39563  stoweidlem26  39576  stoweidlem34  39584  wallispilem4  39618  wallispi2lem1  39621  fmtno5lem1  40790  fmtno5lem2  40791  257prm  40798  fmtno4prmfac  40809  fmtno4nprmfac193  40811  139prmALT  40836  127prm  40840  mod42tp1mod8  40844  3exp4mod41  40858  41prothprmlem2  40860  6even  40945  gbpart8  40977  bgoldbwt  40986  bgoldbst  40987  evengpop3  41001  evengpoap3  41002  nnsum4primeseven  41003  nnsum4primesevenALTV  41004  2t6m3t4e0  41440  linevalexample  41498  zlmodzxzequa  41599  zlmodzxzequap  41602
  Copyright terms: Public domain W3C validator