Theorem 3cn 11133

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 11132	. 2 ⊢ 3 ∈ ℝ
2	1	recni 10090	1 ⊢ 3 ∈ ℂ

Syntax hints:   ∈ wcel 2030  ℂcc 9972  3c3 11109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rrecex 10046  ax-cnre 10047

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-2 11117  df-3 11118

This theorem is referenced by:  3ex  11134  4m1e3  11176  3p2e5  11198  3p3e6  11199  4p4e8  11202  5p4e9  11205  6p4e10OLD  11209  3t1e3  11216  3t2e6  11217  3t3e9  11218  8th4div3  11290  halfpm6th  11291  6p4e10  11636  9t8e72  11707  halfthird  11723  fzo0to42pr  12595  sq3  13001  expnass  13010  fac3  13107  4bc3eq4  13155  sqrlem7  14033  caurcvgr  14448  bpoly2  14832  bpoly3  14833  bpoly4  14834  sin01bnd  14959  cos01bnd  14960  cos1bnd  14961  cos2bnd  14962  cos01gt0  14965  rpnnen2lem3  14989  rpnnen2lem11  14997  3dvdsdec  15101  3dvdsdecOLD  15102  3dvds2dec  15103  3dvds2decOLD  15104  3lcm2e6woprm  15375  prmo3  15792  2exp6  15842  2exp16  15844  7prm  15864  13prm  15870  17prm  15871  19prm  15872  37prm  15875  43prm  15876  83prm  15877  139prm  15878  163prm  15879  317prm  15880  631prm  15881  prmo4  15882  1259lem1  15885  1259lem2  15886  1259lem3  15887  1259lem4  15888  1259lem5  15889  1259prm  15890  2503lem1  15891  2503lem2  15892  2503lem3  15893  2503prm  15894  4001lem1  15895  4001lem2  15896  4001lem3  15897  4001lem4  15898  4001prm  15899  iblitg  23580  tangtx  24302  sincos6thpi  24312  sincos3rdpi  24313  pige3  24314  ang180lem2  24585  1cubr  24614  dcubic1lem  24615  dcubic2  24616  dcubic1  24617  dcubic  24618  mcubic  24619  cubic2  24620  cubic  24621  binom4  24622  quart1cl  24626  quart1lem  24627  quart1  24628  quartlem1  24629  quartlem3  24631  log2cnv  24716  log2tlbnd  24717  log2ublem2  24719  log2ublem3  24720  log2ub  24721  basellem5  24856  basellem8  24859  basellem9  24860  cht3  24944  ppiub  24974  chtub  24982  bclbnd  25050  bposlem6  25059  bposlem8  25061  bposlem9  25062  lgsdir2lem1  25095  lgsdir2lem5  25099  2lgslem3b  25167  2lgslem3d  25169  2lgsoddprmlem3c  25182  2lgsoddprmlem3d  25183  pntibndlem1  25323  pntlemk  25340  ex-opab  27419  ex-exp  27437  ex-dvds  27443  ex-gcd  27444  ex-lcm  27445  ex-prmo  27446  ex-ind-dvds  27448  fib5  30595  fib6  30596  hgt750lem  30857  hgt750lem2  30858  hgt750leme  30864  problem4  31688  problem5  31689  sinccvglem  31692  pigt3  33532  mblfinlem3  33578  itg2addnclem2  33592  itg2addnclem3  33593  heiborlem6  33745  heiborlem7  33746  jm2.23  37880  inductionexd  38770  lhe4.4ex1a  38845  stoweidlem13  40548  stoweidlem26  40561  stoweidlem34  40569  wallispilem4  40603  wallispi2lem1  40606  fmtno5lem1  41790  fmtno5lem2  41791  257prm  41798  fmtno4prmfac  41809  fmtno4nprmfac193  41811  139prmALT  41836  127prm  41840  mod42tp1mod8  41844  3exp4mod41  41858  41prothprmlem2  41860  6even  41945  gbpart8  41981  sbgoldbwt  41990  sbgoldbst  41991  evengpop3  42011  evengpoap3  42012  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  2t6m3t4e0  42451  linevalexample  42509  zlmodzxzequa  42610  zlmodzxzequap  42613