Theorem 7cn 12240

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 12214	. 2 ⊢ 7 = (6 + 1)
2		6cn 12237	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11086	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11140	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026  1c1 11029   + caddc 11031  6c6 12205  7c7 12206

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 11086  ax-addcl 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12209  df-3 12210  df-4 12211  df-5 12212  df-6 12213  df-7 12214

This theorem is referenced by:  8cn  12243  8m1e7  12274  7p2e9  12302  7p3e10  12684  7t2e14  12718  7t4e28  12720  7t7e49  12723  cos2bnd  16115  23prm  17048  139prm  17053  163prm  17054  317prm  17055  631prm  17056  1259lem1  17060  1259lem2  17061  1259lem3  17062  1259lem4  17063  1259lem5  17064  1259prm  17065  2503lem1  17066  2503lem2  17067  2503lem3  17068  4001lem1  17070  4001lem4  17073  4001prm  17074  log2ublem3  26874  log2ub  26875  bclbnd  27207  bposlem8  27218  2lgslem3d  27326  ex-prmo  30421  hgt750lem  34621  hgt750lem2  34622  60lcm7e420  41986  3exp7  42029  3lexlogpow5ineq1  42030  aks4d1p1  42052  sq7  42272  235t711  42281  ex-decpmul  42282  3cubeslem3r  42663  fmtno5lem4  47544  257prm  47549  fmtno4nprmfac193  47562  fmtno5fac  47570  m3prm  47580  139prmALT  47584  127prm  47587  m7prm  47588  2exp340mod341  47721  8exp8mod9  47724