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

Theorem 7cn 11728
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 11702 . 2 7 = (6 + 1)
2 6cn 11725 . . 3 6 ∈ ℂ
3 ax-1cn 10593 . . 3 1 ∈ ℂ
42, 3addcli 10645 . 2 (6 + 1) ∈ ℂ
51, 4eqeltri 2912 1 7 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  (class class class)co 7149  cc 10533  1c1 10536   + caddc 10538  6c6 11693  7c7 11694
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796  ax-1cn 10593  ax-addcl 10595
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-clel 2896  df-2 11697  df-3 11698  df-4 11699  df-5 11700  df-6 11701  df-7 11702
This theorem is referenced by:  8cn  11731  8m1e7  11767  7p2e9  11795  7p3e10  12170  7t2e14  12204  7t4e28  12206  7t7e49  12209  cos2bnd  15541  23prm  16452  139prm  16457  163prm  16458  317prm  16459  631prm  16460  1259lem1  16464  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  1259prm  16469  2503lem1  16470  2503lem2  16471  2503lem3  16472  4001lem1  16474  4001lem4  16477  4001prm  16478  log2ublem3  25540  log2ub  25541  bclbnd  25870  bposlem8  25881  2lgslem3d  25989  ex-prmo  28250  hgt750lem  31982  hgt750lem2  31983  60lcm7e420  39249  3lexlogpow5ineq1  39292  235t711  39419  ex-decpmul  39420  3cubeslem3r  39548  fmtno5lem4  44003  257prm  44008  fmtno4nprmfac193  44021  fmtno5fac  44029  m3prm  44039  139prmALT  44043  127prm  44046  m7prm  44047  2exp340mod341  44181  8exp8mod9  44184
  Copyright terms: Public domain W3C validator