![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3cn | Structured version Visualization version Unicode version |
Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.) |
Ref | Expression |
---|---|
3cn |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3re 10710 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | recni 9680 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-resscn 9621 ax-1cn 9622 ax-icn 9623 ax-addcl 9624 ax-addrcl 9625 ax-mulcl 9626 ax-mulrcl 9627 ax-i2m1 9632 ax-1ne0 9633 ax-rrecex 9636 ax-cnre 9637 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-rab 2757 df-v 3058 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-uni 4212 df-br 4416 df-iota 5564 df-fv 5608 df-ov 6317 df-2 10695 df-3 10696 |
This theorem is referenced by: 3ex 10712 3m1e2 10753 4m1e3 10754 3p2e5 10770 3p3e6 10771 4p4e8 10774 5p4e9 10777 6p4e10 10781 3t1e3 10788 3t2e6 10789 3t3e9 10790 8th4div3 10861 halfpm6th 10862 9t8e72 11180 halfthird 11185 fzo0to42pr 12030 sq3 12403 expnass 12411 fac3 12497 4bc3eq4 12544 sqrlem7 13360 caurcvgr 13786 caurcvgrOLD 13787 bpoly2 14158 bpoly3 14159 bpoly4 14160 sin01bnd 14287 cos01bnd 14288 cos1bnd 14289 cos2bnd 14290 cos01gt0 14293 rpnnen2lem3 14317 rpnnen2lem11 14325 3lcm2e6woprm 14628 prmo3 15047 2exp6 15106 2exp16 15109 7prm 15130 13prm 15135 17prm 15136 19prm 15137 37prm 15140 43prm 15141 83prm 15142 139prm 15143 163prm 15144 317prm 15145 631prm 15146 prmo4 15147 1259lem1 15150 1259lem2 15151 1259lem3 15152 1259lem4 15153 1259lem5 15154 1259prm 15155 2503lem1 15156 2503lem2 15157 2503lem3 15158 2503prm 15159 4001lem1 15160 4001lem2 15161 4001lem3 15162 4001lem4 15163 4001prm 15164 iblitg 22774 tangtx 23508 sincos6thpi 23518 sincos3rdpi 23519 pige3 23520 ang180lem2 23787 1cubr 23816 dcubic1lem 23817 dcubic2 23818 dcubic1 23819 dcubic 23820 mcubic 23821 cubic2 23822 cubic 23823 binom4 23824 quart1cl 23828 quart1lem 23829 quart1 23830 quartlem1 23831 quartlem3 23833 log2cnv 23918 log2tlbnd 23919 log2ublem2 23921 log2ublem3 23922 log2ub 23923 basellem5 24059 basellem8 24062 basellem9 24063 cht3 24148 ppiub 24180 chtub 24188 bclbnd 24256 bposlem6 24265 bposlem8 24267 bposlem9 24268 lgsdir2lem1 24299 lgsdir2lem5 24303 pntibndlem1 24475 pntlemk 24492 extwwlkfablem2 25854 ex-opab 25930 ex-dvds 25946 ex-ind-dvds 25947 fib5 29286 fib6 29287 problem4 30348 problem5 30349 sinccvglem 30364 pigt3 31982 mblfinlem3 32023 itg2addnclem2 32038 itg2addnclem3 32039 heiborlem6 32192 heiborlem7 32193 jm2.23 35895 inductionexd 36637 lhe4.4ex1a 36721 stoweidlem13 37910 stoweidlem26 37923 stoweidlem34 37932 wallispilem4 37967 wallispi2lem1 37970 6even 38875 gbpart8 38906 bgoldbwt 38915 bgoldbst 38916 evengpop3 38930 evengpoap3 38931 nnsum4primeseven 38932 nnsum4primesevenALTV 38933 3exp4mod41 38953 41prothprmlem2 38955 2t6m3t4e0 40401 linevalexample 40460 zlmodzxzequa 40561 zlmodzxzequap 40564 |
Copyright terms: Public domain | W3C validator |