Theorem 7cn 12280

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 12254	. 2 ⊢ 7 = (6 + 1)
2		6cn 12277	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11126	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11180	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  1c1 11069   + caddc 11071  6c6 12245  7c7 12246

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-addcl 11128

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254

This theorem is referenced by:  8cn  12283  8m1e7  12314  7p2e9  12342  7p3e10  12724  7t2e14  12758  7t4e28  12760  7t7e49  12763  cos2bnd  16156  23prm  17089  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem1  17111  4001lem4  17114  4001prm  17115  log2ublem3  26858  log2ub  26859  bclbnd  27191  bposlem8  27202  2lgslem3d  27310  ex-prmo  30388  hgt750lem  34642  hgt750lem2  34643  60lcm7e420  41998  3exp7  42041  3lexlogpow5ineq1  42042  aks4d1p1  42064  sq7  42284  235t711  42293  ex-decpmul  42294  3cubeslem3r  42675  fmtno5lem4  47557  257prm  47562  fmtno4nprmfac193  47575  fmtno5fac  47583  m3prm  47593  139prmALT  47597  127prm  47600  m7prm  47601  2exp340mod341  47734  8exp8mod9  47737