Theorem 3cn 10599

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

Syntax hints:   e. wcel 1762   CCcc 9479   3c3 10575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  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 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-ov 6278  df-2 10583  df-3 10584

This theorem is referenced by:  3ex  10600  3m1e2  10641  3p2e5  10657  3p3e6  10658  4p4e8  10661  5p4e9  10664  6p4e10  10668  3t1e3  10675  3t2e6  10676  3t3e9  10677  8th4div3  10748  halfpm6th  10749  9t8e72  11066  fzo0to42pr  11858  sq3  12220  expnass  12228  fac3  12315  sqrlem7  13032  caurcvgr  13445  sin01bnd  13770  cos01bnd  13771  cos1bnd  13772  cos2bnd  13773  cos01gt0  13776  rpnnen2lem3  13800  rpnnen2lem11  13808  2exp16  14422  7prm  14443  13prm  14448  17prm  14449  19prm  14450  37prm  14453  43prm  14454  83prm  14455  139prm  14456  163prm  14457  317prm  14458  631prm  14459  1259lem1  14460  1259lem2  14461  1259lem3  14462  1259lem4  14463  1259lem5  14464  1259prm  14465  2503lem1  14466  2503lem2  14467  2503lem3  14468  2503prm  14469  4001lem1  14470  4001lem2  14471  4001lem3  14472  4001lem4  14473  4001prm  14474  iblitg  21903  tangtx  22624  sincos6thpi  22634  sincos3rdpi  22635  pige3  22636  ang180lem2  22863  1cubr  22894  dcubic1lem  22895  dcubic2  22896  dcubic1  22897  dcubic  22898  mcubic  22899  cubic2  22900  cubic  22901  binom4  22902  quart1cl  22906  quart1lem  22907  quart1  22908  quartlem1  22909  quartlem3  22911  log2cnv  22996  log2tlbnd  22997  log2ublem2  22999  log2ublem3  23000  log2ub  23001  basellem5  23079  basellem8  23082  basellem9  23083  cht3  23168  ppiub  23200  chtub  23208  bclbnd  23276  bposlem6  23285  bposlem8  23287  bposlem9  23288  lgsdir2lem1  23319  lgsdir2lem5  23323  pntibndlem1  23495  pntlemk  23512  extwwlkfablem2  24741  ex-opab  24816  ex-dvds  24832  fib5  27970  fib6  27971  problem4  28483  problem5  28484  sinccvglem  28499  4bc3eq4  28572  halfthird  28574  bpoly2  29382  bpoly3  29383  bpoly4  29384  mblfinlem3  29617  itg2addnclem2  29631  itg2addnclem3  29632  heiborlem6  29902  heiborlem7  29903  jm2.23  30531  lhe4.4ex1a  30789  stoweidlem13  31268  stoweidlem26  31281  stoweidlem34  31289  wallispilem4  31323  wallispi2lem1  31326  2t6m3t4e0  31876  linevalexample  31944  zlmodzxzequa  32053  zlmodzxzequap  32056