Theorem ltadd2dd 10491

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

Syntax hints:   → wi 4   ∈ wcel 2157   class class class wbr 4855  (class class class)co 6884  ℝcr 10230   + caddc 10234   < clt 10369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-resscn 10288  ax-addrcl 10292  ax-pre-lttri 10305  ax-pre-ltadd 10307

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-opab 4918  df-mpt 4935  df-id 5232  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-ov 6887  df-er 7989  df-en 8203  df-dom 8204  df-sdom 8205  df-pnf 10371  df-mnf 10372  df-ltxr 10374

This theorem is referenced by:  zltaddlt1le  12567  2tnp1ge0ge0  12874  ccatrn  13606  eirrlem  15172  prmreclem5  15861  iccntr  22858  icccmplem2  22860  ivthlem2  23456  uniioombllem3  23589  opnmbllem  23605  dvcnvre  24019  cosordlem  24515  efif1olem2  24527  atanlogaddlem  24877  pntibndlem2  25517  pntlemr  25528  dya2icoseg  30687  opnmbllem0  33777  binomcxplemdvbinom  39070  zltlesub  39997  supxrge  40052  ltadd12dd  40057  xrralrecnnle  40100  0ellimcdiv  40379  climleltrp  40406  ioodvbdlimc1lem2  40645  stoweidlem11  40725  stoweidlem14  40728  stoweidlem26  40740  stoweidlem44  40758  dirkertrigeqlem3  40814  dirkercncflem1  40817  dirkercncflem2  40818  fourierdlem4  40825  fourierdlem10  40831  fourierdlem28  40849  fourierdlem40  40861  fourierdlem50  40870  fourierdlem57  40877  fourierdlem59  40879  fourierdlem60  40880  fourierdlem61  40881  fourierdlem68  40888  fourierdlem74  40894  fourierdlem75  40895  fourierdlem76  40896  fourierdlem78  40898  fourierdlem79  40899  fourierdlem84  40904  fourierdlem93  40913  fourierdlem111  40931  fouriersw  40945  smfaddlem1  41471  smflimlem3  41481