Theorem 7cn 12387

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

Step	Hyp	Ref	Expression
1		df-7 12361	. 2 ⊢ 7 = (6 + 1)
2		6cn 12384	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11242	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11296	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2840	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  1c1 11185   + caddc 11187  6c6 12352  7c7 12353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-addcl 11244

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361

This theorem is referenced by:  8cn  12390  8m1e7  12426  7p2e9  12454  7p3e10  12833  7t2e14  12867  7t4e28  12869  7t7e49  12872  cos2bnd  16236  23prm  17166  139prm  17171  163prm  17172  317prm  17173  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  1259prm  17183  2503lem1  17184  2503lem2  17185  2503lem3  17186  4001lem1  17188  4001lem4  17191  4001prm  17192  log2ublem3  27009  log2ub  27010  bclbnd  27342  bposlem8  27353  2lgslem3d  27461  ex-prmo  30491  hgt750lem  34628  hgt750lem2  34629  60lcm7e420  41967  3exp7  42010  3lexlogpow5ineq1  42011  aks4d1p1  42033  sq7  42284  235t711  42293  ex-decpmul  42294  3cubeslem3r  42643  fmtno5lem4  47430  257prm  47435  fmtno4nprmfac193  47448  fmtno5fac  47456  m3prm  47466  139prmALT  47470  127prm  47473  m7prm  47474  2exp340mod341  47607  8exp8mod9  47610