![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3cn | Structured version Visualization version GIF version |
Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.) |
Ref | Expression |
---|---|
3cn | ⊢ 3 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3re 11297 | . 2 ⊢ 3 ∈ ℝ | |
2 | 1 | recni 10255 | 1 ⊢ 3 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2145 ℂcc 10137 3c3 11274 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-resscn 10196 ax-1cn 10197 ax-icn 10198 ax-addcl 10199 ax-addrcl 10200 ax-mulcl 10201 ax-mulrcl 10202 ax-i2m1 10207 ax-1ne0 10208 ax-rrecex 10211 ax-cnre 10212 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-dif 3727 df-un 3729 df-in 3731 df-ss 3738 df-nul 4065 df-if 4227 df-sn 4318 df-pr 4320 df-op 4324 df-uni 4576 df-br 4788 df-iota 5995 df-fv 6040 df-ov 6797 df-2 11282 df-3 11283 |
This theorem is referenced by: 3ex 11299 4m1e3 11341 3p2e5 11363 3p3e6 11364 4p4e8 11367 5p4e9 11370 6p4e10OLD 11374 3t1e3 11381 3t2e6 11382 3t3e9 11383 8th4div3 11455 halfpm6th 11456 6p4e10 11800 9t8e72 11871 halfthird 11887 fzo0to42pr 12764 sq3 13169 expnass 13178 fac3 13272 4bc3eq4 13320 sqrlem7 14198 caurcvgr 14613 bpoly2 14995 bpoly3 14996 bpoly4 14997 sin01bnd 15122 cos01bnd 15123 cos1bnd 15124 cos2bnd 15125 cos01gt0 15128 rpnnen2lem3 15152 rpnnen2lem11 15160 3dvdsdec 15264 3dvdsdecOLD 15265 3dvds2dec 15266 3lcm2e6woprm 15537 prmo3 15953 2exp6 16003 2exp16 16005 7prm 16025 13prm 16031 17prm 16032 19prm 16033 37prm 16036 43prm 16037 83prm 16038 139prm 16039 163prm 16040 317prm 16041 631prm 16042 prmo4 16043 1259lem1 16046 1259lem2 16047 1259lem3 16048 1259lem4 16049 1259lem5 16050 1259prm 16051 2503lem1 16052 2503lem2 16053 2503lem3 16054 2503prm 16055 4001lem1 16056 4001lem2 16057 4001lem3 16058 4001lem4 16059 4001prm 16060 iblitg 23756 tangtx 24479 sincos6thpi 24489 sincos3rdpi 24490 pige3 24491 ang180lem2 24762 1cubr 24791 dcubic1lem 24792 dcubic2 24793 dcubic1 24794 dcubic 24795 mcubic 24796 cubic2 24797 cubic 24798 binom4 24799 quart1cl 24803 quart1lem 24804 quart1 24805 quartlem1 24806 quartlem3 24808 log2cnv 24893 log2tlbnd 24894 log2ublem2 24896 log2ublem3 24897 log2ub 24898 basellem5 25033 basellem8 25036 basellem9 25037 cht3 25121 ppiub 25151 chtub 25159 bclbnd 25227 bposlem6 25236 bposlem8 25238 bposlem9 25239 lgsdir2lem1 25272 lgsdir2lem5 25276 2lgslem3b 25344 2lgslem3d 25346 2lgsoddprmlem3c 25359 2lgsoddprmlem3d 25360 pntibndlem1 25500 pntlemk 25517 ex-opab 27632 ex-exp 27650 ex-dvds 27656 ex-gcd 27657 ex-lcm 27658 ex-prmo 27659 ex-ind-dvds 27661 fib5 30808 fib6 30809 hgt750lem 31070 hgt750lem2 31071 hgt750leme 31077 problem4 31901 problem5 31902 sinccvglem 31905 pigt3 33736 mblfinlem3 33782 itg2addnclem2 33795 itg2addnclem3 33796 heiborlem6 33948 heiborlem7 33949 jm2.23 38090 inductionexd 38980 lhe4.4ex1a 39055 stoweidlem13 40748 stoweidlem26 40761 stoweidlem34 40769 wallispilem4 40803 wallispi2lem1 40806 fmtno5lem1 41994 fmtno5lem2 41995 257prm 42002 fmtno4prmfac 42013 fmtno4nprmfac193 42015 139prmALT 42040 127prm 42044 mod42tp1mod8 42048 3exp4mod41 42062 41prothprmlem2 42064 6even 42149 gbpart8 42185 sbgoldbwt 42194 sbgoldbst 42195 evengpop3 42215 evengpoap3 42216 nnsum4primeseven 42217 nnsum4primesevenALTV 42218 2t6m3t4e0 42655 linevalexample 42713 zlmodzxzequa 42814 zlmodzxzequap 42817 |
Copyright terms: Public domain | W3C validator |