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

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

Proof of Theorem 9cn
StepHypRef Expression
1 9re 10406 . 2  |-  9  e.  RR
21recni 9396 1  |-  9  e.  CC
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   CCcc 9278   9c9 10376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-resscn 9337  ax-1cn 9338  ax-icn 9339  ax-addcl 9340  ax-addrcl 9341  ax-mulcl 9342  ax-mulrcl 9343  ax-i2m1 9348  ax-1ne0 9349  ax-rrecex 9352  ax-cnre 9353
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-nul 3636  df-if 3790  df-sn 3876  df-pr 3878  df-op 3882  df-uni 4090  df-br 4291  df-iota 5379  df-fv 5424  df-ov 6092  df-2 10378  df-3 10379  df-4 10380  df-5 10381  df-6 10382  df-7 10383  df-8 10384  df-9 10385
This theorem is referenced by:  9t2e18  10848  9t8e72  10854  9t9e81  10855  0.999...  13339  cos2bnd  13470  3dvds  13594  2exp8  14114  139prm  14149  163prm  14150  317prm  14151  631prm  14152  1259lem1  14153  1259lem2  14154  1259lem3  14155  1259lem4  14156  1259lem5  14157  2503lem1  14159  2503lem2  14160  2503lem3  14161  2503prm  14162  4001lem1  14163  4001lem2  14164  4001lem3  14165  4001lem4  14166  mcubic  22240  cubic2  22241  cubic  22242  quartlem1  22250  log2tlbnd  22338  log2ublem3  22341  log2ub  22342  bposlem8  22628
  Copyright terms: Public domain W3C validator