![]() |
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 11402 | . 2 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵))) |
6 | 1, 5 | mpbid 231 | 1 ⊢ (𝜑 → (𝐶 + 𝐴) < (𝐶 + 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 class class class wbr 5149 (class class class)co 7419 ℝcr 11139 + caddc 11143 < clt 11280 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7741 ax-resscn 11197 ax-addrcl 11201 ax-pre-lttri 11214 ax-pre-ltadd 11216 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-nel 3036 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fo 6555 df-f1o 6556 df-fv 6557 df-ov 7422 df-er 8725 df-en 8965 df-dom 8966 df-sdom 8967 df-pnf 11282 df-mnf 11283 df-ltxr 11285 |
This theorem is referenced by: zltaddlt1le 13517 2tnp1ge0ge0 13830 ccatrn 14575 eirrlem 16184 prmreclem5 16892 iccntr 24781 icccmplem2 24783 ivthlem2 25425 uniioombllem3 25558 opnmbllem 25574 dvcnvre 25996 cosordlem 26509 efif1olem2 26522 atanlogaddlem 26890 pntibndlem2 27569 pntlemr 27580 dya2icoseg 34025 opnmbllem0 37257 posbezout 41700 fltnltalem 42218 binomcxplemdvbinom 43929 zltlesub 44802 supxrge 44855 ltadd12dd 44860 xrralrecnnle 44900 0ellimcdiv 45172 climleltrp 45199 ioodvbdlimc1lem2 45455 stoweidlem11 45534 stoweidlem14 45537 stoweidlem26 45549 stoweidlem44 45567 dirkertrigeqlem3 45623 dirkercncflem1 45626 dirkercncflem2 45627 fourierdlem4 45634 fourierdlem10 45640 fourierdlem28 45658 fourierdlem40 45670 fourierdlem50 45679 fourierdlem57 45686 fourierdlem59 45688 fourierdlem60 45689 fourierdlem61 45690 fourierdlem68 45697 fourierdlem74 45703 fourierdlem75 45704 fourierdlem76 45705 fourierdlem78 45707 fourierdlem79 45708 fourierdlem84 45713 fourierdlem93 45722 fourierdlem111 45740 fouriersw 45754 smfaddlem1 46286 smflimlem3 46296 |
Copyright terms: Public domain | W3C validator |