Theorem 3cn 8994

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

Syntax hints:   ∈ wcel 2148  ℂcc 7809  3c3 8971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7903  ax-1re 7905  ax-addrcl 7908

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143  df-2 8978  df-3 8979

This theorem is referenced by:  3ex  8995  3m1e2  9039  4m1e3  9040  3p2e5  9060  3p3e6  9061  4p4e8  9064  5p4e9  9067  3t1e3  9074  3t2e6  9075  3t3e9  9076  8th4div3  9138  halfpm6th  9139  6p4e10  9455  9t8e72  9511  halfthird  9526  fzo0to42pr  10220  sq3  10617  expnass  10626  fac3  10712  4bc3eq4  10753  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  cos1bnd  11767  cos2bnd  11768  cos01gt0  11770  3dvdsdec  11870  3dvds2dec  11871  3lcm2e6woprm  12086  cosq23lt0  14257  tangtx  14262  sincos6thpi  14266  sincos3rdpi  14267  pigt3  14268  binom4  14400  lgsdir2lem1  14432  lgsdir2lem5  14436  2lgsoddprmlem3c  14460  2lgsoddprmlem3d  14461  ex-exp  14482  ex-dvds  14485  ex-gcd  14486