![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 7cn | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
7cn | ⊢ 7 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-7 12220 | . 2 ⊢ 7 = (6 + 1) | |
2 | 6cn 12243 | . . 3 ⊢ 6 ∈ ℂ | |
3 | ax-1cn 11108 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 2, 3 | addcli 11160 | . 2 ⊢ (6 + 1) ∈ ℂ |
5 | 1, 4 | eqeltri 2834 | 1 ⊢ 7 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 (class class class)co 7356 ℂcc 11048 1c1 11051 + caddc 11053 6c6 12211 7c7 12212 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-1cn 11108 ax-addcl 11110 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2728 df-clel 2814 df-2 12215 df-3 12216 df-4 12217 df-5 12218 df-6 12219 df-7 12220 |
This theorem is referenced by: 8cn 12249 8m1e7 12285 7p2e9 12313 7p3e10 12692 7t2e14 12726 7t4e28 12728 7t7e49 12731 cos2bnd 16069 23prm 16990 139prm 16995 163prm 16996 317prm 16997 631prm 16998 1259lem1 17002 1259lem2 17003 1259lem3 17004 1259lem4 17005 1259lem5 17006 1259prm 17007 2503lem1 17008 2503lem2 17009 2503lem3 17010 4001lem1 17012 4001lem4 17015 4001prm 17016 log2ublem3 26296 log2ub 26297 bclbnd 26626 bposlem8 26637 2lgslem3d 26745 ex-prmo 29350 hgt750lem 33204 hgt750lem2 33205 60lcm7e420 40457 3exp7 40500 3lexlogpow5ineq1 40501 aks4d1p1 40523 235t711 40782 ex-decpmul 40783 3cubeslem3r 40987 fmtno5lem4 45719 257prm 45724 fmtno4nprmfac193 45737 fmtno5fac 45745 m3prm 45755 139prmALT 45759 127prm 45762 m7prm 45763 2exp340mod341 45896 8exp8mod9 45899 |
Copyright terms: Public domain | W3C validator |