Theorem 4cn 8917

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

Syntax hints:   ∈ wcel 2128  ℂcc 7733  4c4 8892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-resscn 7827  ax-1re 7829  ax-addrcl 7832

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115  df-2 8898  df-3 8899  df-4 8900

This theorem is referenced by:  5m1e4  8961  4p2e6  8982  4p3e7  8983  4p4e8  8984  4t2e8  8997  4d2e2  8999  8th4div3  9058  div4p1lem1div2  9092  5p5e10  9371  4t4e16  9399  6t5e30  9407  fzo0to42pr  10129  fldiv4p1lem1div2  10214  sq4e2t8  10526  sqoddm1div8  10581  4bc3eq4  10659  4bc2eq6  10660  resqrexlemover  10922  resqrexlemcalc1  10926  resqrexlemcalc3  10928  cos2bnd  11669  flodddiv4  11838  6gcd4e2  11895  6lcm4e12  11980  pythagtriplem1  12156  dveflem  13183  sincosq4sgn  13246  cosq23lt0  13250  sincos6thpi  13259  ex-exp  13400  ex-fac  13401  ex-bc  13402