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

Theorem 7cn 12248
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 12222 . 2 7 = (6 + 1)
2 6cn 12245 . . 3 6 ∈ ℂ
3 ax-1cn 11110 . . 3 1 ∈ ℂ
42, 3addcli 11162 . 2 (6 + 1) ∈ ℂ
51, 4eqeltri 2834 1 7 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 7358  cc 11050  1c1 11053   + caddc 11055  6c6 12213  7c7 12214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11110  ax-addcl 11112
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-clel 2815  df-2 12217  df-3 12218  df-4 12219  df-5 12220  df-6 12221  df-7 12222
This theorem is referenced by:  8cn  12251  8m1e7  12287  7p2e9  12315  7p3e10  12694  7t2e14  12728  7t4e28  12730  7t7e49  12733  cos2bnd  16071  23prm  16992  139prm  16997  163prm  16998  317prm  16999  631prm  17000  1259lem1  17004  1259lem2  17005  1259lem3  17006  1259lem4  17007  1259lem5  17008  1259prm  17009  2503lem1  17010  2503lem2  17011  2503lem3  17012  4001lem1  17014  4001lem4  17017  4001prm  17018  log2ublem3  26301  log2ub  26302  bclbnd  26631  bposlem8  26642  2lgslem3d  26750  ex-prmo  29406  hgt750lem  33267  hgt750lem2  33268  60lcm7e420  40470  3exp7  40513  3lexlogpow5ineq1  40514  aks4d1p1  40536  235t711  40808  ex-decpmul  40809  3cubeslem3r  41013  fmtno5lem4  45755  257prm  45760  fmtno4nprmfac193  45773  fmtno5fac  45781  m3prm  45791  139prmALT  45795  127prm  45798  m7prm  45799  2exp340mod341  45932  8exp8mod9  45935
  Copyright terms: Public domain W3C validator