Theorem 4cn 9199

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 9198	. 2 ⊢ 4 ∈ ℝ
2	1	recni 8169	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2200  ℂcc 8008  4c4 9174

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8102  ax-1re 8104  ax-addrcl 8107

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-2 9180  df-3 9181  df-4 9182

This theorem is referenced by:  5m1e4  9243  4p2e6  9265  4p3e7  9266  4p4e8  9267  4t2e8  9280  4d2e2  9282  8th4div3  9341  div4p1lem1div2  9376  5p5e10  9659  4t4e16  9687  6t5e30  9695  fzo0to42pr  10438  fldiv4p1lem1div2  10537  sq4e2t8  10871  sqoddm1div8  10927  4bc3eq4  11007  4bc2eq6  11008  resqrexlemover  11536  resqrexlemcalc1  11540  resqrexlemcalc3  11542  cos2bnd  12286  flodddiv4  12462  6gcd4e2  12531  6lcm4e12  12624  pythagtriplem1  12803  2exp11  12974  dveflem  15415  sincosq4sgn  15518  cosq23lt0  15522  sincos6thpi  15531  2lgslem3a  15787  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  2lgsoddprmlem2  15800  2lgsoddprmlem3c  15803  2lgsoddprmlem3d  15804  ex-exp  16146  ex-fac  16147  ex-bc  16148