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

Theorem 9cn 11292
Description: The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
9cn 9 ∈ ℂ

Proof of Theorem 9cn
StepHypRef Expression
1 9re 11291 . 2 9 ∈ ℝ
21recni 10236 1 9 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2131  cc 10118  9c9 11261
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-i2m1 10188  ax-1ne0 10189  ax-rrecex 10192  ax-cnre 10193
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-iota 6004  df-fv 6049  df-ov 6808  df-2 11263  df-3 11264  df-4 11265  df-5 11266  df-6 11267  df-7 11268  df-8 11269  df-9 11270
This theorem is referenced by:  10m1e9  11814  9t2e18  11847  9t8e72  11853  9t9e81  11854  9t11e99  11855  9t11e99OLD  11856  0.999...  14803  0.999...OLD  14804  cos2bnd  15109  3dvds  15246  3dvdsOLD  15247  3dvdsdec  15248  3dvdsdecOLD  15249  3dvds2dec  15250  3dvds2decOLD  15251  2exp8  15990  139prm  16025  163prm  16026  317prm  16027  631prm  16028  1259lem1  16032  1259lem2  16033  1259lem3  16034  1259lem4  16035  1259lem5  16036  2503lem1  16038  2503lem2  16039  2503lem3  16040  2503prm  16041  4001lem1  16042  4001lem2  16043  4001lem3  16044  4001lem4  16045  mcubic  24765  cubic2  24766  cubic  24767  quartlem1  24775  log2tlbnd  24863  log2ublem3  24866  log2ub  24867  bposlem8  25207  ex-lcm  27618  1mhdrd  29925  hgt750lem2  31031  fmtno5lem4  41970  257prm  41975  fmtno4nprmfac193  41988  139prmALT  42013  127prm  42017  evengpop3  42188
  Copyright terms: Public domain W3C validator