Theorem 3cn 11298

Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)

Assertion

Ref	Expression
3cn	⊢ 3 ∈ ℂ

Proof of Theorem 3cn

Step	Hyp	Ref	Expression
1		3re 11297	. 2 ⊢ 3 ∈ ℝ
2	1	recni 10255	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2145  ℂcc 10137  3c3 11274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-i2m1 10207  ax-1ne0 10208  ax-rrecex 10211  ax-cnre 10212

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-iota 5995  df-fv 6040  df-ov 6797  df-2 11282  df-3 11283

This theorem is referenced by:  3ex  11299  4m1e3  11341  3p2e5  11363  3p3e6  11364  4p4e8  11367  5p4e9  11370  6p4e10OLD  11374  3t1e3  11381  3t2e6  11382  3t3e9  11383  8th4div3  11455  halfpm6th  11456  6p4e10  11800  9t8e72  11871  halfthird  11887  fzo0to42pr  12764  sq3  13169  expnass  13178  fac3  13272  4bc3eq4  13320  sqrlem7  14198  caurcvgr  14613  bpoly2  14995  bpoly3  14996  bpoly4  14997  sin01bnd  15122  cos01bnd  15123  cos1bnd  15124  cos2bnd  15125  cos01gt0  15128  rpnnen2lem3  15152  rpnnen2lem11  15160  3dvdsdec  15264  3dvdsdecOLD  15265  3dvds2dec  15266  3lcm2e6woprm  15537  prmo3  15953  2exp6  16003  2exp16  16005  7prm  16025  13prm  16031  17prm  16032  19prm  16033  37prm  16036  43prm  16037  83prm  16038  139prm  16039  163prm  16040  317prm  16041  631prm  16042  prmo4  16043  1259lem1  16046  1259lem2  16047  1259lem3  16048  1259lem4  16049  1259lem5  16050  1259prm  16051  2503lem1  16052  2503lem2  16053  2503lem3  16054  2503prm  16055  4001lem1  16056  4001lem2  16057  4001lem3  16058  4001lem4  16059  4001prm  16060  iblitg  23756  tangtx  24479  sincos6thpi  24489  sincos3rdpi  24490  pige3  24491  ang180lem2  24762  1cubr  24791  dcubic1lem  24792  dcubic2  24793  dcubic1  24794  dcubic  24795  mcubic  24796  cubic2  24797  cubic  24798  binom4  24799  quart1cl  24803  quart1lem  24804  quart1  24805  quartlem1  24806  quartlem3  24808  log2cnv  24893  log2tlbnd  24894  log2ublem2  24896  log2ublem3  24897  log2ub  24898  basellem5  25033  basellem8  25036  basellem9  25037  cht3  25121  ppiub  25151  chtub  25159  bclbnd  25227  bposlem6  25236  bposlem8  25238  bposlem9  25239  lgsdir2lem1  25272  lgsdir2lem5  25276  2lgslem3b  25344  2lgslem3d  25346  2lgsoddprmlem3c  25359  2lgsoddprmlem3d  25360  pntibndlem1  25500  pntlemk  25517  ex-opab  27632  ex-exp  27650  ex-dvds  27656  ex-gcd  27657  ex-lcm  27658  ex-prmo  27659  ex-ind-dvds  27661  fib5  30808  fib6  30809  hgt750lem  31070  hgt750lem2  31071  hgt750leme  31077  problem4  31901  problem5  31902  sinccvglem  31905  pigt3  33736  mblfinlem3  33782  itg2addnclem2  33795  itg2addnclem3  33796  heiborlem6  33948  heiborlem7  33949  jm2.23  38090  inductionexd  38980  lhe4.4ex1a  39055  stoweidlem13  40748  stoweidlem26  40761  stoweidlem34  40769  wallispilem4  40803  wallispi2lem1  40806  fmtno5lem1  41994  fmtno5lem2  41995  257prm  42002  fmtno4prmfac  42013  fmtno4nprmfac193  42015  139prmALT  42040  127prm  42044  mod42tp1mod8  42048  3exp4mod41  42062  41prothprmlem2  42064  6even  42149  gbpart8  42185  sbgoldbwt  42194  sbgoldbst  42195  evengpop3  42215  evengpoap3  42216  nnsum4primeseven  42217  nnsum4primesevenALTV  42218  2t6m3t4e0  42655  linevalexample  42713  zlmodzxzequa  42814  zlmodzxzequap  42817