Theorem ltadd2dd 11290

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 11287	. 2 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵)))
6	1, 5	mpbid 232	1 ⊢ (𝜑 → (𝐶 + 𝐴) < (𝐶 + 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5096  (class class class)co 7356  ℝcr 11023   + caddc 11027   < clt 11164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-addrcl 11085  ax-pre-lttri 11098  ax-pre-ltadd 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7359  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-ltxr 11169

This theorem is referenced by:  zltaddlt1le  13419  2tnp1ge0ge0  13747  ccatrn  14511  eirrlem  16127  prmreclem5  16846  iccntr  24764  icccmplem2  24766  ivthlem2  25407  uniioombllem3  25540  opnmbllem  25556  dvcnvre  25978  cosordlem  26493  efif1olem2  26506  atanlogaddlem  26877  pntibndlem2  27556  pntlemr  27567  dya2icoseg  34383  opnmbllem0  37796  posbezout  42293  fltnltalem  42847  binomcxplemdvbinom  44536  zltlesub  45475  supxrge  45525  ltadd12dd  45530  xrralrecnnle  45569  0ellimcdiv  45835  climleltrp  45862  ioodvbdlimc1lem2  46118  stoweidlem11  46197  stoweidlem14  46200  stoweidlem26  46212  stoweidlem44  46230  dirkertrigeqlem3  46286  dirkercncflem1  46289  dirkercncflem2  46290  fourierdlem4  46297  fourierdlem10  46303  fourierdlem28  46321  fourierdlem40  46333  fourierdlem50  46342  fourierdlem57  46349  fourierdlem59  46351  fourierdlem60  46352  fourierdlem61  46353  fourierdlem68  46360  fourierdlem74  46366  fourierdlem75  46367  fourierdlem76  46368  fourierdlem78  46370  fourierdlem79  46371  fourierdlem84  46376  fourierdlem93  46385  fourierdlem111  46403  fouriersw  46417  smfaddlem1  46949  smflimlem3  46959