![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imcl | Structured version Visualization version GIF version |
Description: The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
Ref | Expression |
---|---|
imcl | ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imre 14055 | . 2 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) = (ℜ‘(-i · 𝐴))) | |
2 | negicn 10483 | . . . 4 ⊢ -i ∈ ℂ | |
3 | mulcl 10221 | . . . 4 ⊢ ((-i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (-i · 𝐴) ∈ ℂ) | |
4 | 2, 3 | mpan 662 | . . 3 ⊢ (𝐴 ∈ ℂ → (-i · 𝐴) ∈ ℂ) |
5 | recl 14057 | . . 3 ⊢ ((-i · 𝐴) ∈ ℂ → (ℜ‘(-i · 𝐴)) ∈ ℝ) | |
6 | 4, 5 | syl 17 | . 2 ⊢ (𝐴 ∈ ℂ → (ℜ‘(-i · 𝐴)) ∈ ℝ) |
7 | 1, 6 | eqeltrd 2849 | 1 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2144 ‘cfv 6031 (class class class)co 6792 ℂcc 10135 ℝcr 10136 ici 10139 · cmul 10142 -cneg 10468 ℜcre 14044 ℑcim 14045 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-8 2146 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 ax-sep 4912 ax-nul 4920 ax-pow 4971 ax-pr 5034 ax-un 7095 ax-resscn 10194 ax-1cn 10195 ax-icn 10196 ax-addcl 10197 ax-addrcl 10198 ax-mulcl 10199 ax-mulrcl 10200 ax-mulcom 10201 ax-addass 10202 ax-mulass 10203 ax-distr 10204 ax-i2m1 10205 ax-1ne0 10206 ax-1rid 10207 ax-rnegex 10208 ax-rrecex 10209 ax-cnre 10210 ax-pre-lttri 10211 ax-pre-lttrn 10212 ax-pre-ltadd 10213 ax-pre-mulgt0 10214 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-3or 1071 df-3an 1072 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-eu 2621 df-mo 2622 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-ne 2943 df-nel 3046 df-ral 3065 df-rex 3066 df-reu 3067 df-rmo 3068 df-rab 3069 df-v 3351 df-sbc 3586 df-csb 3681 df-dif 3724 df-un 3726 df-in 3728 df-ss 3735 df-nul 4062 df-if 4224 df-pw 4297 df-sn 4315 df-pr 4317 df-op 4321 df-uni 4573 df-br 4785 df-opab 4845 df-mpt 4862 df-id 5157 df-po 5170 df-so 5171 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-iota 5994 df-fun 6033 df-fn 6034 df-f 6035 df-f1 6036 df-fo 6037 df-f1o 6038 df-fv 6039 df-riota 6753 df-ov 6795 df-oprab 6796 df-mpt2 6797 df-er 7895 df-en 8109 df-dom 8110 df-sdom 8111 df-pnf 10277 df-mnf 10278 df-xr 10279 df-ltxr 10280 df-le 10281 df-sub 10469 df-neg 10470 df-div 10886 df-2 11280 df-cj 14046 df-re 14047 df-im 14048 |
This theorem is referenced by: imf 14060 remim 14064 mulre 14068 cjreb 14070 recj 14071 reneg 14072 readd 14073 remullem 14075 remul2 14077 imcj 14079 imneg 14080 imadd 14081 imsub 14082 immul2 14084 imdiv 14085 cjcj 14087 cjadd 14088 ipcnval 14090 cjmulval 14092 cjmulge0 14093 cjneg 14094 imval2 14098 cnrecnv 14112 imcli 14115 imcld 14142 absrele 14255 efeul 15097 absef 15132 absefib 15133 efieq1re 15134 cnsubrg 20020 mbfconst 23620 itgconst 23804 tanregt0 24505 ellogrn 24526 argimgt0 24578 argimlt0 24579 logneg2 24581 tanarg 24585 logf1o2 24616 logreclem 24720 asinlem3a 24817 asinlem3 24818 zetacvg 24961 sigarls 41560 |
Copyright terms: Public domain | W3C validator |