Theorem 7cn 12430

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 12403	. 2 ⊢ 7 = (6 + 1)
2		6cn 12427	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11251	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11308	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2857	1 ⊢ 7 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7418  ℂcc 11191  1c1 11194   + caddc 11196  6c6 12394  7c7 12395

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 2733  ax-1cn 11251  ax-addcl 11253

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-2 12398  df-3 12399  df-4 12400  df-5 12401  df-6 12402  df-7 12403

This theorem is used by:  8cn  12433  8m1e7  12468  7p2e9  12496  7p3e10  12887  7t2e14  12921  7t4e28  12923  7t7e49  12926  cos2bnd  16349  23prm  17290  83prm  17294  139prm  17295  163prm  17296  317prm  17297  631prm  17298  1259lem1  17302  1259lem2  17303  1259lem3  17304  1259lem4  17305  1259lem5  17306  1259prm  17307  2503lem1  17308  2503lem2  17309  2503lem3  17310  4001lem1  17312  4001lem4  17315  4001prm  17316  log2ublem3  27269  log2ub  27270  bclbnd  27600  bposlem8  27611  2lgslem3d  27719  ex-prmo  31053  hgt750lem  35273  hgt750lem2  35274  60lcm7e420  43040  3exp7  43083  3lexlogpow5ineq1  43084  aks4d1p1  43106  25or6to4  43236  1p8e9  43295  sq7  43333  235t711  43342  ex-decpmul  43343  3cubeslem3r  43677  fmtno5lem4  48610  257prm  48615  fmtno4nprmfac193  48628  fmtno5fac  48636  m3prm  48646  139prmALT  48650  127prm  48653  m7prm  48654  ppivalnn4  48681  2exp340mod341  48800  8exp8mod9  48803