![]() |
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 12221 | . 2 ⊢ 6 = (5 + 1) | |
2 | 5cn 12242 | . . 3 ⊢ 5 ∈ ℂ | |
3 | ax-1cn 11110 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 2, 3 | addcli 11162 | . 2 ⊢ (5 + 1) ∈ ℂ |
5 | 1, 4 | eqeltri 2834 | 1 ⊢ 6 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 (class class class)co 7358 ℂcc 11050 1c1 11053 + caddc 11055 5c5 12212 6c6 12213 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 ax-1cn 11110 ax-addcl 11112 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2729 df-clel 2815 df-2 12217 df-3 12218 df-4 12219 df-5 12220 df-6 12221 |
This theorem is referenced by: 7cn 12248 7m1e6 12286 6p2e8 12313 6p3e9 12314 halfpm6th 12375 6p4e10 12691 6t2e12 12723 6t3e18 12724 6t5e30 12726 5recm6rec 12763 bpoly2 15941 bpoly3 15942 bpoly4 15943 efi4p 16020 ef01bndlem 16067 cos01bnd 16069 3lcm2e6woprm 16492 6lcm4e12 16493 2exp8 16962 2exp11 16963 2exp16 16964 19prm 16991 83prm 16996 163prm 16998 317prm 16999 631prm 17000 1259lem1 17004 1259lem2 17005 1259lem3 17006 1259lem4 17007 1259lem5 17008 2503lem1 17010 2503lem2 17011 2503lem3 17012 2503prm 17013 4001lem1 17014 4001lem2 17015 4001lem4 17017 4001prm 17018 sincos6thpi 25875 sincos3rdpi 25876 1cubrlem 26194 log2ublem3 26301 log2ub 26302 basellem5 26437 basellem8 26440 ppiub 26555 bclbnd 26631 bposlem8 26642 bposlem9 26643 2lgslem3d 26750 2lgsoddprmlem3d 26764 ex-exp 29397 ex-bc 29399 ex-gcd 29404 ex-lcm 29405 hgt750lemd 33264 hgt750lem2 33268 problem5 34260 60gcd6e6 40464 60lcm7e420 40470 3exp7 40513 3lexlogpow5ineq1 40514 3lexlogpow5ineq5 40520 aks4d1p1p5 40535 aks4d1p1 40536 lhe4.4ex1a 42616 wallispi2lem2 44320 fmtno5lem1 45752 fmtno5lem4 45755 fmtno5 45756 fmtno4prmfac 45771 fmtno5faclem2 45779 fmtno5faclem3 45780 fmtno5fac 45781 flsqrt5 45793 139prmALT 45795 127prm 45798 mod42tp1mod8 45801 2t6m3t4e0 46431 zlmodzxzequa 46584 zlmodzxzequap 46587 |
Copyright terms: Public domain | W3C validator |