Theorem renegcl 11492

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ifcif 4491  ℝcr 11074  1c1 11076  -cneg 11413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220  df-sub 11414  df-neg 11415

This theorem is referenced by:  resubcl  11493  negreb  11494  renegcld  11612  negn0  11614  negf1o  11615  ltnegcon1  11686  ltnegcon2  11687  lenegcon1  11689  lenegcon2  11690  mullt0  11704  mulge0b  12060  mulle0b  12061  negfi  12139  infm3lem  12148  infm3  12149  riotaneg  12169  elnnz  12546  btwnz  12644  ublbneg  12899  supminf  12901  uzwo3  12909  zmax  12911  rebtwnz  12913  rpneg  12992  negelrp  12993  max0sub  13163  xnegcl  13180  xnegneg  13181  xltnegi  13183  rexsub  13200  xnegid  13205  xnegdi  13215  xpncan  13218  xnpcan  13219  xadddi  13262  iooneg  13439  iccneg  13440  icoshftf1o  13442  dfceil2  13808  ceicl  13810  ceige  13813  ceim1l  13816  negmod0  13847  modaddb  13878  negmod  13888  addmodlteq  13918  crim  15088  cnpart  15213  sqrtneglem  15239  absnid  15271  max0add  15283  absdiflt  15291  absdifle  15292  sqreulem  15333  resinhcl  16131  rpcoshcl  16132  tanhlt1  16135  tanhbnd  16136  remulg  21523  resubdrg  21524  cnheiborlem  24860  evth2  24866  ismbf3d  25562  mbfinf  25573  itgconst  25727  reeff1o  26364  atanbnd  26843  sgnneg  32765  ltflcei  37609  cos2h  37612  iblabsnclem  37684  ftc1anclem1  37694  areacirclem2  37710  areacirclem3  37711  areacirc  37714  mulltgt0  45023  rexabslelem  45421  xnegrecl  45441  supminfrnmpt  45448  supminfxr  45467  limsupre  45646  climinf3  45721  liminfreuzlem  45807  stoweidlem10  46015  etransclem46  46285  smfinflem  46822  finfdm  46851  ceilbi  47338  ceildivmod  47344  line2  48745