Theorem 3cn 10606

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 10605	. 2 |- 3 e. RR
2	1	recni 9597	1 |- 3 e. CC

Syntax hints:   e. wcel 1823   CCcc 9479   3c3 10582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-i2m1 9549  ax-1ne0 9550  ax-rrecex 9553  ax-cnre 9554

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-2 10590  df-3 10591

This theorem is referenced by:  3ex  10607  3m1e2  10648  3p2e5  10664  3p3e6  10665  4p4e8  10668  5p4e9  10671  6p4e10  10675  3t1e3  10682  3t2e6  10683  3t3e9  10684  8th4div3  10755  halfpm6th  10756  9t8e72  11077  fzo0to42pr  11882  sq3  12247  expnass  12255  fac3  12342  sqrlem7  13164  caurcvgr  13578  sin01bnd  14002  cos01bnd  14003  cos1bnd  14004  cos2bnd  14005  cos01gt0  14008  rpnnen2lem3  14034  rpnnen2lem11  14042  2exp6  14656  2exp16  14659  7prm  14680  13prm  14685  17prm  14686  19prm  14687  37prm  14690  43prm  14691  83prm  14692  139prm  14693  163prm  14694  317prm  14695  631prm  14696  1259lem1  14697  1259lem2  14698  1259lem3  14699  1259lem4  14700  1259lem5  14701  1259prm  14702  2503lem1  14703  2503lem2  14704  2503lem3  14705  2503prm  14706  4001lem1  14707  4001lem2  14708  4001lem3  14709  4001lem4  14710  4001prm  14711  iblitg  22341  tangtx  23064  sincos6thpi  23074  sincos3rdpi  23075  pige3  23076  ang180lem2  23341  1cubr  23370  dcubic1lem  23371  dcubic2  23372  dcubic1  23373  dcubic  23374  mcubic  23375  cubic2  23376  cubic  23377  binom4  23378  quart1cl  23382  quart1lem  23383  quart1  23384  quartlem1  23385  quartlem3  23387  log2cnv  23472  log2tlbnd  23473  log2ublem2  23475  log2ublem3  23476  log2ub  23477  basellem5  23556  basellem8  23559  basellem9  23560  cht3  23645  ppiub  23677  chtub  23685  bclbnd  23753  bposlem6  23762  bposlem8  23764  bposlem9  23765  lgsdir2lem1  23796  lgsdir2lem5  23800  pntibndlem1  23972  pntlemk  23989  extwwlkfablem2  25280  ex-opab  25355  ex-dvds  25371  ex-ind-dvds  25372  fib5  28608  fib6  28609  problem4  29286  problem5  29287  sinccvglem  29302  4bc3eq4  29352  halfthird  29354  bpoly2  30047  bpoly3  30048  bpoly4  30049  mblfinlem3  30293  itg2addnclem2  30307  itg2addnclem3  30308  heiborlem6  30552  heiborlem7  30553  jm2.23  31177  lhe4.4ex1a  31475  stoweidlem13  32034  stoweidlem26  32047  stoweidlem34  32055  wallispilem4  32089  wallispi2lem1  32092  2t6m3t4e0  33191  linevalexample  33250  zlmodzxzequa  33351  zlmodzxzequap  33354  inductionexd  38419