![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > renegcl | Structured version Visualization version GIF version |
Description: Closure law for negative of reals. The weak deduction theorem dedth 4588 is used to convert hypothesis of the inference (deduction) form of this theorem, renegcli 11567, to an antecedent. (Contributed by NM, 20-Jan-1997.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
renegcl | ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negeq 11497 | . . 3 ⊢ (𝐴 = if(𝐴 ∈ ℝ, 𝐴, 1) → -𝐴 = -if(𝐴 ∈ ℝ, 𝐴, 1)) | |
2 | 1 | eleq1d 2823 | . 2 ⊢ (𝐴 = if(𝐴 ∈ ℝ, 𝐴, 1) → (-𝐴 ∈ ℝ ↔ -if(𝐴 ∈ ℝ, 𝐴, 1) ∈ ℝ)) |
3 | 1re 11258 | . . . 4 ⊢ 1 ∈ ℝ | |
4 | 3 | elimel 4599 | . . 3 ⊢ if(𝐴 ∈ ℝ, 𝐴, 1) ∈ ℝ |
5 | 4 | renegcli 11567 | . 2 ⊢ -if(𝐴 ∈ ℝ, 𝐴, 1) ∈ ℝ |
6 | 2, 5 | dedth 4588 | 1 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1536 ∈ wcel 2105 ifcif 4530 ℝcr 11151 1c1 11153 -cneg 11490 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 ax-resscn 11209 ax-1cn 11210 ax-icn 11211 ax-addcl 11212 ax-addrcl 11213 ax-mulcl 11214 ax-mulrcl 11215 ax-mulcom 11216 ax-addass 11217 ax-mulass 11218 ax-distr 11219 ax-i2m1 11220 ax-1ne0 11221 ax-1rid 11222 ax-rnegex 11223 ax-rrecex 11224 ax-cnre 11225 ax-pre-lttri 11226 ax-pre-lttrn 11227 ax-pre-ltadd 11228 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5582 df-po 5596 df-so 5597 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-er 8743 df-en 8984 df-dom 8985 df-sdom 8986 df-pnf 11294 df-mnf 11295 df-ltxr 11297 df-sub 11491 df-neg 11492 |
This theorem is referenced by: resubcl 11570 negreb 11571 renegcld 11687 negn0 11689 negf1o 11690 ltnegcon1 11761 ltnegcon2 11762 lenegcon1 11764 lenegcon2 11765 mullt0 11779 mulge0b 12135 mulle0b 12136 negfi 12214 infm3lem 12223 infm3 12224 riotaneg 12244 elnnz 12620 btwnz 12718 ublbneg 12972 supminf 12974 uzwo3 12982 zmax 12984 rebtwnz 12986 rpneg 13064 negelrp 13065 max0sub 13234 xnegcl 13251 xnegneg 13252 xltnegi 13254 rexsub 13271 xnegid 13276 xnegdi 13286 xpncan 13289 xnpcan 13290 xadddi 13333 iooneg 13507 iccneg 13508 icoshftf1o 13510 dfceil2 13875 ceicl 13877 ceige 13880 ceim1l 13883 negmod0 13914 negmod 13953 addmodlteq 13983 crim 15150 cnpart 15275 sqrtneglem 15301 absnid 15333 max0add 15345 absdiflt 15352 absdifle 15353 sqreulem 15394 resinhcl 16188 rpcoshcl 16189 tanhlt1 16192 tanhbnd 16193 remulg 21642 resubdrg 21643 cnheiborlem 24999 evth2 25005 ismbf3d 25702 mbfinf 25713 itgconst 25868 reeff1o 26505 atanbnd 26983 sgnneg 34521 ltflcei 37594 cos2h 37597 iblabsnclem 37669 ftc1anclem1 37679 areacirclem2 37695 areacirclem3 37696 areacirc 37699 mulltgt0 44959 rexabslelem 45367 xnegrecl 45387 supminfrnmpt 45394 supminfxr 45413 limsupre 45596 climinf3 45671 liminfreuzlem 45757 stoweidlem10 45965 etransclem46 46235 smfinflem 46772 finfdm 46801 ceildivmod 47278 line2 48601 |
Copyright terms: Public domain | W3C validator |