Theorem renegcld 7921

Description: Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
renegcld.1	|- ( ph -> A e. RR )

Assertion

Ref	Expression
renegcld	|- ( ph -> -u A e. RR )

Proof of Theorem renegcld

Step	Hyp	Ref	Expression
1		renegcld.1	. 2 |- ( ph -> A e. RR )
2		renegcl 7806	. 2 |- ( A e. RR -> -u A e. RR )
3	1, 2	syl 14	1 |- ( ph -> -u A e. RR )

Syntax hints:   -> wi 4   e. wcel 1439   RRcr 7412   -ucneg 7717

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3965  ax-pow 4017  ax-pr 4047  ax-setind 4368  ax-resscn 7500  ax-1cn 7501  ax-icn 7503  ax-addcl 7504  ax-addrcl 7505  ax-mulcl 7506  ax-addcom 7508  ax-addass 7510  ax-distr 7512  ax-i2m1 7513  ax-0id 7516  ax-rnegex 7517  ax-cnre 7519

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-reu 2367  df-rab 2369  df-v 2624  df-sbc 2844  df-dif 3004  df-un 3006  df-in 3008  df-ss 3015  df-pw 3437  df-sn 3458  df-pr 3459  df-op 3461  df-uni 3662  df-br 3854  df-opab 3908  df-id 4131  df-xp 4460  df-rel 4461  df-cnv 4462  df-co 4463  df-dm 4464  df-iota 4995  df-fun 5032  df-fv 5038  df-riota 5624  df-ov 5671  df-oprab 5672  df-mpt2 5673  df-sub 7718  df-neg 7719

This theorem is referenced by:  eqord2  8025  possumd  8109  reapmul1  8135  reapneg  8137  apneg  8151  mulext1  8152  recgt0  8374  prodgt0  8376  prodge0  8378  negiso  8479  nnnegz  8816  peano2z  8849  supinfneg  9146  infsupneg  9147  monoord2  9968  recj  10364  reneg  10365  imcj  10372  imneg  10373  cjap  10403  resqrexlemcalc3  10512  resqrexlemgt0  10516  abslt  10584  absle  10585  minmax  10724  lemininf  10727  ltmininf  10728  climge0  10776  absefib  11123  efieq1re  11124  dvdslelemd  11185  infssuzex  11286