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

Theorem 7cn 12246
Description: The number 7 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
Assertion
Ref Expression
7cn 7 ∈ ℂ

Proof of Theorem 7cn
StepHypRef Expression
1 df-7 12220 . 2 7 = (6 + 1)
2 6cn 12243 . . 3 6 ∈ ℂ
3 ax-1cn 11108 . . 3 1 ∈ ℂ
42, 3addcli 11160 . 2 (6 + 1) ∈ ℂ
51, 4eqeltri 2834 1 7 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  (class class class)co 7356  cc 11048  1c1 11051   + caddc 11053  6c6 12211  7c7 12212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-1cn 11108  ax-addcl 11110
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2728  df-clel 2814  df-2 12215  df-3 12216  df-4 12217  df-5 12218  df-6 12219  df-7 12220
This theorem is referenced by:  8cn  12249  8m1e7  12285  7p2e9  12313  7p3e10  12692  7t2e14  12726  7t4e28  12728  7t7e49  12731  cos2bnd  16069  23prm  16990  139prm  16995  163prm  16996  317prm  16997  631prm  16998  1259lem1  17002  1259lem2  17003  1259lem3  17004  1259lem4  17005  1259lem5  17006  1259prm  17007  2503lem1  17008  2503lem2  17009  2503lem3  17010  4001lem1  17012  4001lem4  17015  4001prm  17016  log2ublem3  26296  log2ub  26297  bclbnd  26626  bposlem8  26637  2lgslem3d  26745  ex-prmo  29350  hgt750lem  33204  hgt750lem2  33205  60lcm7e420  40457  3exp7  40500  3lexlogpow5ineq1  40501  aks4d1p1  40523  235t711  40782  ex-decpmul  40783  3cubeslem3r  40987  fmtno5lem4  45719  257prm  45724  fmtno4nprmfac193  45737  fmtno5fac  45745  m3prm  45755  139prmALT  45759  127prm  45762  m7prm  45763  2exp340mod341  45896  8exp8mod9  45899
  Copyright terms: Public domain W3C validator