Theorem 9cn 11309

Description: The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
9cn	⊢ 9 ∈ ℂ

Proof of Theorem 9cn

Step	Hyp	Ref	Expression
1		9re 11308	. 2 ⊢ 9 ∈ ℝ
2	1	recni 10253	1 ⊢ 9 ∈ ℂ

Syntax hints:   ∈ wcel 2144  ℂcc 10135  9c9 11278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-resscn 10194  ax-1cn 10195  ax-icn 10196  ax-addcl 10197  ax-addrcl 10198  ax-mulcl 10199  ax-mulrcl 10200  ax-i2m1 10205  ax-1ne0 10206  ax-rrecex 10209  ax-cnre 10210

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-iota 5994  df-fv 6039  df-ov 6795  df-2 11280  df-3 11281  df-4 11282  df-5 11283  df-6 11284  df-7 11285  df-8 11286  df-9 11287

This theorem is referenced by:  10m1e9  11830  9t2e18  11863  9t8e72  11869  9t9e81  11870  9t11e99  11871  9t11e99OLD  11872  0.999...  14818  0.999...OLD  14819  cos2bnd  15123  3dvds  15260  3dvdsOLD  15261  3dvdsdec  15262  3dvdsdecOLD  15263  3dvds2dec  15264  2exp8  16002  139prm  16037  163prm  16038  317prm  16039  631prm  16040  1259lem1  16044  1259lem2  16045  1259lem3  16046  1259lem4  16047  1259lem5  16048  2503lem1  16050  2503lem2  16051  2503lem3  16052  2503prm  16053  4001lem1  16054  4001lem2  16055  4001lem3  16056  4001lem4  16057  mcubic  24794  cubic2  24795  cubic  24796  quartlem1  24804  log2tlbnd  24892  log2ublem3  24895  log2ub  24896  bposlem8  25236  ex-lcm  27651  1mhdrd  29958  hgt750lem2  31064  fmtno5lem4  41986  257prm  41991  fmtno4nprmfac193  42004  139prmALT  42029  127prm  42033  evengpop3  42204