Theorem 7cn 12331

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 12304	. 2 ⊢ 7 = (6 + 1)
2		6cn 12328	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11154	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11211	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2865	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2149  (class class class)co 7408  ℂcc 11094  1c1 11097   + caddc 11099  6c6 12295  7c7 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11154  ax-addcl 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-2 12299  df-3 12300  df-4 12301  df-5 12302  df-6 12303  df-7 12304

This theorem is referenced by:  8cn  12334  8m1e7  12369  7p2e9  12397  7p3e10  12787  7t2e14  12821  7t4e28  12823  7t7e49  12826  cos2bnd  16240  23prm  17175  139prm  17180  163prm  17181  317prm  17182  631prm  17183  1259lem1  17187  1259lem2  17188  1259lem3  17189  1259lem4  17190  1259lem5  17191  1259prm  17192  2503lem1  17193  2503lem2  17194  2503lem3  17195  4001lem1  17197  4001lem4  17200  4001prm  17201  log2ublem3  27075  log2ub  27076  bclbnd  27406  bposlem8  27417  2lgslem3d  27525  ex-prmo  30747  hgt750lem  34979  hgt750lem2  34980  60lcm7e420  42662  3exp7  42705  3lexlogpow5ineq1  42706  aks4d1p1  42728  sq7  42940  235t711  42949  ex-decpmul  42950  3cubeslem3r  43303  fmtno5lem4  48190  257prm  48195  fmtno4nprmfac193  48208  fmtno5fac  48216  m3prm  48226  139prmALT  48230  127prm  48233  m7prm  48234  ppivalnn4  48261  2exp340mod341  48380  8exp8mod9  48383