| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 6cn | Structured version Visualization version GIF version | ||
| Description: The number 6 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 |
|---|---|
| 6cn | ⊢ 6 ∈ ℂ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-6 12243 | . 2 ⊢ 6 = (5 + 1) | |
| 2 | 5cn 12264 | . . 3 ⊢ 5 ∈ ℂ | |
| 3 | ax-1cn 11092 | . . 3 ⊢ 1 ∈ ℂ | |
| 4 | 2, 3 | addcli 11147 | . 2 ⊢ (5 + 1) ∈ ℂ |
| 5 | 1, 4 | eqeltri 2837 | 1 ⊢ 6 ∈ ℂ |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2121 (class class class)co 7359 ℂcc 11032 1c1 11035 + caddc 11037 5c5 12234 6c6 12235 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-ext 2713 ax-1cn 11092 ax-addcl 11094 |
| This theorem depends on definitions: df-bi 209 df-an 398 df-ex 1788 df-cleq 2733 df-clel 2816 df-2 12239 df-3 12240 df-4 12241 df-5 12242 df-6 12243 |
| This theorem is referenced by: 7cn 12270 7m1e6 12303 6p2e8 12330 6p3e9 12331 halfpm6th 12394 6p4e10 12711 6t2e12 12743 6t3e18 12744 6t5e30 12746 5recm6rec 12782 bpoly2 16017 bpoly3 16018 bpoly4 16019 efi4p 16099 ef01bndlem 16146 cos01bnd 16148 3lcm2e6woprm 16579 6lcm4e12 16580 2exp8 17054 2exp11 17055 2exp16 17056 19prm 17083 83prm 17088 163prm 17090 317prm 17091 631prm 17092 1259lem1 17096 1259lem2 17097 1259lem3 17098 1259lem4 17099 1259lem5 17100 2503lem1 17102 2503lem2 17103 2503lem3 17104 2503prm 17105 4001lem1 17106 4001lem2 17107 4001lem4 17109 4001prm 17110 sincos6thpi 26501 sincos3rdpi 26502 1cubrlem 26826 log2ublem3 26933 log2ub 26934 basellem5 27069 basellem8 27072 ppiub 27188 bclbnd 27264 bposlem8 27275 bposlem9 27276 2lgslem3d 27383 2lgsoddprmlem3d 27397 ex-exp 30540 ex-bc 30542 ex-gcd 30547 ex-lcm 30548 hgt750lemd 34842 hgt750lem2 34846 problem5 35910 60gcd6e6 42502 60lcm7e420 42508 3exp7 42551 3lexlogpow5ineq1 42552 3lexlogpow5ineq5 42558 aks4d1p1p5 42573 aks4d1p1 42574 sq6 42785 lhe4.4ex1a 44786 wallispi2lem2 46527 sin5tlem1 47348 sin5tlem4 47351 sin5tlem5 47352 fmtno5lem1 48043 fmtno5lem4 48046 fmtno5 48047 fmtno4prmfac 48062 fmtno5faclem2 48070 fmtno5faclem3 48071 fmtno5fac 48072 flsqrt5 48084 139prmALT 48086 127prm 48089 mod42tp1mod8 48092 2t6m3t4e0 48851 zlmodzxzequa 48999 zlmodzxzequap 49002 |
| Copyright terms: Public domain | W3C validator |