Theorem 3cn 9358

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

Syntax hints:   ∈ wcel 2209  ℂcc 8167  3c3 9335

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8261  ax-1re 8263  ax-addrcl 8266

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-2 9342  df-3 9343

This theorem is referenced by:  3ex  9359  3m1e2  9403  4m1e3  9404  3p2e5  9425  3p3e6  9426  4p4e8  9429  5p4e9  9432  3t1e3  9439  3t2e6  9440  3t3e9  9441  8th4div3  9503  halfpm6th  9504  6p4e10  9827  9t8e72  9883  halfthird  9898  fzo0to42pr  10616  sq3  11051  expnass  11060  fac3  11148  4bc3eq4  11190  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  cos1bnd  12504  cos2bnd  12505  cos01gt0  12508  3dvdsdec  12610  3dvds2dec  12611  5ndvds3  12679  3lcm2e6woprm  12842  2exp6  13190  2exp16  13194  cosq23lt0  15857  tangtx  15862  sincos6thpi  15866  sincos3rdpi  15867  pigt3  15868  binom4  16004  lgsdir2lem1  16061  lgsdir2lem5  16065  2lgslem3b  16127  2lgslem3d  16129  2lgsoddprmlem3c  16142  2lgsoddprmlem3d  16143  ex-exp  16655  ex-dvds  16658  ex-gcd  16659