![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 0cn | Structured version Visualization version Unicode version |
Description: 0 is a complex number. See also 0cnALT 9864. (Contributed by NM, 19-Feb-2005.) |
Ref | Expression |
---|---|
0cn |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-i2m1 9607 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax-icn 9598 |
. . . 4
![]() ![]() ![]() ![]() | |
3 | mulcl 9623 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 2, 3 | mp2an 678 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | ax-1cn 9597 |
. . 3
![]() ![]() ![]() ![]() | |
6 | addcl 9621 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 4, 5, 6 | mp2an 678 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 7 | eqeltrri 2526 |
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 1669 ax-4 1682 ax-5 1758 ax-ext 2431 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-mulcl 9601 ax-i2m1 9607 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 df-cleq 2444 df-clel 2447 |
This theorem is referenced by: 0cnd 9636 c0ex 9637 1re 9642 00id 9808 mul02lem1 9809 mul02 9811 mul01 9812 addid1 9813 addid2 9816 negcl 9875 subid 9893 subid1 9894 neg0 9920 negid 9921 negsub 9922 subneg 9923 negneg 9924 negeq0 9928 negsubdi 9930 renegcli 9935 mulneg1 10055 msqge0 10135 ixi 10241 muleqadd 10256 div0 10298 ofsubge0 10608 0m0e0 10719 elznn0 10952 ser0 12265 0exp0e1 12277 0exp 12307 sq0 12366 sqeqor 12388 binom2 12389 bcval5 12503 s1co 12930 shftval3 13139 shftidt2 13144 cjne0 13226 sqrt0 13305 abs0 13348 abs00bd 13354 abs2dif 13395 clim0 13570 climz 13613 serclim0 13641 rlimneg 13710 sumrblem 13777 fsumcvg 13778 summolem2a 13781 sumss 13790 fsumss 13791 fsumcvg2 13793 fsumsplit 13806 sumsplit 13829 fsumrelem 13867 fsumrlim 13871 fsumo1 13872 0fallfac 14090 0risefac 14091 binomfallfac 14094 fsumcube 14113 ef0 14145 eftlub 14163 sin0 14203 tan0 14205 divalglem9 14381 divalglem9OLD 14382 sadadd2lem2 14424 sadadd3 14435 bezout 14510 pcmpt2 14838 prmreclem2 14861 4sqlem11 14899 ramcl 14987 odadd1 17486 cnaddablx 17506 cnaddabl 17507 frgpnabllem1 17509 cncrng 18989 cnfld0 18992 cnbl0 21794 cnblcld 21795 cnfldnm 21799 xrge0gsumle 21851 xrge0tsms 21852 cnheibor 21983 csscld 22220 clsocv 22221 cnflduss 22323 cnfldcusp 22324 rrxmvallem 22358 rrxmval 22359 mbfss 22602 mbfmulc2lem 22603 0plef 22630 0pledm 22631 itg1ge0 22644 itg1addlem4 22657 itg2splitlem 22706 itg2addlem 22716 ibl0 22744 iblcnlem 22746 iblss2 22763 itgss3 22772 dvconst 22871 dvcnp2 22874 dvrec 22909 dvexp3 22930 dveflem 22931 dvef 22932 dv11cn 22953 lhop1lem 22965 plyun0 23151 plyeq0lem 23164 coeeulem 23178 coeeu 23179 coef3 23186 dgrle 23197 0dgrb 23200 coefv0 23202 coemulc 23209 coe1termlem 23212 coe1term 23213 dgr0 23216 dgrmulc 23225 dgrcolem2 23228 vieta1lem2 23264 iaa 23281 aareccl 23282 aalioulem3 23290 taylthlem2 23329 psercn 23381 pserdvlem2 23383 abelthlem2 23387 abelthlem3 23388 abelthlem5 23390 abelthlem7 23393 abelth 23396 sin2kpi 23438 cos2kpi 23439 sinkpi 23474 efopn 23603 logtayl 23605 cxpval 23609 0cxp 23611 cxpexp 23613 cxpcl 23619 cxpge0 23628 mulcxplem 23629 mulcxp 23630 cxpmul2 23634 dvsqrt 23682 dvcnsqrt 23684 cxpcn3 23688 abscxpbnd 23693 efrlim 23895 ftalem2 23998 ftalem3 23999 ftalem4 24000 ftalem5 24001 ftalem4OLD 24002 ftalem5OLD 24003 ftalem7 24005 prmorcht 24105 muinv 24122 1sgm2ppw 24128 logfacbnd3 24151 logexprlim 24153 dchrelbas2 24165 dchrmulid2 24180 dchrfi 24183 dchrinv 24189 lgsdir2 24256 lgsdir 24258 dchrvmasumiflem1 24339 dchrvmasumiflem2 24340 rpvmasum2 24350 log2sumbnd 24382 selberg2lem 24388 logdivbnd 24394 ax5seglem8 24966 axlowdimlem6 24977 axlowdimlem13 24984 ex-co 25888 avril1 25900 cnaddablo 26078 cnid 26079 addinv 26080 vc0 26188 vcz 26189 vcoprne 26198 ipasslem8 26478 siilem2 26493 hvmul0 26677 hi01 26749 norm-iii 26793 h1de2ctlem 27208 pjmuli 27342 pjneli 27376 eigre 27488 eigorth 27491 elnlfn 27581 0cnfn 27633 0lnfn 27638 lnopunilem2 27664 xrge0tsmsd 28548 qqh0 28788 qqhcn 28795 eulerpartlemgs2 29213 sgnneg 29411 subfacp1lem6 29908 sinccvglem 30316 abs2sqle 30324 abs2sqlt 30325 tan2h 31937 poimirlem16 31956 poimirlem19 31959 poimirlem31 31971 mblfinlem2 31978 ovoliunnfl 31982 voliunnfl 31984 dvtanlem 31990 ftc1anclem5 32021 cntotbnd 32128 flcidc 36040 dvconstbi 36683 expgrowth 36684 dvradcnv2 36696 binomcxplemdvbinom 36702 binomcxplemnotnn0 36705 negcncfg 37758 ioodvbdlimc1 37807 ioodvbdlimc2 37810 itgsinexplem1 37830 stoweidlem26 37886 stoweidlem36 37897 stoweidlem55 37916 stirlinglem8 37943 fourierdlem103 38073 sqwvfoura 38092 sqwvfourb 38093 ovn0lem 38387 nn0sumshdiglemA 40483 nn0sumshdiglemB 40484 nn0sumshdiglem1 40485 sec0 40533 |
Copyright terms: Public domain | W3C validator |