Theorem 4cn 9211

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

Syntax hints:   ∈ wcel 2200  ℂcc 8020  4c4 9186

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 8114  ax-1re 8116  ax-addrcl 8119

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 3204  df-ss 3211  df-2 9192  df-3 9193  df-4 9194

This theorem is referenced by:  5m1e4  9255  4p2e6  9277  4p3e7  9278  4p4e8  9279  4t2e8  9292  4d2e2  9294  8th4div3  9353  div4p1lem1div2  9388  5p5e10  9671  4t4e16  9699  6t5e30  9707  fzo0to42pr  10455  fldiv4p1lem1div2  10555  sq4e2t8  10889  sqoddm1div8  10945  4bc3eq4  11025  4bc2eq6  11026  resqrexlemover  11561  resqrexlemcalc1  11565  resqrexlemcalc3  11567  cos2bnd  12311  flodddiv4  12487  6gcd4e2  12556  6lcm4e12  12649  pythagtriplem1  12828  2exp11  12999  dveflem  15440  sincosq4sgn  15543  cosq23lt0  15547  sincos6thpi  15556  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2lgsoddprmlem2  15825  2lgsoddprmlem3c  15828  2lgsoddprmlem3d  15829  ex-exp  16259  ex-fac  16260  ex-bc  16261