MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  recld Structured version   Visualization version   GIF version

Theorem recld 13871
Description: The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
Hypothesis
Ref Expression
recld.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
recld (𝜑 → (ℜ‘𝐴) ∈ ℝ)

Proof of Theorem recld
StepHypRef Expression
1 recld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 recl 13787 . 2 (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
31, 2syl 17 1 (𝜑 → (ℜ‘𝐴) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  cfv 5849  cc 9881  cr 9882  cre 13774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-br 4616  df-opab 4676  df-mpt 4677  df-id 4991  df-po 4997  df-so 4998  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-er 7690  df-en 7903  df-dom 7904  df-sdom 7905  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-div 10632  df-2 11026  df-cj 13776  df-re 13777
This theorem is referenced by:  abstri  14007  sqreulem  14036  eqsqrt2d  14045  rlimrege0  14247  recoscl  14799  cos01bnd  14844  cnsubrg  19728  mbfeqa  23323  mbfss  23326  mbfmulc2re  23328  mbfadd  23341  mbfmulc2  23343  mbflim  23348  mbfmul  23406  iblcn  23478  itgcnval  23479  itgre  23480  itgim  23481  iblneg  23482  itgneg  23483  iblss  23484  itgeqa  23493  iblconst  23497  ibladd  23500  itgadd  23504  iblabs  23508  iblabsr  23509  iblmulc2  23510  itgmulc2  23513  itgabs  23514  itgsplit  23515  dvlip  23667  tanregt0  24196  efif1olem4  24202  eff1olem  24205  lognegb  24247  relog  24254  efiarg  24264  cosarg0d  24266  argregt0  24267  argrege0  24268  abslogle  24275  logcnlem4  24298  cxpsqrtlem  24355  cxpcn3lem  24395  abscxpbnd  24401  cosangneg2d  24444  angrtmuld  24445  lawcoslem1  24452  isosctrlem1  24455  asinlem3a  24504  asinlem3  24505  asinneg  24520  asinsinlem  24525  asinsin  24526  acosbnd  24534  atanlogaddlem  24547  atanlogadd  24548  atanlogsublem  24549  atanlogsub  24550  atantan  24557  o1cxp  24608  cxploglim2  24612  zetacvg  24648  lgamgulmlem2  24663  sqsscirc2  29749  ibladdnc  33120  itgaddnc  33123  iblabsnc  33127  iblmulc2nc  33128  itgmulc2nc  33131  itgabsnc  33132  bddiblnc  33133  ftc1anclem2  33139  ftc1anclem5  33142  ftc1anclem6  33143  ftc1anclem8  33145  cntotbnd  33248  isosctrlem1ALT  38674  iblsplit  39505
  Copyright terms: Public domain W3C validator