Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0cn | Structured version Visualization version GIF version |
Description: Zero is a complex number. See also 0cnALT 10862. (Contributed by NM, 19-Feb-2005.) |
Ref | Expression |
---|---|
0cn | ⊢ 0 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-i2m1 10593 | . 2 ⊢ ((i · i) + 1) = 0 | |
2 | ax-icn 10584 | . . . 4 ⊢ i ∈ ℂ | |
3 | mulcl 10609 | . . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ) | |
4 | 2, 2, 3 | mp2an 688 | . . 3 ⊢ (i · i) ∈ ℂ |
5 | ax-1cn 10583 | . . 3 ⊢ 1 ∈ ℂ | |
6 | addcl 10607 | . . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ) | |
7 | 4, 5, 6 | mp2an 688 | . 2 ⊢ ((i · i) + 1) ∈ ℂ |
8 | 1, 7 | eqeltrri 2907 | 1 ⊢ 0 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 (class class class)co 7145 ℂcc 10523 0cc0 10525 1c1 10526 ici 10527 + caddc 10528 · cmul 10530 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 ax-1cn 10583 ax-icn 10584 ax-addcl 10585 ax-mulcl 10587 ax-i2m1 10593 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-clel 2890 |
This theorem is referenced by: 0cnd 10622 c0ex 10623 1re 10629 00id 10803 mul02lem1 10804 mul02 10806 mul01 10807 addid1 10808 addid2 10811 negcl 10874 subid 10893 subid1 10894 neg0 10920 negid 10921 negsub 10922 subneg 10923 negneg 10924 negeq0 10928 negsubdi 10930 renegcli 10935 mulneg1 11064 msqge0 11149 ixi 11257 muleqadd 11272 div0 11316 ofsubge0 11625 0m0e0 11745 nn0sscn 11890 elznn0 11984 ser0 13410 0exp0e1 13422 0exp 13452 sq0 13543 sqeqor 13566 binom2 13567 bcval5 13666 s1co 14183 shftval3 14423 shftidt2 14428 cjne0 14510 sqrt0 14589 abs0 14633 abs00bd 14639 abs2dif 14680 clim0 14851 climz 14894 serclim0 14922 rlimneg 14991 sumrblem 15056 fsumcvg 15057 summolem2a 15060 sumss 15069 fsumss 15070 fsumcvg2 15072 fsumsplit 15085 sumsplit 15111 fsumrelem 15150 fsumrlim 15154 fsumo1 15155 0fallfac 15379 0risefac 15380 binomfallfac 15383 fsumcube 15402 ef0 15432 eftlub 15450 sin0 15490 tan0 15492 divalglem9 15740 sadadd2lem2 15787 sadadd3 15798 bezout 15879 pcmpt2 16217 4sqlem11 16279 ramcl 16353 4001lem2 16463 odadd1 18897 cnaddablx 18917 cnaddabl 18918 cnaddid 18919 frgpnabllem1 18922 cncrng 20494 cnfld0 20497 cnbl0 23309 cnblcld 23310 cnfldnm 23314 xrge0gsumle 23368 xrge0tsms 23369 cnheibor 23486 cnlmod 23671 csscld 23779 clsocv 23780 cnflduss 23886 cnfldcusp 23887 rrxmvallem 23934 rrxmval 23935 mbfss 24174 mbfmulc2lem 24175 0plef 24200 0pledm 24201 itg1ge0 24214 itg1addlem4 24227 itg2splitlem 24276 itg2addlem 24286 ibl0 24314 iblcnlem 24316 iblss2 24333 itgss3 24342 dvconst 24441 dvcnp2 24444 dvrec 24479 dvexp3 24502 dveflem 24503 dv11cn 24525 lhop1lem 24537 plyun0 24714 plyeq0lem 24727 coeeulem 24741 coeeu 24742 coef3 24749 dgrle 24760 0dgrb 24763 coefv0 24765 coemulc 24772 coe1termlem 24775 coe1term 24776 dgr0 24779 dgrmulc 24788 dgrcolem2 24791 vieta1lem2 24827 iaa 24841 aareccl 24842 aalioulem3 24850 taylthlem2 24889 psercn 24941 pserdvlem2 24943 abelthlem2 24947 abelthlem3 24948 abelthlem5 24950 abelthlem7 24953 abelth 24956 sin2kpi 24996 cos2kpi 24997 sinkpi 25034 efopn 25168 logtayl 25170 cxpval 25174 0cxp 25176 cxpexp 25178 cxpcl 25184 cxpge0 25193 mulcxplem 25194 mulcxp 25195 cxpmul2 25199 dvsqrt 25250 dvcnsqrt 25252 cxpcn3 25256 abscxpbnd 25261 efrlim 25474 ftalem2 25578 ftalem3 25579 ftalem4 25580 ftalem5 25581 ftalem7 25583 prmorcht 25682 muinv 25697 1sgm2ppw 25703 logfacbnd3 25726 logexprlim 25728 dchrelbas2 25740 dchrmulid2 25755 dchrfi 25758 dchrinv 25764 lgsdir2 25833 lgsdir 25835 addsqnreup 25946 dchrvmasumiflem1 26004 dchrvmasumiflem2 26005 rpvmasum2 26015 log2sumbnd 26047 selberg2lem 26053 logdivbnd 26059 ax5seglem8 26649 axlowdimlem6 26660 axlowdimlem13 26667 ex-co 28144 avril1 28169 vc0 28278 vcz 28279 cnaddabloOLD 28285 cnidOLD 28286 ipasslem8 28541 siilem2 28556 hvmul0 28728 hi01 28800 norm-iii 28844 h1de2ctlem 29259 pjmuli 29393 pjneli 29427 eigre 29539 eigorth 29542 elnlfn 29632 0cnfn 29684 0lnfn 29689 lnopunilem2 29715 xrge0tsmsd 30619 qqh0 31124 qqhcn 31131 eulerpartlemgs2 31537 sgnneg 31697 breprexpnat 31804 hgt750lem2 31822 subfacp1lem6 32329 sinccvglem 32812 abs2sqle 32820 abs2sqlt 32821 tan2h 34765 poimirlem16 34789 poimirlem19 34792 poimirlem31 34804 mblfinlem2 34811 ovoliunnfl 34815 voliunnfl 34817 dvtanlem 34822 ftc1anclem5 34852 cntotbnd 34955 sn-1ne2 39036 fltnltalem 39152 flcidc 39652 dvconstbi 40543 expgrowth 40544 dvradcnv2 40556 binomcxplemdvbinom 40562 binomcxplemnotnn0 40565 xralrple3 41518 negcncfg 42040 ioodvbdlimc1 42094 ioodvbdlimc2 42096 itgsinexplem1 42115 stoweidlem26 42188 stoweidlem36 42198 stoweidlem55 42217 stirlinglem8 42243 fourierdlem103 42371 sqwvfoura 42390 sqwvfourb 42391 ovn0lem 42724 nn0sumshdiglemA 44607 nn0sumshdiglemB 44608 nn0sumshdiglem1 44609 sec0 44787 |
Copyright terms: Public domain | W3C validator |