![]() |
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 11430. (Contributed by NM, 19-Feb-2005.) |
Ref | Expression |
---|---|
0cn | ⊢ 0 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-i2m1 11160 | . 2 ⊢ ((i · i) + 1) = 0 | |
2 | ax-icn 11151 | . . . 4 ⊢ i ∈ ℂ | |
3 | mulcl 11176 | . . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ) | |
4 | 2, 2, 3 | mp2an 690 | . . 3 ⊢ (i · i) ∈ ℂ |
5 | ax-1cn 11150 | . . 3 ⊢ 1 ∈ ℂ | |
6 | addcl 11174 | . . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ) | |
7 | 4, 5, 6 | mp2an 690 | . 2 ⊢ ((i · i) + 1) ∈ ℂ |
8 | 1, 7 | eqeltrri 2829 | 1 ⊢ 0 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 (class class class)co 7393 ℂcc 11090 0cc0 11092 1c1 11093 ici 11094 + caddc 11095 · cmul 11097 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 ax-1cn 11150 ax-icn 11151 ax-addcl 11152 ax-mulcl 11154 ax-i2m1 11160 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2723 df-clel 2809 |
This theorem is referenced by: 0cnd 11189 c0ex 11190 1re 11196 00id 11371 mul02lem1 11372 mul02 11374 mul01 11375 addrid 11376 addlid 11379 negcl 11442 subid 11461 subid1 11462 neg0 11488 negid 11489 negsub 11490 subneg 11491 negneg 11492 negeq0 11496 negsubdi 11498 renegcli 11503 mulneg1 11632 msqge0 11717 ixi 11825 muleqadd 11840 div0 11884 ofsubge0 12193 0m0e0 12314 nn0sscn 12459 elznn0 12555 ser0 14002 0exp0e1 14014 0exp 14045 sq0 14138 sqeqor 14162 binom2 14163 bcval5 14260 s1co 14766 shftval3 15005 shftidt2 15010 cjne0 15092 sqrt0 15170 abs0 15214 abs00bd 15220 abs2dif 15261 clim0 15432 climz 15475 serclim0 15503 rlimneg 15575 sumrblem 15639 fsumcvg 15640 summolem2a 15643 sumss 15652 fsumss 15653 fsumcvg2 15655 fsumsplit 15669 sumsplit 15696 fsumrelem 15735 fsumrlim 15739 fsumo1 15740 0fallfac 15963 0risefac 15964 binomfallfac 15967 fsumcube 15986 ef0 16016 eftlub 16034 sin0 16074 tan0 16076 divalglem9 16326 sadadd2lem2 16373 sadadd3 16384 bezout 16467 pcmpt2 16808 4sqlem11 16870 ramcl 16944 4001lem2 17057 odadd1 19676 cnaddablx 19696 cnaddabl 19697 cnaddid 19698 frgpnabllem1 19701 cncrng 20900 cnfld0 20903 cnbl0 24219 cnblcld 24220 cnfldnm 24224 xrge0gsumle 24278 xrge0tsms 24279 cnheibor 24400 cnlmod 24585 csscld 24695 clsocv 24696 cnflduss 24802 cnfldcusp 24803 rrxmvallem 24850 rrxmval 24851 mbfss 25092 mbfmulc2lem 25093 0plef 25118 0pledm 25119 itg1ge0 25132 itg1addlem4 25145 itg1addlem4OLD 25146 itg2splitlem 25195 itg2addlem 25205 ibl0 25233 iblcnlem 25235 iblss2 25252 itgss3 25261 dvconst 25363 dvcnp2 25366 dvrec 25401 dvexp3 25424 dveflem 25425 dv11cn 25447 lhop1lem 25459 plyun0 25640 plyeq0lem 25653 coeeulem 25667 coeeu 25668 coef3 25675 dgrle 25686 0dgrb 25689 coefv0 25691 coemulc 25698 coe1termlem 25701 coe1term 25702 dgr0 25705 dgrmulc 25714 dgrcolem2 25717 vieta1lem2 25753 iaa 25767 aareccl 25768 aalioulem3 25776 taylthlem2 25815 psercn 25867 pserdvlem2 25869 abelthlem2 25873 abelthlem3 25874 abelthlem5 25876 abelthlem7 25879 abelth 25882 sin2kpi 25922 cos2kpi 25923 sinkpi 25960 efopn 26095 logtayl 26097 cxpval 26101 0cxp 26103 cxpexp 26105 cxpcl 26111 cxpge0 26120 mulcxplem 26121 mulcxp 26122 cxpmul2 26126 dvsqrt 26177 dvcnsqrt 26179 cxpcn3 26183 abscxpbnd 26188 efrlim 26401 ftalem2 26505 ftalem3 26506 ftalem4 26507 ftalem5 26508 ftalem7 26510 prmorcht 26609 muinv 26624 1sgm2ppw 26630 logfacbnd3 26653 logexprlim 26655 dchrelbas2 26667 dchrmullid 26682 dchrfi 26685 dchrinv 26691 lgsdir2 26760 lgsdir 26762 addsqnreup 26873 dchrvmasumiflem1 26931 dchrvmasumiflem2 26932 rpvmasum2 26942 log2sumbnd 26974 selberg2lem 26980 logdivbnd 26986 ax5seglem8 28059 axlowdimlem6 28070 axlowdimlem13 28077 ex-co 29556 avril1 29581 vc0 29690 vcz 29691 cnaddabloOLD 29697 cnidOLD 29698 ipasslem8 29953 siilem2 29968 hvmul0 30140 hi01 30212 norm-iii 30256 h1de2ctlem 30671 pjmuli 30805 pjneli 30839 eigre 30951 eigorth 30954 elnlfn 31044 0cnfn 31096 0lnfn 31101 lnopunilem2 31127 xrge0tsmsd 32080 qqh0 32793 qqhcn 32800 eulerpartlemgs2 33208 sgnneg 33368 breprexpnat 33475 hgt750lem2 33493 subfacp1lem6 34005 sinccvglem 34486 abs2sqle 34494 abs2sqlt 34495 tan2h 36282 poimirlem16 36306 poimirlem19 36309 poimirlem31 36321 mblfinlem2 36328 ovoliunnfl 36332 voliunnfl 36334 dvtanlem 36339 ftc1anclem5 36367 cntotbnd 36467 60lcm7e420 40678 lcmineqlem10 40706 3lexlogpow5ineq1 40722 sn-1ne2 40965 sn-it0e0 41068 addinvcom 41084 sn-0tie0 41092 fltnltalem 41184 flcidc 41685 dvconstbi 42862 expgrowth 42863 dvradcnv2 42875 binomcxplemdvbinom 42881 binomcxplemnotnn0 42884 xralrple3 43855 negcncfg 44368 ioodvbdlimc1 44420 ioodvbdlimc2 44422 itgsinexplem1 44441 stoweidlem26 44513 stoweidlem36 44523 stoweidlem55 44542 stirlinglem8 44568 fourierdlem103 44696 sqwvfoura 44715 sqwvfourb 44716 ovn0lem 45052 nn0sumshdiglemA 46951 nn0sumshdiglemB 46952 nn0sumshdiglem1 46953 sec0 47451 |
Copyright terms: Public domain | W3C validator |