![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imcld | Structured version Visualization version GIF version |
Description: The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
Ref | Expression |
---|---|
recld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Ref | Expression |
---|---|
imcld | ⊢ (𝜑 → (ℑ‘𝐴) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | imcl 14046 | . 2 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (ℑ‘𝐴) ∈ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2135 ‘cfv 6045 ℂcc 10122 ℝcr 10123 ℑcim 14033 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1867 ax-4 1882 ax-5 1984 ax-6 2050 ax-7 2086 ax-8 2137 ax-9 2144 ax-10 2164 ax-11 2179 ax-12 2192 ax-13 2387 ax-ext 2736 ax-sep 4929 ax-nul 4937 ax-pow 4988 ax-pr 5051 ax-un 7110 ax-resscn 10181 ax-1cn 10182 ax-icn 10183 ax-addcl 10184 ax-addrcl 10185 ax-mulcl 10186 ax-mulrcl 10187 ax-mulcom 10188 ax-addass 10189 ax-mulass 10190 ax-distr 10191 ax-i2m1 10192 ax-1ne0 10193 ax-1rid 10194 ax-rnegex 10195 ax-rrecex 10196 ax-cnre 10197 ax-pre-lttri 10198 ax-pre-lttrn 10199 ax-pre-ltadd 10200 ax-pre-mulgt0 10201 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1631 df-ex 1850 df-nf 1855 df-sb 2043 df-eu 2607 df-mo 2608 df-clab 2743 df-cleq 2749 df-clel 2752 df-nfc 2887 df-ne 2929 df-nel 3032 df-ral 3051 df-rex 3052 df-reu 3053 df-rmo 3054 df-rab 3055 df-v 3338 df-sbc 3573 df-csb 3671 df-dif 3714 df-un 3716 df-in 3718 df-ss 3725 df-nul 4055 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-op 4324 df-uni 4585 df-br 4801 df-opab 4861 df-mpt 4878 df-id 5170 df-po 5183 df-so 5184 df-xp 5268 df-rel 5269 df-cnv 5270 df-co 5271 df-dm 5272 df-rn 5273 df-res 5274 df-ima 5275 df-iota 6008 df-fun 6047 df-fn 6048 df-f 6049 df-f1 6050 df-fo 6051 df-f1o 6052 df-fv 6053 df-riota 6770 df-ov 6812 df-oprab 6813 df-mpt2 6814 df-er 7907 df-en 8118 df-dom 8119 df-sdom 8120 df-pnf 10264 df-mnf 10265 df-xr 10266 df-ltxr 10267 df-le 10268 df-sub 10456 df-neg 10457 df-div 10873 df-2 11267 df-cj 14034 df-re 14035 df-im 14036 |
This theorem is referenced by: rlimrecl 14506 resincl 15065 sin01bnd 15110 recld2 22814 mbfeqa 23605 mbfss 23608 mbfmulc2re 23610 mbfadd 23623 mbfmulc2 23625 mbflim 23630 mbfmul 23688 iblcn 23760 itgcnval 23761 itgre 23762 itgim 23763 iblneg 23764 itgneg 23765 ibladd 23782 itgadd 23786 iblabs 23790 itgmulc2 23795 aaliou2b 24291 efif1olem3 24485 eff1olem 24489 logimclad 24514 abslogimle 24515 logrnaddcl 24516 lognegb 24531 logcj 24547 efiarg 24548 cosargd 24549 argregt0 24551 argrege0 24552 argimgt0 24553 argimlt0 24554 logimul 24555 abslogle 24559 tanarg 24560 logcnlem2 24584 logcnlem3 24585 logcnlem4 24586 logcnlem5 24587 logcn 24588 dvloglem 24589 logf1o2 24591 efopnlem1 24597 efopnlem2 24598 cxpsqrtlem 24643 abscxpbnd 24689 ang180lem2 24735 lawcos 24741 isosctrlem1 24743 isosctrlem2 24744 asinneg 24808 asinsinlem 24813 atanlogaddlem 24835 atanlogsublem 24837 atanlogsub 24838 basellem3 25004 sqsscirc2 30260 ibladdnc 33776 itgaddnc 33779 iblabsnc 33783 iblmulc2nc 33784 itgmulc2nc 33787 bddiblnc 33789 ftc1anclem2 33795 ftc1anclem6 33799 ftc1anclem8 33801 cntotbnd 33904 isosctrlem1ALT 39665 dstregt0 39988 absimnre 40201 absimlere 40204 cnrefiisplem 40554 sigarim 41542 |
Copyright terms: Public domain | W3C validator |