Theorem 7cn 11972

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 11946	. 2 ⊢ 7 = (6 + 1)
2		6cn 11969	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 10835	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10887	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2836	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2112  (class class class)co 7252  ℂcc 10775  1c1 10778   + caddc 10780  6c6 11937  7c7 11938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710  ax-1cn 10835  ax-addcl 10837

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2731  df-clel 2818  df-2 11941  df-3 11942  df-4 11943  df-5 11944  df-6 11945  df-7 11946

This theorem is referenced by:  8cn  11975  8m1e7  12011  7p2e9  12039  7p3e10  12416  7t2e14  12450  7t4e28  12452  7t7e49  12455  cos2bnd  15800  23prm  16723  139prm  16728  163prm  16729  317prm  16730  631prm  16731  1259lem1  16735  1259lem2  16736  1259lem3  16737  1259lem4  16738  1259lem5  16739  1259prm  16740  2503lem1  16741  2503lem2  16742  2503lem3  16743  4001lem1  16745  4001lem4  16748  4001prm  16749  log2ublem3  25978  log2ub  25979  bclbnd  26308  bposlem8  26319  2lgslem3d  26427  ex-prmo  28699  hgt750lem  32506  hgt750lem2  32507  60lcm7e420  39925  3exp7  39968  3lexlogpow5ineq1  39969  aks4d1p1  39990  235t711  40212  ex-decpmul  40213  3cubeslem3r  40397  fmtno5lem4  44869  257prm  44874  fmtno4nprmfac193  44887  fmtno5fac  44895  m3prm  44905  139prmALT  44909  127prm  44912  m7prm  44913  2exp340mod341  45046  8exp8mod9  45049