Theorem 4cn 8117

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

Syntax hints:   ∈ wcel 1433  ℂcc 6979  4c4 8091

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-resscn 7068  ax-1re 7070  ax-addrcl 7073

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-in 2979  df-ss 2986  df-2 8098  df-3 8099  df-4 8100

This theorem is referenced by:  4p2e6  8175  4p3e7  8176  4p4e8  8177  4t2e8  8190  4d2e2  8192  8th4div3  8250  div4p1lem1div2  8284  5p5e10  8547  4t4e16  8575  6t5e30  8583  fzo0to42pr  9229  fldiv4p1lem1div2  9307  sqoddm1div8  9625  4bc3eq4  9700  4bc2eq6  9701  resqrexlemover  9896  resqrexlemcalc1  9900  resqrexlemcalc3  9902  flodddiv4  10334  6gcd4e2  10384  6lcm4e12  10469  ex-fac  10565  ex-bc  10566