Theorem renegcl 11516

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ifcif 4487  ℝcr 11094  1c1 11096  -cneg 11437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-ltxr 11243  df-sub 11438  df-neg 11439

This theorem is referenced by:  resubcl  11517  negreb  11518  renegcld  11636  negn0  11638  negf1o  11639  ltnegcon1  11710  ltnegcon2  11711  lenegcon1  11713  lenegcon2  11714  mullt0  11728  mulge0b  12080  mulle0b  12081  negfi  12159  infm3lem  12168  infm3  12169  riotaneg  12189  elnnz  12596  btwnz  12694  ublbneg  12952  supminf  12954  uzwo3  12962  zmax  12964  rebtwnz  12966  rpneg  13045  negelrp  13046  max0sub  13217  xnegcl  13234  xnegneg  13235  xltnegi  13237  rexsub  13254  xnegid  13259  xnegdi  13269  xpncan  13272  xnpcan  13273  xadddi  13316  iooneg  13493  iccneg  13494  icoshftf1o  13496  dfceil2  13868  ceicl  13870  ceige  13873  ceim1l  13876  negmod0  13907  modaddb  13938  negmod  13948  addmodlteq  13978  sgnneg  15133  crim  15162  cnpart  15287  sqrtneglem  15313  absnid  15345  max0add  15357  absdiflt  15365  absdifle  15366  sqreulem  15407  resinhcl  16207  rpcoshcl  16208  tanhlt1  16211  tanhbnd  16212  remulg  21757  resubdrg  21758  cnheiborlem  25113  evth2  25119  ismbf3d  25813  mbfinf  25824  itgconst  25978  reeff1o  26610  atanbnd  27091  ltflcei  38259  cos2h  38262  iblabsnclem  38334  ftc1anclem1  38344  areacirclem2  38360  areacirclem3  38361  areacirc  38364  mulltgt0  45742  rexabslelem  46132  xnegrecl  46152  supminfrnmpt  46159  supminfxr  46178  limsupre  46355  climinf3  46430  liminfreuzlem  46516  stoweidlem10  46724  etransclem46  46994  smfinflem  47531  finfdm  47560  ceilbi  48074  ceildivmod  48082  line2  49532