| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ltsubaddd | Structured version Visualization version GIF version | ||
| Description: 'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.) |
| Ref | Expression |
|---|---|
| leidd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
| ltnegd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
| ltadd1d.3 | ⊢ (𝜑 → 𝐶 ∈ ℝ) |
| Ref | Expression |
|---|---|
| ltsubaddd | ⊢ (𝜑 → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | leidd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
| 2 | ltnegd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
| 3 | ltadd1d.3 | . 2 ⊢ (𝜑 → 𝐶 ∈ ℝ) | |
| 4 | ltsubadd 11612 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵))) | |
| 5 | 1, 2, 3, 4 | syl3anc 1379 | 1 ⊢ (𝜑 → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 207 ∈ wcel 2119 class class class wbr 5073 (class class class)co 7357 ℝcr 11029 + caddc 11033 < clt 11171 − cmin 11369 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-sep 5219 ax-nul 5229 ax-pow 5295 ax-pr 5363 ax-un 7679 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 |
| This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4263 df-if 4456 df-pw 4532 df-sn 4557 df-pr 4559 df-op 4563 df-uni 4840 df-br 5074 df-opab 5136 df-mpt 5155 df-id 5514 df-po 5527 df-so 5528 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7314 df-ov 7360 df-oprab 7361 df-mpo 7362 df-er 8634 df-en 8885 df-dom 8886 df-sdom 8887 df-pnf 11173 df-mnf 11174 df-ltxr 11176 df-sub 11371 df-neg 11372 |
| This theorem is referenced by: sublt0d 11768 ltaddsublt 11769 supaddc 12115 suprzcl 12601 2submod 13886 hashdvds 16737 prmreclem6 16884 4sqlem6 16906 ovolshftlem1 25495 opnmbllem 25587 mbfaddlem 25646 itg2monolem1 25736 dvlt0 25991 lhop1 26000 plydivlem3 26280 efif1olem1 26525 ang180lem2 26793 atanlogsublem 26898 bposlem1 27266 crctcshwlkn0lem5 29901 eucrctshift 30332 bcm1n 32888 subfacval3 35426 opnmbllem0 38032 itg2addnclem 38047 itg2gt0cn 38051 aks4d1p1p3 42563 aks4d1p1 42570 posbezout 42594 iooiinicc 45995 0ellimcdiv 46100 wallispilem3 46518 fourierdlem41 46599 fourierdlem49 46606 fourierdlem97 46654 elaa2lem 46684 sge0ltfirp 46851 ceilbi 47808 sfprmdvdsmersenne 48089 proththdlem 48099 ltsubaddb 49013 ltsubsubb 49014 ltsubadd2b 49015 |
| Copyright terms: Public domain | W3C validator |