Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > abssubge0d | Structured version Visualization version GIF version |
Description: Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.) |
Ref | Expression |
---|---|
absltd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
absltd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
abssubge0d.2 | ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
Ref | Expression |
---|---|
abssubge0d | ⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | absltd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
2 | absltd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
3 | abssubge0d.2 | . 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵) | |
4 | abssubge0 14924 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴)) | |
5 | 1, 2, 3, 4 | syl3anc 1373 | 1 ⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ∈ wcel 2112 class class class wbr 5070 ‘cfv 6401 (class class class)co 7235 ℝcr 10758 ≤ cle 10898 − cmin 11092 abscabs 14830 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-sep 5209 ax-nul 5216 ax-pow 5275 ax-pr 5339 ax-un 7545 ax-cnex 10815 ax-resscn 10816 ax-1cn 10817 ax-icn 10818 ax-addcl 10819 ax-addrcl 10820 ax-mulcl 10821 ax-mulrcl 10822 ax-mulcom 10823 ax-addass 10824 ax-mulass 10825 ax-distr 10826 ax-i2m1 10827 ax-1ne0 10828 ax-1rid 10829 ax-rnegex 10830 ax-rrecex 10831 ax-cnre 10832 ax-pre-lttri 10833 ax-pre-lttrn 10834 ax-pre-ltadd 10835 ax-pre-mulgt0 10836 ax-pre-sup 10837 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3425 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4255 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5153 df-tr 5179 df-id 5472 df-eprel 5478 df-po 5486 df-so 5487 df-fr 5527 df-we 5529 df-xp 5575 df-rel 5576 df-cnv 5577 df-co 5578 df-dm 5579 df-rn 5580 df-res 5581 df-ima 5582 df-pred 6179 df-ord 6237 df-on 6238 df-lim 6239 df-suc 6240 df-iota 6359 df-fun 6403 df-fn 6404 df-f 6405 df-f1 6406 df-fo 6407 df-f1o 6408 df-fv 6409 df-riota 7192 df-ov 7238 df-oprab 7239 df-mpo 7240 df-om 7667 df-2nd 7784 df-wrecs 8071 df-recs 8132 df-rdg 8170 df-er 8415 df-en 8651 df-dom 8652 df-sdom 8653 df-sup 9088 df-pnf 10899 df-mnf 10900 df-xr 10901 df-ltxr 10902 df-le 10903 df-sub 11094 df-neg 11095 df-div 11520 df-nn 11861 df-2 11923 df-3 11924 df-n0 12121 df-z 12207 df-uz 12469 df-rp 12617 df-seq 13607 df-exp 13668 df-cj 14695 df-re 14696 df-im 14697 df-sqrt 14831 df-abs 14832 |
This theorem is referenced by: climsqz2 15236 rlimsqz2 15247 cvgcmp 15413 flo1 15451 blcvx 23727 ivthlem2 24381 volcn 24535 dvferm1lem 24913 dvlip 24922 lhop1 24943 ftc1a 24966 abelth2 25366 dvlog2lem 25572 chordthmlem4 25750 leibpi 25857 mudivsum 26443 pntrsumo1 26478 pntpbnd1 26499 pntibndlem2 26504 unbdqndv2lem2 34461 climinf 42868 lptre2pt 42902 dvbdfbdioolem1 43190 fourierdlem42 43411 ovolval3 43906 |
Copyright terms: Public domain | W3C validator |