Theorem 3cn 9381

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

This proof depends on syntax axioms:   ∈ wcel 2209  ℂcc 8177  3c3 9358

This proof depends on 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 8271  ax-1re 8273  ax-addrcl 8276

This proof 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 9365  df-3 9366

This theorem is used by:  3ex  9382  3m1e2  9426  4m1e3  9427  3p2e5  9448  3p3e6  9449  4p4e8  9452  5p4e9  9455  3t1e3  9462  3t2e6  9463  2t3e6  9464  3t3e9  9465  8th4div3  9528  halfpm6th  9529  6p4e10  9857  9t8e72  9913  halfthird  9928  fzo0to42pr  10648  sq3  11086  expnass  11095  fac3  11184  4bc3eq4  11226  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  cos1bnd  12542  cos2bnd  12543  cos01gt0  12546  3dvdsdec  12648  3dvds2dec  12649  5ndvds3  12717  3lcm2e6woprm  12880  2exp6  13233  2exp16  13237  13prm  13250  17prm  13251  19prm  13252  37prm  13255  43prm  13256  83prm  13257  139prm  13258  163prm  13259  317prm  13260  631prm  13261  1259lem1  13262  1259lem2  13263  1259lem3  13264  1259lem4  13265  1259lem5  13266  1259prm  13267  cosq23lt0  15984  tangtx  15989  sincos6thpi  15993  sincos3rdpi  15994  pigt3  15995  binom4  16138  log2tlbndlog2  16139  log2ublem2  16141  log2ublem3  16142  log2ublog2  16143  ppiqub  16194  bclbnd  16205  lgsdir2lem1  16245  lgsdir2lem5  16249  2lgslem3b  16311  2lgslem3d  16313  2lgsoddprmlem3c  16326  2lgsoddprmlem3d  16327  ex-exp  16839  ex-dvds  16842  ex-gcd  16843