Theorem 4cn 9149

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

Syntax hints:   ∈ wcel 2178  ℂcc 7958  4c4 9124

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-resscn 8052  ax-1re 8054  ax-addrcl 8057

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187  df-2 9130  df-3 9131  df-4 9132

This theorem is referenced by:  5m1e4  9193  4p2e6  9215  4p3e7  9216  4p4e8  9217  4t2e8  9230  4d2e2  9232  8th4div3  9291  div4p1lem1div2  9326  5p5e10  9609  4t4e16  9637  6t5e30  9645  fzo0to42pr  10386  fldiv4p1lem1div2  10485  sq4e2t8  10819  sqoddm1div8  10875  4bc3eq4  10955  4bc2eq6  10956  resqrexlemover  11436  resqrexlemcalc1  11440  resqrexlemcalc3  11442  cos2bnd  12186  flodddiv4  12362  6gcd4e2  12431  6lcm4e12  12524  pythagtriplem1  12703  2exp11  12874  dveflem  15313  sincosq4sgn  15416  cosq23lt0  15420  sincos6thpi  15429  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2lgsoddprmlem2  15698  2lgsoddprmlem3c  15701  2lgsoddprmlem3d  15702  ex-exp  15863  ex-fac  15864  ex-bc  15865