Theorem 3cn 10630

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

Syntax hints:   e. wcel 1872   CCcc 9483   3c3 10606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-i2m1 9553  ax-1ne0 9554  ax-rrecex 9557  ax-cnre 9558

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-iota 5503  df-fv 5547  df-ov 6247  df-2 10614  df-3 10615

This theorem is referenced by:  3ex  10631  3m1e2  10672  3p2e5  10688  3p3e6  10689  4p4e8  10692  5p4e9  10695  6p4e10  10699  3t1e3  10706  3t2e6  10707  3t3e9  10708  8th4div3  10779  halfpm6th  10780  9t8e72  11098  halfthird  11103  fzo0to42pr  11945  sq3  12317  expnass  12325  fac3  12411  4bc3eq4  12458  sqrlem7  13251  caurcvgr  13676  caurcvgrOLD  13677  bpoly2  14048  bpoly3  14049  bpoly4  14050  sin01bnd  14177  cos01bnd  14178  cos1bnd  14179  cos2bnd  14180  cos01gt0  14183  rpnnen2lem3  14207  rpnnen2lem11  14215  3lcm2e6woprm  14518  prmo3  14937  2exp6  14996  2exp16  14999  7prm  15020  13prm  15025  17prm  15026  19prm  15027  37prm  15030  43prm  15031  83prm  15032  139prm  15033  163prm  15034  317prm  15035  631prm  15036  prmo4  15037  1259lem1  15040  1259lem2  15041  1259lem3  15042  1259lem4  15043  1259lem5  15044  1259prm  15045  2503lem1  15046  2503lem2  15047  2503lem3  15048  2503prm  15049  4001lem1  15050  4001lem2  15051  4001lem3  15052  4001lem4  15053  4001prm  15054  iblitg  22663  tangtx  23397  sincos6thpi  23407  sincos3rdpi  23408  pige3  23409  ang180lem2  23676  1cubr  23705  dcubic1lem  23706  dcubic2  23707  dcubic1  23708  dcubic  23709  mcubic  23710  cubic2  23711  cubic  23712  binom4  23713  quart1cl  23717  quart1lem  23718  quart1  23719  quartlem1  23720  quartlem3  23722  log2cnv  23807  log2tlbnd  23808  log2ublem2  23810  log2ublem3  23811  log2ub  23812  basellem5  23948  basellem8  23951  basellem9  23952  cht3  24037  ppiub  24069  chtub  24077  bclbnd  24145  bposlem6  24154  bposlem8  24156  bposlem9  24157  lgsdir2lem1  24188  lgsdir2lem5  24192  pntibndlem1  24364  pntlemk  24381  extwwlkfablem2  25743  ex-opab  25819  ex-dvds  25835  ex-ind-dvds  25836  fib5  29185  fib6  29186  problem4  30247  problem5  30248  sinccvglem  30263  pigt3  31845  mblfinlem3  31886  itg2addnclem2  31901  itg2addnclem3  31902  heiborlem6  32055  heiborlem7  32056  jm2.23  35764  inductionexd  36506  lhe4.4ex1a  36591  stoweidlem13  37756  stoweidlem26  37769  stoweidlem34  37778  wallispilem4  37813  wallispi2lem1  37816  6even  38651  gbpart8  38682  bgoldbwt  38691  bgoldbst  38692  evengpop3  38706  evengpoap3  38707  nnsum4primeseven  38708  nnsum4primesevenALTV  38709  3exp4mod41  38729  41prothprmlem2  38731  2t6m3t4e0  39722  linevalexample  39781  zlmodzxzequa  39882  zlmodzxzequap  39885