ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  4cn GIF version

Theorem 4cn 8821
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
StepHypRef Expression
1 4re 8820 . 2 4 ∈ ℝ
21recni 7801 1 4 ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 1481  cc 7641  4c4 8796
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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-resscn 7735  ax-1re 7737  ax-addrcl 7740
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3081  df-ss 3088  df-2 8802  df-3 8803  df-4 8804
This theorem is referenced by:  5m1e4  8865  4p2e6  8886  4p3e7  8887  4p4e8  8888  4t2e8  8901  4d2e2  8903  8th4div3  8962  div4p1lem1div2  8996  5p5e10  9275  4t4e16  9303  6t5e30  9311  fzo0to42pr  10027  fldiv4p1lem1div2  10108  sq4e2t8  10420  sqoddm1div8  10474  4bc3eq4  10550  4bc2eq6  10551  resqrexlemover  10813  resqrexlemcalc1  10817  resqrexlemcalc3  10819  cos2bnd  11501  flodddiv4  11665  6gcd4e2  11717  6lcm4e12  11802  dveflem  12893  sincosq4sgn  12956  cosq23lt0  12960  sincos6thpi  12969  ex-exp  13108  ex-fac  13109  ex-bc  13110
  Copyright terms: Public domain W3C validator