Theorem renegcl 11451

Description: Closure law for negative of reals. The weak deduction theorem dedth 4526 is used to convert hypothesis of the inference (deduction) form of this theorem, renegcli 11449, 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 11379	. . 3 ⊢ (𝐴 = if(𝐴 ∈ ℝ, 𝐴, 1) → -𝐴 = -if(𝐴 ∈ ℝ, 𝐴, 1))
2	1	eleq1d 2822	. 2 ⊢ (𝐴 = if(𝐴 ∈ ℝ, 𝐴, 1) → (-𝐴 ∈ ℝ ↔ -if(𝐴 ∈ ℝ, 𝐴, 1) ∈ ℝ))
3		1re 11138	. . . 4 ⊢ 1 ∈ ℝ
4	3	elimel 4537	. . 3 ⊢ if(𝐴 ∈ ℝ, 𝐴, 1) ∈ ℝ
5	4	renegcli 11449	. 2 ⊢ -if(𝐴 ∈ ℝ, 𝐴, 1) ∈ ℝ
6	2, 5	dedth 4526	1 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ifcif 4467  ℝcr 11031  1c1 11033  -cneg 11372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-ltxr 11178  df-sub 11373  df-neg 11374

This theorem is referenced by:  resubcl  11452  negreb  11453  renegcld  11571  negn0  11573  negf1o  11574  ltnegcon1  11645  ltnegcon2  11646  lenegcon1  11648  lenegcon2  11649  mullt0  11663  mulge0b  12020  mulle0b  12021  negfi  12099  infm3lem  12108  infm3  12109  riotaneg  12129  elnnz  12528  btwnz  12626  ublbneg  12877  supminf  12879  uzwo3  12887  zmax  12889  rebtwnz  12891  rpneg  12970  negelrp  12971  max0sub  13142  xnegcl  13159  xnegneg  13160  xltnegi  13162  rexsub  13179  xnegid  13184  xnegdi  13194  xpncan  13197  xnpcan  13198  xadddi  13241  iooneg  13418  iccneg  13419  icoshftf1o  13421  dfceil2  13792  ceicl  13794  ceige  13797  ceim1l  13800  negmod0  13831  modaddb  13862  negmod  13872  addmodlteq  13902  crim  15071  cnpart  15196  sqrtneglem  15222  absnid  15254  max0add  15266  absdiflt  15274  absdifle  15275  sqreulem  15316  resinhcl  16117  rpcoshcl  16118  tanhlt1  16121  tanhbnd  16122  remulg  21600  resubdrg  21601  cnheiborlem  24934  evth2  24940  ismbf3d  25634  mbfinf  25645  itgconst  25799  reeff1o  26428  atanbnd  26906  sgnneg  32924  ltflcei  37946  cos2h  37949  iblabsnclem  38021  ftc1anclem1  38031  areacirclem2  38047  areacirclem3  38048  areacirc  38051  mulltgt0  45474  rexabslelem  45867  xnegrecl  45887  supminfrnmpt  45894  supminfxr  45913  limsupre  46090  climinf3  46165  liminfreuzlem  46251  stoweidlem10  46459  etransclem46  46729  smfinflem  47266  finfdm  47295  ceilbi  47800  ceildivmod  47808  line2  49243