Theorem 7cn 12266

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 12240	. 2 ⊢ 7 = (6 + 1)
2		6cn 12263	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11087	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11142	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027  1c1 11030   + caddc 11032  6c6 12231  7c7 12232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-addcl 11089

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240

This theorem is referenced by:  8cn  12269  8m1e7  12300  7p2e9  12328  7p3e10  12710  7t2e14  12744  7t4e28  12746  7t7e49  12749  cos2bnd  16146  23prm  17080  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem1  17098  2503lem2  17099  2503lem3  17100  4001lem1  17102  4001lem4  17105  4001prm  17106  log2ublem3  26930  log2ub  26931  bclbnd  27261  bposlem8  27272  2lgslem3d  27380  ex-prmo  30547  hgt750lem  34835  hgt750lem2  34836  60lcm7e420  42495  3exp7  42538  3lexlogpow5ineq1  42539  aks4d1p1  42561  sq7  42773  235t711  42782  ex-decpmul  42783  3cubeslem3r  43136  fmtno5lem4  48034  257prm  48039  fmtno4nprmfac193  48052  fmtno5fac  48060  m3prm  48070  139prmALT  48074  127prm  48077  m7prm  48078  ppivalnn4  48105  2exp340mod341  48224  8exp8mod9  48227