Theorem 7cn 12243

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7360  ℂcc 11028  1c1 11031   + caddc 11033  6c6 12208  7c7 12209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11088  ax-addcl 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12212  df-3 12213  df-4 12214  df-5 12215  df-6 12216  df-7 12217

This theorem is referenced by:  8cn  12246  8m1e7  12277  7p2e9  12305  7p3e10  12686  7t2e14  12720  7t4e28  12722  7t7e49  12725  cos2bnd  16117  23prm  17050  139prm  17055  163prm  17056  317prm  17057  631prm  17058  1259lem1  17062  1259lem2  17063  1259lem3  17064  1259lem4  17065  1259lem5  17066  1259prm  17067  2503lem1  17068  2503lem2  17069  2503lem3  17070  4001lem1  17072  4001lem4  17075  4001prm  17076  log2ublem3  26918  log2ub  26919  bclbnd  27251  bposlem8  27262  2lgslem3d  27370  ex-prmo  30517  hgt750lem  34789  hgt750lem2  34790  60lcm7e420  42301  3exp7  42344  3lexlogpow5ineq1  42345  aks4d1p1  42367  sq7  42587  235t711  42596  ex-decpmul  42597  3cubeslem3r  42965  fmtno5lem4  47838  257prm  47843  fmtno4nprmfac193  47856  fmtno5fac  47864  m3prm  47874  139prmALT  47878  127prm  47881  m7prm  47882  2exp340mod341  48015  8exp8mod9  48018