Theorem 7cn 12438

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 12411	. 2 ⊢ 7 = (6 + 1)
2		6cn 12435	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11259	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11316	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2857	1 ⊢ 7 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7421  ℂcc 11199  1c1 11202   + caddc 11204  6c6 12402  7c7 12403

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 11259  ax-addcl 11261

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-2 12406  df-3 12407  df-4 12408  df-5 12409  df-6 12410  df-7 12411

This theorem is used by:  8cn  12441  8m1e7  12476  7p2e9  12504  7p3e10  12895  7t2e14  12929  7t4e28  12931  7t7e49  12934  cos2bnd  16357  23prm  17298  83prm  17302  139prm  17303  163prm  17304  317prm  17305  631prm  17306  1259lem1  17310  1259lem2  17311  1259lem3  17312  1259lem4  17313  1259lem5  17314  1259prm  17315  2503lem1  17316  2503lem2  17317  2503lem3  17318  4001lem1  17320  4001lem4  17323  4001prm  17324  log2ublem3  27277  log2ub  27278  bclbnd  27608  bposlem8  27619  2lgslem3d  27727  ex-prmo  31061  hgt750lem  35281  hgt750lem2  35282  60lcm7e420  43062  3exp7  43105  3lexlogpow5ineq1  43106  aks4d1p1  43128  25or6to4  43258  1p8e9  43317  sq7  43355  235t711  43364  ex-decpmul  43365  3cubeslem3r  43699  fmtno5lem4  48642  257prm  48647  fmtno4nprmfac193  48660  fmtno5fac  48668  m3prm  48678  139prmALT  48682  127prm  48685  m7prm  48686  ppivalnn4  48713  2exp340mod341  48832  8exp8mod9  48835