MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  5cn Structured version   Unicode version

Theorem 5cn 10502
Description: The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
5cn  |-  5  e.  CC

Proof of Theorem 5cn
StepHypRef Expression
1 5re 10501 . 2  |-  5  e.  RR
21recni 9499 1  |-  5  e.  CC
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758   CCcc 9381   5c5 10475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-i2m1 9451  ax-1ne0 9452  ax-rrecex 9455  ax-cnre 9456
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-iota 5479  df-fv 5524  df-ov 6193  df-2 10481  df-3 10482  df-4 10483  df-5 10484
This theorem is referenced by:  5p2e7  10560  5p3e8  10561  5p4e9  10562  5p5e10  10563  5t2e10  10577  ef01bndlem  13570  dec5dvds  14195  dec5nprm  14197  2exp16  14219  prmlem1  14237  17prm  14246  139prm  14253  163prm  14254  317prm  14255  631prm  14256  1259lem1  14257  1259lem2  14258  1259lem3  14259  1259lem4  14260  2503lem1  14263  2503lem2  14264  2503lem3  14265  4001lem1  14267  4001lem2  14268  4001lem3  14269  4001lem4  14270  4001prm  14271  log2ublem3  22459  log2ub  22460  ppiublem2  22658  ppiub  22659  bclbnd  22735  bposlem4  22742  bposlem5  22743  bposlem6  22744  bposlem8  22746  bposlem9  22747  lgsdir2lem1  22778  5recm6rec  27527  bpoly4  28336  linevalexample  31002  5m4e1  31449
  Copyright terms: Public domain W3C validator