Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0cn | Structured version Visualization version GIF version |
Description: 0 is a complex number. See also 0cnALT 10149. (Contributed by NM, 19-Feb-2005.) |
Ref | Expression |
---|---|
0cn | ⊢ 0 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-i2m1 9883 | . 2 ⊢ ((i · i) + 1) = 0 | |
2 | ax-icn 9874 | . . . 4 ⊢ i ∈ ℂ | |
3 | mulcl 9899 | . . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ) | |
4 | 2, 2, 3 | mp2an 704 | . . 3 ⊢ (i · i) ∈ ℂ |
5 | ax-1cn 9873 | . . 3 ⊢ 1 ∈ ℂ | |
6 | addcl 9897 | . . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ) | |
7 | 4, 5, 6 | mp2an 704 | . 2 ⊢ ((i · i) + 1) ∈ ℂ |
8 | 1, 7 | eqeltrri 2685 | 1 ⊢ 0 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1977 (class class class)co 6549 ℂcc 9813 0cc0 9815 1c1 9816 ici 9817 + caddc 9818 · cmul 9820 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-ext 2590 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-mulcl 9877 ax-i2m1 9883 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-cleq 2603 df-clel 2606 |
This theorem is referenced by: 0cnd 9912 c0ex 9913 1re 9918 00id 10090 mul02lem1 10091 mul02 10093 mul01 10094 addid1 10095 addid2 10098 negcl 10160 subid 10179 subid1 10180 neg0 10206 negid 10207 negsub 10208 subneg 10209 negneg 10210 negeq0 10214 negsubdi 10216 renegcli 10221 mulneg1 10345 msqge0 10428 ixi 10535 muleqadd 10550 div0 10594 ofsubge0 10896 0m0e0 11007 elznn0 11269 ser0 12715 0exp0e1 12727 0exp 12757 sq0 12817 sqeqor 12840 binom2 12841 bcval5 12967 s1co 13430 shftval3 13664 shftidt2 13669 cjne0 13751 sqrt0 13830 abs0 13873 abs00bd 13879 abs2dif 13920 clim0 14085 climz 14128 serclim0 14156 rlimneg 14225 sumrblem 14289 fsumcvg 14290 summolem2a 14293 sumss 14302 fsumss 14303 fsumcvg2 14305 fsumsplit 14318 sumsplit 14341 fsumrelem 14380 fsumrlim 14384 fsumo1 14385 0fallfac 14607 0risefac 14608 binomfallfac 14611 fsumcube 14630 ef0 14660 eftlub 14678 sin0 14718 tan0 14720 divalglem9 14962 sadadd2lem2 15010 sadadd3 15021 bezout 15098 pcmpt2 15435 4sqlem11 15497 ramcl 15571 4001lem2 15687 odadd1 18074 cnaddablx 18094 cnaddabl 18095 cnaddid 18096 frgpnabllem1 18099 cncrng 19586 cnfld0 19589 cnbl0 22387 cnblcld 22388 cnfldnm 22392 xrge0gsumle 22444 xrge0tsms 22445 cnheibor 22562 cnlmod 22748 csscld 22856 clsocv 22857 cnflduss 22960 cnfldcusp 22961 rrxmvallem 22995 rrxmval 22996 mbfss 23219 mbfmulc2lem 23220 0plef 23245 0pledm 23246 itg1ge0 23259 itg1addlem4 23272 itg2splitlem 23321 itg2addlem 23331 ibl0 23359 iblcnlem 23361 iblss2 23378 itgss3 23387 dvconst 23486 dvcnp2 23489 dvrec 23524 dvexp3 23545 dveflem 23546 dvef 23547 dv11cn 23568 lhop1lem 23580 plyun0 23757 plyeq0lem 23770 coeeulem 23784 coeeu 23785 coef3 23792 dgrle 23803 0dgrb 23806 coefv0 23808 coemulc 23815 coe1termlem 23818 coe1term 23819 dgr0 23822 dgrmulc 23831 dgrcolem2 23834 vieta1lem2 23870 iaa 23884 aareccl 23885 aalioulem3 23893 taylthlem2 23932 psercn 23984 pserdvlem2 23986 abelthlem2 23990 abelthlem3 23991 abelthlem5 23993 abelthlem7 23996 abelth 23999 sin2kpi 24039 cos2kpi 24040 sinkpi 24075 efopn 24204 logtayl 24206 cxpval 24210 0cxp 24212 cxpexp 24214 cxpcl 24220 cxpge0 24229 mulcxplem 24230 mulcxp 24231 cxpmul2 24235 dvsqrt 24283 dvcnsqrt 24285 cxpcn3 24289 abscxpbnd 24294 efrlim 24496 ftalem2 24600 ftalem3 24601 ftalem4 24602 ftalem5 24603 ftalem7 24605 prmorcht 24704 muinv 24719 1sgm2ppw 24725 logfacbnd3 24748 logexprlim 24750 dchrelbas2 24762 dchrmulid2 24777 dchrfi 24780 dchrinv 24786 lgsdir2 24855 lgsdir 24857 dchrvmasumiflem1 24990 dchrvmasumiflem2 24991 rpvmasum2 25001 log2sumbnd 25033 selberg2lem 25039 logdivbnd 25045 ax5seglem8 25616 axlowdimlem6 25627 axlowdimlem13 25634 ex-co 26687 avril1 26711 vc0 26813 vcz 26814 cnaddabloOLD 26820 cnidOLD 26821 ipasslem8 27076 siilem2 27091 hvmul0 27265 hi01 27337 norm-iii 27381 h1de2ctlem 27798 pjmuli 27932 pjneli 27966 eigre 28078 eigorth 28081 elnlfn 28171 0cnfn 28223 0lnfn 28228 lnopunilem2 28254 xrge0tsmsd 29116 qqh0 29356 qqhcn 29363 eulerpartlemgs2 29769 sgnneg 29929 subfacp1lem6 30421 sinccvglem 30820 abs2sqle 30828 abs2sqlt 30829 tan2h 32571 poimirlem16 32595 poimirlem19 32598 poimirlem31 32610 mblfinlem2 32617 ovoliunnfl 32621 voliunnfl 32623 dvtanlem 32629 ftc1anclem5 32659 cntotbnd 32765 flcidc 36763 dvconstbi 37555 expgrowth 37556 dvradcnv2 37568 binomcxplemdvbinom 37574 binomcxplemnotnn0 37577 xralrple3 38531 negcncfg 38766 ioodvbdlimc1 38823 ioodvbdlimc2 38825 itgsinexplem1 38845 stoweidlem26 38919 stoweidlem36 38929 stoweidlem55 38948 stirlinglem8 38974 fourierdlem103 39102 sqwvfoura 39121 sqwvfourb 39122 ovn0lem 39455 nn0sumshdiglemA 42211 nn0sumshdiglemB 42212 nn0sumshdiglem1 42213 sec0 42300 |
Copyright terms: Public domain | W3C validator |