Theorem 4cn 8991

Description: The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
4cn	⊢ 4 ∈ ℂ

Proof of Theorem 4cn

Step	Hyp	Ref	Expression
1		4re 8990	. 2 ⊢ 4 ∈ ℝ
2	1	recni 7964	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2148  ℂcc 7804  4c4 8966

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 7898  ax-1re 7900  ax-addrcl 7903

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 3135  df-ss 3142  df-2 8972  df-3 8973  df-4 8974

This theorem is referenced by:  5m1e4  9035  4p2e6  9056  4p3e7  9057  4p4e8  9058  4t2e8  9071  4d2e2  9073  8th4div3  9132  div4p1lem1div2  9166  5p5e10  9448  4t4e16  9476  6t5e30  9484  fzo0to42pr  10213  fldiv4p1lem1div2  10298  sq4e2t8  10610  sqoddm1div8  10666  4bc3eq4  10744  4bc2eq6  10745  resqrexlemover  11010  resqrexlemcalc1  11014  resqrexlemcalc3  11016  cos2bnd  11759  flodddiv4  11929  6gcd4e2  11986  6lcm4e12  12077  pythagtriplem1  12255  dveflem  13969  sincosq4sgn  14032  cosq23lt0  14036  sincos6thpi  14045  ex-exp  14250  ex-fac  14251  ex-bc  14252