Theorem 7cn 12256

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 12230	. 2 ⊢ 7 = (6 + 1)
2		6cn 12253	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11102	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11156	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042  1c1 11045   + caddc 11047  6c6 12221  7c7 12222

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 11102  ax-addcl 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230

This theorem is referenced by:  8cn  12259  8m1e7  12290  7p2e9  12318  7p3e10  12700  7t2e14  12734  7t4e28  12736  7t7e49  12739  cos2bnd  16132  23prm  17065  139prm  17070  163prm  17071  317prm  17072  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  1259prm  17082  2503lem1  17083  2503lem2  17084  2503lem3  17085  4001lem1  17087  4001lem4  17090  4001prm  17091  log2ublem3  26834  log2ub  26835  bclbnd  27167  bposlem8  27178  2lgslem3d  27286  ex-prmo  30361  hgt750lem  34615  hgt750lem2  34616  60lcm7e420  41971  3exp7  42014  3lexlogpow5ineq1  42015  aks4d1p1  42037  sq7  42257  235t711  42266  ex-decpmul  42267  3cubeslem3r  42648  fmtno5lem4  47530  257prm  47535  fmtno4nprmfac193  47548  fmtno5fac  47556  m3prm  47566  139prmALT  47570  127prm  47573  m7prm  47574  2exp340mod341  47707  8exp8mod9  47710