Theorem 7cn 12359

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 12332	. 2 ⊢ 7 = (6 + 1)
2		6cn 12356	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11182	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11239	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2856	1 ⊢ 7 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7413  ℂcc 11122  1c1 11125   + caddc 11127  6c6 12323  7c7 12324

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-1cn 11182  ax-addcl 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332

This theorem is used by:  8cn  12362  8m1e7  12397  7p2e9  12425  7p3e10  12816  7t2e14  12850  7t4e28  12852  7t7e49  12855  cos2bnd  16276  23prm  17211  83prm  17215  139prm  17216  163prm  17217  317prm  17218  631prm  17219  1259lem1  17223  1259lem2  17224  1259lem3  17225  1259lem4  17226  1259lem5  17227  1259prm  17228  2503lem1  17229  2503lem2  17230  2503lem3  17231  4001lem1  17233  4001lem4  17236  4001prm  17237  log2ublem3  27185  log2ub  27186  bclbnd  27516  bposlem8  27527  2lgslem3d  27635  ex-prmo  30939  hgt750lem  35159  hgt750lem2  35160  60lcm7e420  42876  3exp7  42919  3lexlogpow5ineq1  42920  aks4d1p1  42942  25or6to4  43072  1p8e9  43131  sq7  43171  235t711  43180  ex-decpmul  43181  3cubeslem3r  43532  fmtno5lem4  48459  257prm  48464  fmtno4nprmfac193  48477  fmtno5fac  48485  m3prm  48495  139prmALT  48499  127prm  48502  m7prm  48503  ppivalnn4  48530  2exp340mod341  48649  8exp8mod9  48652