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

Theorem recld 13052
Description: The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
Hypothesis
Ref Expression
recld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
recld  |-  ( ph  ->  ( Re `  A
)  e.  RR )

Proof of Theorem recld
StepHypRef Expression
1 recld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 recl 12968 . 2  |-  ( A  e.  CC  ->  (
Re `  A )  e.  RR )
31, 2syl 16 1  |-  ( ph  ->  ( Re `  A
)  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1836   ` cfv 5513   CCcc 9423   RRcr 9424   Recre 12955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513  ax-resscn 9482  ax-1cn 9483  ax-icn 9484  ax-addcl 9485  ax-addrcl 9486  ax-mulcl 9487  ax-mulrcl 9488  ax-mulcom 9489  ax-addass 9490  ax-mulass 9491  ax-distr 9492  ax-i2m1 9493  ax-1ne0 9494  ax-1rid 9495  ax-rnegex 9496  ax-rrecex 9497  ax-cnre 9498  ax-pre-lttri 9499  ax-pre-lttrn 9500  ax-pre-ltadd 9501  ax-pre-mulgt0 9502
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-nel 2594  df-ral 2751  df-rex 2752  df-reu 2753  df-rmo 2754  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-op 3968  df-uni 4181  df-br 4385  df-opab 4443  df-mpt 4444  df-id 4726  df-po 4731  df-so 4732  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-riota 6180  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-er 7251  df-en 7458  df-dom 7459  df-sdom 7460  df-pnf 9563  df-mnf 9564  df-xr 9565  df-ltxr 9566  df-le 9567  df-sub 9742  df-neg 9743  df-div 10146  df-2 10533  df-cj 12957  df-re 12958
This theorem is referenced by:  abstri  13188  sqreulem  13217  eqsqrt2d  13226  rlimrege0  13427  recoscl  13901  cos01bnd  13946  cnsubrg  18614  mbfeqa  22158  mbfss  22161  mbfmulc2re  22163  mbfadd  22176  mbfmulc2  22178  mbflim  22183  mbfmul  22241  iblcn  22313  itgcnval  22314  itgre  22315  itgim  22316  iblneg  22317  itgneg  22318  iblss  22319  itgeqa  22328  iblconst  22332  ibladd  22335  itgadd  22339  iblabs  22343  iblabsr  22344  iblmulc2  22345  itgmulc2  22348  itgabs  22349  itgsplit  22350  dvlip  22502  tanregt0  23034  efif1olem4  23040  eff1olem  23043  lognegb  23085  relog  23092  efiarg  23102  cosarg0d  23104  argregt0  23105  argrege0  23106  abslogle  23113  logcnlem4  23136  cxpsqrtlem  23193  cxpcn3lem  23231  abscxpbnd  23237  cosangneg2d  23280  angrtmuld  23281  lawcoslem1  23288  isosctrlem1  23291  asinlem3a  23340  asinlem3  23341  asinneg  23356  asinsinlem  23361  asinsin  23362  acosbnd  23370  atanlogaddlem  23383  atanlogadd  23384  atanlogsublem  23385  atanlogsub  23386  atantan  23393  o1cxp  23444  cxploglim2  23448  sqsscirc2  28080  zetacvg  28786  lgamgulmlem2  28801  ibladdnc  30278  itgaddnc  30281  iblabsnc  30285  iblmulc2nc  30286  itgmulc2nc  30289  itgabsnc  30290  bddiblnc  30291  ftc1anclem2  30297  ftc1anclem5  30300  ftc1anclem6  30301  ftc1anclem8  30303  cntotbnd  30498  iblsplit  31970  isosctrlem1ALT  34120
  Copyright terms: Public domain W3C validator