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

Theorem 4cn 8254
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 8253 . 2 4 ∈ ℝ
21recni 7263 1 4 ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 1434  cc 7111  4c4 8228
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-resscn 7200  ax-1re 7202  ax-addrcl 7205
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-in 2988  df-ss 2995  df-2 8235  df-3 8236  df-4 8237
This theorem is referenced by:  4p2e6  8312  4p3e7  8313  4p4e8  8314  4t2e8  8327  4d2e2  8329  8th4div3  8387  div4p1lem1div2  8421  5p5e10  8698  4t4e16  8726  6t5e30  8734  fzo0to42pr  9376  fldiv4p1lem1div2  9457  sqoddm1div8  9792  4bc3eq4  9867  4bc2eq6  9868  resqrexlemover  10115  resqrexlemcalc1  10119  resqrexlemcalc3  10121  flodddiv4  10559  6gcd4e2  10609  6lcm4e12  10694  ex-fac  10843  ex-bc  10844
  Copyright terms: Public domain W3C validator