Theorem ltadd2dd 11469

Description: Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
letrd.3	⊢ (𝜑 → 𝐶 ∈ ℝ)
ltletrd.4	⊢ (𝜑 → 𝐴 < 𝐵)

Assertion

Ref	Expression
ltadd2dd	⊢ (𝜑 → (𝐶 + 𝐴) < (𝐶 + 𝐵))

Proof of Theorem 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 11466	. 2 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵)))
6	1, 5	mpbid 235	1 ⊢ (𝜑 → (𝐶 + 𝐴) < (𝐶 + 𝐵))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  (class class class)co 7420  ℝcr 11199   + caddc 11203   < clt 11343

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-resscn 11257  ax-addrcl 11261  ax-pre-lttri 11274  ax-pre-ltadd 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348

This theorem is used by:  zltaddlt1le  13636  2tnp1ge0ge0  13969  ccatrn  14735  eirrlem  16372  prmreclem5  17098  iccntr  25141  icccmplem2  25143  ivthlem2  25773  uniioombllem3  25906  opnmbllem  25922  dvcnvre  26339  cosordlem  26858  efif1olem2  26871  atanlogaddlem  27241  pntibndlem2  27918  pntlemr  27929  dya2icoseg  34909  opnmbllem0  38574  posbezout  43150  fltnltalem  43673  binomcxplemdvbinom  45336  zltlesub  46300  supxrge  46349  ltadd12dd  46354  xrralrecnnle  46393  0ellimcdiv  46658  climleltrp  46685  ioodvbdlimc1lem2  46941  stoweidlem11  47020  stoweidlem14  47023  stoweidlem26  47035  stoweidlem44  47053  dirkertrigeqlem3  47109  dirkercncflem1  47112  dirkercncflem2  47113  fourierdlem4  47120  fourierdlem10  47126  fourierdlem28  47144  fourierdlem40  47156  fourierdlem50  47165  fourierdlem57  47172  fourierdlem59  47174  fourierdlem60  47175  fourierdlem61  47176  fourierdlem68  47183  fourierdlem74  47189  fourierdlem75  47190  fourierdlem76  47191  fourierdlem78  47193  fourierdlem79  47194  fourierdlem84  47199  fourierdlem93  47208  fourierdlem111  47226  fouriersw  47240  smfaddlem1  47772  smflimlem3  47782