![]() |
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 11558 | . 2 ⊢ 6 = (5 + 1) | |
2 | 5cn 11579 | . . 3 ⊢ 5 ∈ ℂ | |
3 | ax-1cn 10448 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 2, 3 | addcli 10500 | . 2 ⊢ (5 + 1) ∈ ℂ |
5 | 1, 4 | eqeltri 2881 | 1 ⊢ 6 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2083 (class class class)co 7023 ℂcc 10388 1c1 10391 + caddc 10393 5c5 11549 6c6 11550 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-ext 2771 ax-1cn 10448 ax-addcl 10450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1766 df-cleq 2790 df-clel 2865 df-2 11554 df-3 11555 df-4 11556 df-5 11557 df-6 11558 |
This theorem is referenced by: 7cn 11585 7m1e6 11623 6p2e8 11650 6p3e9 11651 halfpm6th 11712 6p4e10 12024 6t2e12 12056 6t3e18 12057 6t5e30 12059 5recm6rec 12096 bpoly2 15248 bpoly3 15249 bpoly4 15250 efi4p 15327 ef01bndlem 15374 cos01bnd 15376 3lcm2e6woprm 15792 6lcm4e12 15793 2exp8 16256 2exp16 16257 19prm 16284 83prm 16289 163prm 16291 317prm 16292 631prm 16293 1259lem1 16297 1259lem2 16298 1259lem3 16299 1259lem4 16300 1259lem5 16301 2503lem1 16303 2503lem2 16304 2503lem3 16305 2503prm 16306 4001lem1 16307 4001lem2 16308 4001lem4 16310 4001prm 16311 sincos6thpi 24788 sincos3rdpi 24789 1cubrlem 25104 log2ublem3 25212 log2ub 25213 basellem5 25348 basellem8 25351 ppiub 25466 bclbnd 25542 bposlem8 25553 bposlem9 25554 2lgslem3d 25661 2lgsoddprmlem3d 25675 ex-exp 27917 ex-bc 27919 ex-gcd 27924 ex-lcm 27925 hgt750lemd 31532 hgt750lem2 31536 problem5 32522 lhe4.4ex1a 40220 wallispi2lem2 41921 fmtno5lem1 43219 fmtno5lem4 43222 fmtno5 43223 fmtno4prmfac 43238 fmtno5faclem2 43246 fmtno5faclem3 43247 fmtno5fac 43248 flsqrt5 43261 139prmALT 43263 127prm 43267 2exp11 43269 mod42tp1mod8 43271 2t6m3t4e0 43896 zlmodzxzequa 44053 zlmodzxzequap 44056 |
Copyright terms: Public domain | W3C validator |