Theorem 4cn 9113

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

Syntax hints:   ∈ wcel 2175  ℂcc 7922  4c4 9088

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-resscn 8016  ax-1re 8018  ax-addrcl 8021

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178  df-2 9094  df-3 9095  df-4 9096

This theorem is referenced by:  5m1e4  9157  4p2e6  9179  4p3e7  9180  4p4e8  9181  4t2e8  9194  4d2e2  9196  8th4div3  9255  div4p1lem1div2  9290  5p5e10  9573  4t4e16  9601  6t5e30  9609  fzo0to42pr  10347  fldiv4p1lem1div2  10446  sq4e2t8  10780  sqoddm1div8  10836  4bc3eq4  10916  4bc2eq6  10917  resqrexlemover  11292  resqrexlemcalc1  11296  resqrexlemcalc3  11298  cos2bnd  12042  flodddiv4  12218  6gcd4e2  12287  6lcm4e12  12380  pythagtriplem1  12559  2exp11  12730  dveflem  15169  sincosq4sgn  15272  cosq23lt0  15276  sincos6thpi  15285  2lgslem3a  15541  2lgslem3b  15542  2lgslem3c  15543  2lgslem3d  15544  2lgsoddprmlem2  15554  2lgsoddprmlem3c  15557  2lgsoddprmlem3d  15558  ex-exp  15625  ex-fac  15626  ex-bc  15627