Theorem renegcl 11599

Description: Closure law for negative of reals. The weak deduction theorem dedth 4606 is used to convert hypothesis of the inference (deduction) form of this theorem, renegcli 11597, to an antecedent. (Contributed by NM, 20-Jan-1997.) (Proof modification is discouraged.)

Assertion

Ref	Expression
renegcl	⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)

Proof of Theorem renegcl

Step	Hyp	Ref	Expression
1		negeq 11528	. . 3 ⊢ (𝐴 = if(𝐴 ∈ ℝ, 𝐴, 1) → -𝐴 = -if(𝐴 ∈ ℝ, 𝐴, 1))
2	1	eleq1d 2829	. 2 ⊢ (𝐴 = if(𝐴 ∈ ℝ, 𝐴, 1) → (-𝐴 ∈ ℝ ↔ -if(𝐴 ∈ ℝ, 𝐴, 1) ∈ ℝ))
3		1re 11290	. . . 4 ⊢ 1 ∈ ℝ
4	3	elimel 4617	. . 3 ⊢ if(𝐴 ∈ ℝ, 𝐴, 1) ∈ ℝ
5	4	renegcli 11597	. 2 ⊢ -if(𝐴 ∈ ℝ, 𝐴, 1) ∈ ℝ
6	2, 5	dedth 4606	1 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ifcif 4548  ℝcr 11183  1c1 11185  -cneg 11521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-ltxr 11329  df-sub 11522  df-neg 11523

This theorem is referenced by:  resubcl  11600  negreb  11601  renegcld  11717  negn0  11719  negf1o  11720  ltnegcon1  11791  ltnegcon2  11792  lenegcon1  11794  lenegcon2  11795  mullt0  11809  mulge0b  12165  mulle0b  12166  negfi  12244  infm3lem  12253  infm3  12254  riotaneg  12274  elnnz  12649  btwnz  12746  ublbneg  12998  supminf  13000  uzwo3  13008  zmax  13010  rebtwnz  13012  rpneg  13089  negelrp  13090  max0sub  13258  xnegcl  13275  xnegneg  13276  xltnegi  13278  rexsub  13295  xnegid  13300  xnegdi  13310  xpncan  13313  xnpcan  13314  xadddi  13357  iooneg  13531  iccneg  13532  icoshftf1o  13534  dfceil2  13890  ceicl  13892  ceige  13895  ceim1l  13898  negmod0  13929  negmod  13967  addmodlteq  13997  crim  15164  cnpart  15289  sqrtneglem  15315  absnid  15347  max0add  15359  absdiflt  15366  absdifle  15367  sqreulem  15408  resinhcl  16204  rpcoshcl  16205  tanhlt1  16208  tanhbnd  16209  remulg  21648  resubdrg  21649  cnheiborlem  25005  evth2  25011  ismbf3d  25708  mbfinf  25719  itgconst  25874  reeff1o  26509  atanbnd  26987  sgnneg  34505  ltflcei  37568  cos2h  37571  iblabsnclem  37643  ftc1anclem1  37653  areacirclem2  37669  areacirclem3  37670  areacirc  37673  mulltgt0  44922  rexabslelem  45333  xnegrecl  45353  supminfrnmpt  45360  supminfxr  45379  limsupre  45562  climinf3  45637  liminfreuzlem  45723  stoweidlem10  45931  etransclem46  46201  smfinflem  46738  finfdm  46767  line2  48486