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

Theorem 4cn 8766
Description: The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
4cn  |-  4  e.  CC

Proof of Theorem 4cn
StepHypRef Expression
1 4re 8765 . 2  |-  4  e.  RR
21recni 7746 1  |-  4  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1465   CCcc 7586   4c4 8741
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 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-resscn 7680  ax-1re 7682  ax-addrcl 7685
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-in 3047  df-ss 3054  df-2 8747  df-3 8748  df-4 8749
This theorem is referenced by:  5m1e4  8810  4p2e6  8831  4p3e7  8832  4p4e8  8833  4t2e8  8846  4d2e2  8848  8th4div3  8907  div4p1lem1div2  8941  5p5e10  9220  4t4e16  9248  6t5e30  9256  fzo0to42pr  9965  fldiv4p1lem1div2  10046  sq4e2t8  10358  sqoddm1div8  10412  4bc3eq4  10487  4bc2eq6  10488  resqrexlemover  10750  resqrexlemcalc1  10754  resqrexlemcalc3  10756  cos2bnd  11394  flodddiv4  11558  6gcd4e2  11610  6lcm4e12  11695  dveflem  12782  sincosq4sgn  12837  cosq23lt0  12841  sincos6thpi  12850  ex-exp  12866  ex-fac  12867  ex-bc  12868
  Copyright terms: Public domain W3C validator