Theorem 4cn 9114

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

Syntax hints:   ∈ wcel 2176  ℂcc 7923  4c4 9089

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-resscn 8017  ax-1re 8019  ax-addrcl 8022

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179  df-2 9095  df-3 9096  df-4 9097

This theorem is referenced by:  5m1e4  9158  4p2e6  9180  4p3e7  9181  4p4e8  9182  4t2e8  9195  4d2e2  9197  8th4div3  9256  div4p1lem1div2  9291  5p5e10  9574  4t4e16  9602  6t5e30  9610  fzo0to42pr  10349  fldiv4p1lem1div2  10448  sq4e2t8  10782  sqoddm1div8  10838  4bc3eq4  10918  4bc2eq6  10919  resqrexlemover  11321  resqrexlemcalc1  11325  resqrexlemcalc3  11327  cos2bnd  12071  flodddiv4  12247  6gcd4e2  12316  6lcm4e12  12409  pythagtriplem1  12588  2exp11  12759  dveflem  15198  sincosq4sgn  15301  cosq23lt0  15305  sincos6thpi  15314  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2lgsoddprmlem2  15583  2lgsoddprmlem3c  15586  2lgsoddprmlem3d  15587  ex-exp  15663  ex-fac  15664  ex-bc  15665