![]() |
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 10308. (Contributed by NM, 19-Feb-2005.) |
Ref | Expression |
---|---|
0cn | ⊢ 0 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-i2m1 10042 | . 2 ⊢ ((i · i) + 1) = 0 | |
2 | ax-icn 10033 | . . . 4 ⊢ i ∈ ℂ | |
3 | mulcl 10058 | . . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ) | |
4 | 2, 2, 3 | mp2an 708 | . . 3 ⊢ (i · i) ∈ ℂ |
5 | ax-1cn 10032 | . . 3 ⊢ 1 ∈ ℂ | |
6 | addcl 10056 | . . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ) | |
7 | 4, 5, 6 | mp2an 708 | . 2 ⊢ ((i · i) + 1) ∈ ℂ |
8 | 1, 7 | eqeltrri 2727 | 1 ⊢ 0 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2030 (class class class)co 6690 ℂcc 9972 0cc0 9974 1c1 9975 ici 9976 + caddc 9977 · cmul 9979 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-ext 2631 ax-1cn 10032 ax-icn 10033 ax-addcl 10034 ax-mulcl 10036 ax-i2m1 10042 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1745 df-cleq 2644 df-clel 2647 |
This theorem is referenced by: 0cnd 10071 c0ex 10072 1re 10077 00id 10249 mul02lem1 10250 mul02 10252 mul01 10253 addid1 10254 addid2 10257 negcl 10319 subid 10338 subid1 10339 neg0 10365 negid 10366 negsub 10367 subneg 10368 negneg 10369 negeq0 10373 negsubdi 10375 renegcli 10380 mulneg1 10504 msqge0 10587 ixi 10694 muleqadd 10709 div0 10753 ofsubge0 11057 0m0e0 11168 elznn0 11430 ser0 12893 0exp0e1 12905 0exp 12935 sq0 12995 sqeqor 13018 binom2 13019 bcval5 13145 s1co 13625 shftval3 13860 shftidt2 13865 cjne0 13947 sqrt0 14026 abs0 14069 abs00bd 14075 abs2dif 14116 clim0 14281 climz 14324 serclim0 14352 rlimneg 14421 sumrblem 14486 fsumcvg 14487 summolem2a 14490 sumss 14499 fsumss 14500 fsumcvg2 14502 fsumsplit 14515 sumsplit 14543 fsumrelem 14583 fsumrlim 14587 fsumo1 14588 0fallfac 14812 0risefac 14813 binomfallfac 14816 fsumcube 14835 ef0 14865 eftlub 14883 sin0 14923 tan0 14925 divalglem9 15171 sadadd2lem2 15219 sadadd3 15230 bezout 15307 pcmpt2 15644 4sqlem11 15706 ramcl 15780 4001lem2 15896 odadd1 18297 cnaddablx 18317 cnaddabl 18318 cnaddid 18319 frgpnabllem1 18322 cncrng 19815 cnfld0 19818 cnbl0 22624 cnblcld 22625 cnfldnm 22629 xrge0gsumle 22683 xrge0tsms 22684 cnheibor 22801 cnlmod 22986 csscld 23094 clsocv 23095 cnflduss 23198 cnfldcusp 23199 rrxmvallem 23233 rrxmval 23234 mbfss 23458 mbfmulc2lem 23459 0plef 23484 0pledm 23485 itg1ge0 23498 itg1addlem4 23511 itg2splitlem 23560 itg2addlem 23570 ibl0 23598 iblcnlem 23600 iblss2 23617 itgss3 23626 dvconst 23725 dvcnp2 23728 dvrec 23763 dvexp3 23786 dveflem 23787 dvef 23788 dv11cn 23809 lhop1lem 23821 plyun0 23998 plyeq0lem 24011 coeeulem 24025 coeeu 24026 coef3 24033 dgrle 24044 0dgrb 24047 coefv0 24049 coemulc 24056 coe1termlem 24059 coe1term 24060 dgr0 24063 dgrmulc 24072 dgrcolem2 24075 vieta1lem2 24111 iaa 24125 aareccl 24126 aalioulem3 24134 taylthlem2 24173 psercn 24225 pserdvlem2 24227 abelthlem2 24231 abelthlem3 24232 abelthlem5 24234 abelthlem7 24237 abelth 24240 sin2kpi 24280 cos2kpi 24281 sinkpi 24316 efopn 24449 logtayl 24451 cxpval 24455 0cxp 24457 cxpexp 24459 cxpcl 24465 cxpge0 24474 mulcxplem 24475 mulcxp 24476 cxpmul2 24480 dvsqrt 24528 dvcnsqrt 24530 cxpcn3 24534 abscxpbnd 24539 efrlim 24741 ftalem2 24845 ftalem3 24846 ftalem4 24847 ftalem5 24848 ftalem7 24850 prmorcht 24949 muinv 24964 1sgm2ppw 24970 logfacbnd3 24993 logexprlim 24995 dchrelbas2 25007 dchrmulid2 25022 dchrfi 25025 dchrinv 25031 lgsdir2 25100 lgsdir 25102 dchrvmasumiflem1 25235 dchrvmasumiflem2 25236 rpvmasum2 25246 log2sumbnd 25278 selberg2lem 25284 logdivbnd 25290 ax5seglem8 25861 axlowdimlem6 25872 axlowdimlem13 25879 ex-co 27425 avril1 27449 vc0 27557 vcz 27558 cnaddabloOLD 27564 cnidOLD 27565 ipasslem8 27820 siilem2 27835 hvmul0 28009 hi01 28081 norm-iii 28125 h1de2ctlem 28542 pjmuli 28676 pjneli 28710 eigre 28822 eigorth 28825 elnlfn 28915 0cnfn 28967 0lnfn 28972 lnopunilem2 28998 xrge0tsmsd 29913 qqh0 30156 qqhcn 30163 eulerpartlemgs2 30570 sgnneg 30730 breprexpnat 30840 hgt750lem2 30858 subfacp1lem6 31293 sinccvglem 31692 abs2sqle 31700 abs2sqlt 31701 tan2h 33531 poimirlem16 33555 poimirlem19 33558 poimirlem31 33570 mblfinlem2 33577 ovoliunnfl 33581 voliunnfl 33583 dvtanlem 33589 ftc1anclem5 33619 cntotbnd 33725 flcidc 38061 dvconstbi 38850 expgrowth 38851 dvradcnv2 38863 binomcxplemdvbinom 38869 binomcxplemnotnn0 38872 xralrple3 39903 negcncfg 40412 ioodvbdlimc1 40466 ioodvbdlimc2 40468 itgsinexplem1 40487 stoweidlem26 40561 stoweidlem36 40571 stoweidlem55 40590 stirlinglem8 40616 fourierdlem103 40744 sqwvfoura 40763 sqwvfourb 40764 ovn0lem 41100 nn0sumshdiglemA 42738 nn0sumshdiglemB 42739 nn0sumshdiglem1 42740 sec0 42829 |
Copyright terms: Public domain | W3C validator |