Theorem imcld 15285

Description: The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)

Hypothesis

Ref	Expression
recld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
imcld	⊢ (𝜑 → (ℑ‘𝐴) ∈ ℝ)

Proof of Theorem imcld

Step	Hyp	Ref	Expression
1		recld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		imcl 15201	. 2 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ)
3	1, 2	syl 18	1 ⊢ (𝜑 → (ℑ‘𝐴) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6533  ℂcc 11125  ℝcr 11126  ℑcim 15188

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-div 11899  df-nn 12261  df-2 12330  df-cj 15189  df-re 15190  df-im 15191

This theorem is used by:  rlimrecl  15670  resincl  16231  sin01bnd  16276  recld2  25044  mbfeqa  25874  mbfss  25877  mbfmulc2re  25879  mbfadd  25892  mbfmulc2  25894  mbflim  25899  mbfmul  25957  iblcn  26029  itgcnval  26030  itgre  26031  itgim  26032  iblneg  26033  itgneg  26034  ibladd  26051  itgadd  26055  iblabs  26059  itgmulc2  26064  bddiblnc  26072  aaliou2b  26580  efif1olem3  26784  eff1olem  26788  logimclad  26812  abslogimle  26813  logrnaddcl  26814  lognegb  26830  logcj  26846  efiarg  26847  cosargd  26848  argregt0  26850  argrege0  26851  argimgt0  26852  argimlt0  26853  logimul  26854  abslogle  26858  tanarg  26859  logcnlem2  26883  logcnlem3  26884  logcnlem4  26885  logcnlem5  26886  logcn  26887  dvloglem  26888  logf1o2  26890  efopnlem1  26896  efopnlem2  26897  cxpsqrtlem  26942  abscxpbnd  26993  ang180lem2  27050  lawcos  27056  isosctrlem1  27058  isosctrlem2  27059  asinneg  27126  asinsinlem  27131  atanlogaddlem  27153  atanlogsublem  27155  atanlogsub  27156  basellem3  27322  re0cj  33217  constrconj  34258  constrimcl  34283  constrmulcl  34284  sqsscirc2  34422  ibladdnc  38429  itgaddnc  38432  iblabsnc  38436  iblmulc2nc  38437  itgmulc2nc  38440  ftc1anclem2  38446  ftc1anclem6  38450  ftc1anclem8  38452  cntotbnd  38549  isosctrlem1ALT  45759  dstregt0  46118  absimnre  46307  absimlere  46310  cnrefiisplem  46660  sigarim  47682  readdcnnred  48194  resubcnnred  48195  cndivrenred  48197