| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > renegcld | GIF version | ||
| Description: Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
| Ref | Expression |
|---|---|
| renegcld.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
| Ref | Expression |
|---|---|
| renegcld | ⊢ (𝜑 → -𝐴 ∈ ℝ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | renegcld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
| 2 | renegcl 8440 | . 2 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ) | |
| 3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → -𝐴 ∈ ℝ) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∈ wcel 2202 ℝcr 8031 -cneg 8351 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-14 2205 ax-ext 2213 ax-sep 4207 ax-pow 4264 ax-pr 4299 ax-setind 4635 ax-resscn 8124 ax-1cn 8125 ax-icn 8127 ax-addcl 8128 ax-addrcl 8129 ax-mulcl 8130 ax-addcom 8132 ax-addass 8134 ax-distr 8136 ax-i2m1 8137 ax-0id 8140 ax-rnegex 8141 ax-cnre 8143 |
| This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-ral 2515 df-rex 2516 df-reu 2517 df-rab 2519 df-v 2804 df-sbc 3032 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-br 4089 df-opab 4151 df-id 4390 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-iota 5286 df-fun 5328 df-fv 5334 df-riota 5971 df-ov 6021 df-oprab 6022 df-mpo 6023 df-sub 8352 df-neg 8353 |
| This theorem is referenced by: eqord2 8664 possumd 8749 reapmul1 8775 reapneg 8777 apneg 8791 mulext1 8792 recgt0 9030 prodgt0 9032 prodge0 9034 negiso 9135 nnnegz 9482 peano2z 9515 nn0negleid 9548 difgtsumgt 9549 supinfneg 9829 infsupneg 9830 infssuzex 10494 zsupssdc 10499 monoord2 10749 recj 11429 reneg 11430 imcj 11437 imneg 11438 cjap 11468 resqrexlemcalc3 11578 resqrexlemgt0 11582 abslt 11650 absle 11651 minmax 11792 mincl 11793 lemininf 11796 ltmininf 11797 bdtri 11802 xrmaxaddlem 11822 xrminrpcl 11836 climge0 11887 cos12dec 12331 absefib 12334 efieq1re 12335 dvdslelemd 12406 bitscmp 12521 bitsinv1lem 12524 4sqexercise2 12974 4sqlemsdc 12975 mulgnegnn 13721 ivthdec 15371 coseq0negpitopi 15563 cosq34lt1 15577 rpabscxpbnd 15667 lgsneg 15756 lgsdilem 15759 lgseisenlem1 15802 |
| Copyright terms: Public domain | W3C validator |