Theorem 7cn 12334

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 12308	. 2 ⊢ 7 = (6 + 1)
2		6cn 12331	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11187	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11241	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2830	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127  1c1 11130   + caddc 11132  6c6 12299  7c7 12300

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11187  ax-addcl 11189

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809  df-2 12303  df-3 12304  df-4 12305  df-5 12306  df-6 12307  df-7 12308

This theorem is referenced by:  8cn  12337  8m1e7  12373  7p2e9  12401  7p3e10  12783  7t2e14  12817  7t4e28  12819  7t7e49  12822  cos2bnd  16206  23prm  17138  139prm  17143  163prm  17144  317prm  17145  631prm  17146  1259lem1  17150  1259lem2  17151  1259lem3  17152  1259lem4  17153  1259lem5  17154  1259prm  17155  2503lem1  17156  2503lem2  17157  2503lem3  17158  4001lem1  17160  4001lem4  17163  4001prm  17164  log2ublem3  26910  log2ub  26911  bclbnd  27243  bposlem8  27254  2lgslem3d  27362  ex-prmo  30440  hgt750lem  34683  hgt750lem2  34684  60lcm7e420  42023  3exp7  42066  3lexlogpow5ineq1  42067  aks4d1p1  42089  sq7  42345  235t711  42354  ex-decpmul  42355  3cubeslem3r  42710  fmtno5lem4  47570  257prm  47575  fmtno4nprmfac193  47588  fmtno5fac  47596  m3prm  47606  139prmALT  47610  127prm  47613  m7prm  47614  2exp340mod341  47747  8exp8mod9  47750