Theorem 6cn 11305

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

Assertion

Ref	Expression
6cn	⊢ 6 ∈ ℂ

Proof of Theorem 6cn

Step	Hyp	Ref	Expression
1		6re 11304	. 2 ⊢ 6 ∈ ℝ
2	1	recni 10255	1 ⊢ 6 ∈ ℂ

Syntax hints:   ∈ wcel 2145  ℂcc 10137  6c6 11277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-i2m1 10207  ax-1ne0 10208  ax-rrecex 10211  ax-cnre 10212

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-iota 5995  df-fv 6040  df-ov 6797  df-2 11282  df-3 11283  df-4 11284  df-5 11285  df-6 11286

This theorem is referenced by:  7m1e6  11344  6p2e8  11372  6p3e9  11373  6p4e10OLD  11374  halfpm6th  11456  6p4e10  11800  6t2e12  11843  6t3e18  11844  6t5e30  11846  5recm6rec  11888  bpoly2  14995  bpoly3  14996  bpoly4  14997  efi4p  15074  ef01bndlem  15121  cos01bnd  15123  3lcm2e6woprm  15537  6lcm4e12  15538  2exp8  16004  2exp16  16005  19prm  16033  83prm  16038  163prm  16040  317prm  16041  631prm  16042  prmo6  16045  1259lem1  16046  1259lem2  16047  1259lem3  16048  1259lem4  16049  1259lem5  16050  2503lem1  16052  2503lem2  16053  2503lem3  16054  2503prm  16055  4001lem1  16056  4001lem2  16057  4001lem4  16059  4001prm  16060  sincos6thpi  24489  sincos3rdpi  24490  1cubrlem  24790  log2ublem3  24897  log2ub  24898  basellem5  25033  basellem8  25036  ppiub  25151  bclbnd  25227  bposlem8  25238  bposlem9  25239  2lgslem3d  25346  2lgsoddprmlem3d  25360  ex-exp  27650  ex-bc  27652  ex-gcd  27657  ex-lcm  27658  hgt750lemd  31067  hgt750lem2  31071  problem5  31902  lhe4.4ex1a  39055  wallispi2lem2  40807  fmtno5lem1  41994  fmtno5lem4  41997  fmtno5  41998  fmtno4prmfac  42013  fmtno5faclem2  42021  fmtno5faclem3  42022  fmtno5fac  42023  flsqrt5  42038  139prmALT  42040  127prm  42044  2exp11  42046  mod42tp1mod8  42048  2t6m3t4e0  42655  zlmodzxzequa  42814  zlmodzxzequap  42817