![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ltadd2dd | Structured version Visualization version GIF version |
Description: Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.) |
Ref | Expression |
---|---|
ltd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
ltd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
letrd.3 | ⊢ (𝜑 → 𝐶 ∈ ℝ) |
ltletrd.4 | ⊢ (𝜑 → 𝐴 < 𝐵) |
Ref | Expression |
---|---|
ltadd2dd | ⊢ (𝜑 → (𝐶 + 𝐴) < (𝐶 + 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltletrd.4 | . 2 ⊢ (𝜑 → 𝐴 < 𝐵) | |
2 | ltd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
3 | ltd.2 | . . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
4 | letrd.3 | . . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ) | |
5 | 2, 3, 4 | ltadd2d 10643 | . 2 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵))) |
6 | 1, 5 | mpbid 233 | 1 ⊢ (𝜑 → (𝐶 + 𝐴) < (𝐶 + 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2081 class class class wbr 4962 (class class class)co 7016 ℝcr 10382 + caddc 10386 < clt 10521 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 ax-resscn 10440 ax-addrcl 10444 ax-pre-lttri 10457 ax-pre-ltadd 10459 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-ov 7019 df-er 8139 df-en 8358 df-dom 8359 df-sdom 8360 df-pnf 10523 df-mnf 10524 df-ltxr 10526 |
This theorem is referenced by: zltaddlt1le 12740 2tnp1ge0ge0 13049 ccatrn 13787 eirrlem 15390 prmreclem5 16085 iccntr 23112 icccmplem2 23114 ivthlem2 23736 uniioombllem3 23869 opnmbllem 23885 dvcnvre 24299 cosordlem 24796 efif1olem2 24808 atanlogaddlem 25172 pntibndlem2 25849 pntlemr 25860 dya2icoseg 31152 opnmbllem0 34459 fltnltalem 38771 binomcxplemdvbinom 40223 zltlesub 41092 supxrge 41147 ltadd12dd 41152 xrralrecnnle 41194 0ellimcdiv 41472 climleltrp 41499 ioodvbdlimc1lem2 41758 stoweidlem11 41838 stoweidlem14 41841 stoweidlem26 41853 stoweidlem44 41871 dirkertrigeqlem3 41927 dirkercncflem1 41930 dirkercncflem2 41931 fourierdlem4 41938 fourierdlem10 41944 fourierdlem28 41962 fourierdlem40 41974 fourierdlem50 41983 fourierdlem57 41990 fourierdlem59 41992 fourierdlem60 41993 fourierdlem61 41994 fourierdlem68 42001 fourierdlem74 42007 fourierdlem75 42008 fourierdlem76 42009 fourierdlem78 42011 fourierdlem79 42012 fourierdlem84 42017 fourierdlem93 42026 fourierdlem111 42044 fouriersw 42058 smfaddlem1 42581 smflimlem3 42591 |
Copyright terms: Public domain | W3C validator |