| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > subge0d | GIF version | ||
| Description: Nonnegative subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
| Ref | Expression |
|---|---|
| leidd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
| ltnegd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
| Ref | Expression |
|---|---|
| subge0d | ⊢ (𝜑 → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | leidd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
| 2 | ltnegd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
| 3 | subge0 8563 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴)) | |
| 4 | 1, 2, 3 | syl2anc 411 | 1 ⊢ (𝜑 → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ↔ wb 105 ∈ wcel 2177 class class class wbr 4050 (class class class)co 5956 ℝcr 7939 0cc0 7940 ≤ cle 8123 − cmin 8258 |
| 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 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4169 ax-pow 4225 ax-pr 4260 ax-un 4487 ax-setind 4592 ax-cnex 8031 ax-resscn 8032 ax-1cn 8033 ax-1re 8034 ax-icn 8035 ax-addcl 8036 ax-addrcl 8037 ax-mulcl 8038 ax-addcom 8040 ax-addass 8042 ax-distr 8044 ax-i2m1 8045 ax-0id 8048 ax-rnegex 8049 ax-cnre 8051 ax-pre-ltadd 8056 |
| This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rab 2494 df-v 2775 df-sbc 3003 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-pw 3622 df-sn 3643 df-pr 3644 df-op 3646 df-uni 3856 df-br 4051 df-opab 4113 df-id 4347 df-xp 4688 df-rel 4689 df-cnv 4690 df-co 4691 df-dm 4692 df-iota 5240 df-fun 5281 df-fv 5287 df-riota 5911 df-ov 5959 df-oprab 5960 df-mpo 5961 df-pnf 8124 df-mnf 8125 df-xr 8126 df-ltxr 8127 df-le 8128 df-sub 8260 df-neg 8261 |
| This theorem is referenced by: lemul1a 8946 uzsubsubfz 10184 qfracge0 10441 modqge0 10494 q2submod 10547 modqsubdir 10555 modsumfzodifsn 10558 uzennn 10598 ser3le 10699 bcval5 10925 resqrexlemglsq 11403 fzomaxdiflem 11493 amgm2 11499 climle 11715 fsumle 11844 cvgratnnlemabsle 11908 cvgratnnlemsumlt 11909 uzwodc 12428 pcz 12725 4sqlem15 12798 dich0 15194 gausslemma2dlem0h 15603 lgseisenlem1 15617 |
| Copyright terms: Public domain | W3C validator |