Theorem 4cn 8656

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

Syntax hints:   ∈ wcel 1448  ℂcc 7498  4c4 8631

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-resscn 7587  ax-1re 7589  ax-addrcl 7592

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-in 3027  df-ss 3034  df-2 8637  df-3 8638  df-4 8639

This theorem is referenced by:  4p2e6  8715  4p3e7  8716  4p4e8  8717  4t2e8  8730  4d2e2  8732  8th4div3  8791  div4p1lem1div2  8825  5p5e10  9104  4t4e16  9132  6t5e30  9140  fzo0to42pr  9838  fldiv4p1lem1div2  9919  sq4e2t8  10231  sqoddm1div8  10285  4bc3eq4  10360  4bc2eq6  10361  resqrexlemover  10622  resqrexlemcalc1  10626  resqrexlemcalc3  10628  cos2bnd  11265  flodddiv4  11426  6gcd4e2  11476  6lcm4e12  11561  ex-exp  12542  ex-fac  12543  ex-bc  12544