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

Theorem 4cn 8038
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 8037 . 2 4 ∈ ℝ
21recni 7067 1 4 ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 1407  cc 6915  4c4 8012
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-11 1411  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036  ax-resscn 7004  ax-1re 7006  ax-addrcl 7009
This theorem depends on definitions:  df-bi 114  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-in 2949  df-ss 2956  df-2 8019  df-3 8020  df-4 8021
This theorem is referenced by:  4p2e6  8096  4p3e7  8097  4p4e8  8098  4t2e8  8111  4d2e2  8113  8th4div3  8171  div4p1lem1div2  8205  5p5e10  8467  4t4e16  8495  6t5e30  8503  fzo0to42pr  9148  fldiv4p1lem1div2  9220  sqoddm1div8  9533  4bc3eq4  9605  4bc2eq6  9606  resqrexlemover  9800  resqrexlemcalc1  9804  resqrexlemcalc3  9806  ex-fac  10224  ex-bc  10225
  Copyright terms: Public domain W3C validator