Theorem 3cn 10711

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

Step	Hyp	Ref	Expression
1		3re 10710	. 2 |- 3 e. RR
2	1	recni 9680	1 |- 3 e. CC

Syntax hints:   e. wcel 1897   CCcc 9562   3c3 10687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-i2m1 9632  ax-1ne0 9633  ax-rrecex 9636  ax-cnre 9637

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-iota 5564  df-fv 5608  df-ov 6317  df-2 10695  df-3 10696

This theorem is referenced by:  3ex  10712  3m1e2  10753  4m1e3  10754  3p2e5  10770  3p3e6  10771  4p4e8  10774  5p4e9  10777  6p4e10  10781  3t1e3  10788  3t2e6  10789  3t3e9  10790  8th4div3  10861  halfpm6th  10862  9t8e72  11180  halfthird  11185  fzo0to42pr  12030  sq3  12403  expnass  12411  fac3  12497  4bc3eq4  12544  sqrlem7  13360  caurcvgr  13786  caurcvgrOLD  13787  bpoly2  14158  bpoly3  14159  bpoly4  14160  sin01bnd  14287  cos01bnd  14288  cos1bnd  14289  cos2bnd  14290  cos01gt0  14293  rpnnen2lem3  14317  rpnnen2lem11  14325  3lcm2e6woprm  14628  prmo3  15047  2exp6  15106  2exp16  15109  7prm  15130  13prm  15135  17prm  15136  19prm  15137  37prm  15140  43prm  15141  83prm  15142  139prm  15143  163prm  15144  317prm  15145  631prm  15146  prmo4  15147  1259lem1  15150  1259lem2  15151  1259lem3  15152  1259lem4  15153  1259lem5  15154  1259prm  15155  2503lem1  15156  2503lem2  15157  2503lem3  15158  2503prm  15159  4001lem1  15160  4001lem2  15161  4001lem3  15162  4001lem4  15163  4001prm  15164  iblitg  22774  tangtx  23508  sincos6thpi  23518  sincos3rdpi  23519  pige3  23520  ang180lem2  23787  1cubr  23816  dcubic1lem  23817  dcubic2  23818  dcubic1  23819  dcubic  23820  mcubic  23821  cubic2  23822  cubic  23823  binom4  23824  quart1cl  23828  quart1lem  23829  quart1  23830  quartlem1  23831  quartlem3  23833  log2cnv  23918  log2tlbnd  23919  log2ublem2  23921  log2ublem3  23922  log2ub  23923  basellem5  24059  basellem8  24062  basellem9  24063  cht3  24148  ppiub  24180  chtub  24188  bclbnd  24256  bposlem6  24265  bposlem8  24267  bposlem9  24268  lgsdir2lem1  24299  lgsdir2lem5  24303  pntibndlem1  24475  pntlemk  24492  extwwlkfablem2  25854  ex-opab  25930  ex-dvds  25946  ex-ind-dvds  25947  fib5  29286  fib6  29287  problem4  30348  problem5  30349  sinccvglem  30364  pigt3  31982  mblfinlem3  32023  itg2addnclem2  32038  itg2addnclem3  32039  heiborlem6  32192  heiborlem7  32193  jm2.23  35895  inductionexd  36637  lhe4.4ex1a  36721  stoweidlem13  37910  stoweidlem26  37923  stoweidlem34  37932  wallispilem4  37967  wallispi2lem1  37970  6even  38875  gbpart8  38906  bgoldbwt  38915  bgoldbst  38916  evengpop3  38930  evengpoap3  38931  nnsum4primeseven  38932  nnsum4primesevenALTV  38933  3exp4mod41  38953  41prothprmlem2  38955  2t6m3t4e0  40401  linevalexample  40460  zlmodzxzequa  40561  zlmodzxzequap  40564