![]() |
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 12331 | . 2 ⊢ 6 = (5 + 1) | |
2 | 5cn 12352 | . . 3 ⊢ 5 ∈ ℂ | |
3 | ax-1cn 11216 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 2, 3 | addcli 11270 | . 2 ⊢ (5 + 1) ∈ ℂ |
5 | 1, 4 | eqeltri 2822 | 1 ⊢ 6 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 (class class class)co 7424 ℂcc 11156 1c1 11159 + caddc 11161 5c5 12322 6c6 12323 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-1cn 11216 ax-addcl 11218 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-clel 2803 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 |
This theorem is referenced by: 7cn 12358 7m1e6 12396 6p2e8 12423 6p3e9 12424 halfpm6th 12485 6p4e10 12801 6t2e12 12833 6t3e18 12834 6t5e30 12836 5recm6rec 12873 bpoly2 16059 bpoly3 16060 bpoly4 16061 efi4p 16139 ef01bndlem 16186 cos01bnd 16188 3lcm2e6woprm 16616 6lcm4e12 16617 2exp8 17091 2exp11 17092 2exp16 17093 19prm 17120 83prm 17125 163prm 17127 317prm 17128 631prm 17129 1259lem1 17133 1259lem2 17134 1259lem3 17135 1259lem4 17136 1259lem5 17137 2503lem1 17139 2503lem2 17140 2503lem3 17141 2503prm 17142 4001lem1 17143 4001lem2 17144 4001lem4 17146 4001prm 17147 sincos6thpi 26543 sincos3rdpi 26544 1cubrlem 26869 log2ublem3 26976 log2ub 26977 basellem5 27113 basellem8 27116 ppiub 27233 bclbnd 27309 bposlem8 27320 bposlem9 27321 2lgslem3d 27428 2lgsoddprmlem3d 27442 ex-exp 30383 ex-bc 30385 ex-gcd 30390 ex-lcm 30391 hgt750lemd 34494 hgt750lem2 34498 problem5 35497 60gcd6e6 41703 60lcm7e420 41709 3exp7 41752 3lexlogpow5ineq1 41753 3lexlogpow5ineq5 41759 aks4d1p1p5 41774 aks4d1p1 41775 lhe4.4ex1a 44003 wallispi2lem2 45693 fmtno5lem1 47125 fmtno5lem4 47128 fmtno5 47129 fmtno4prmfac 47144 fmtno5faclem2 47152 fmtno5faclem3 47153 fmtno5fac 47154 flsqrt5 47166 139prmALT 47168 127prm 47171 mod42tp1mod8 47174 2t6m3t4e0 47727 zlmodzxzequa 47879 zlmodzxzequap 47882 |
Copyright terms: Public domain | W3C validator |