Metamath Proof Explorer


Theorem ltadd12dd

Description: Addition to both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ltadd12dd.a
|- ( ph -> A e. RR )
ltadd12dd.b
|- ( ph -> B e. RR )
ltadd12dd.c
|- ( ph -> C e. RR )
ltadd12dd.d
|- ( ph -> D e. RR )
ltadd12dd.ac
|- ( ph -> A < C )
ltadd12dd.bd
|- ( ph -> B < D )
Assertion ltadd12dd
|- ( ph -> ( A + B ) < ( C + D ) )

Proof

Step Hyp Ref Expression
1 ltadd12dd.a
 |-  ( ph -> A e. RR )
2 ltadd12dd.b
 |-  ( ph -> B e. RR )
3 ltadd12dd.c
 |-  ( ph -> C e. RR )
4 ltadd12dd.d
 |-  ( ph -> D e. RR )
5 ltadd12dd.ac
 |-  ( ph -> A < C )
6 ltadd12dd.bd
 |-  ( ph -> B < D )
7 1 2 readdcld
 |-  ( ph -> ( A + B ) e. RR )
8 3 2 readdcld
 |-  ( ph -> ( C + B ) e. RR )
9 3 4 readdcld
 |-  ( ph -> ( C + D ) e. RR )
10 1 3 2 5 ltadd1dd
 |-  ( ph -> ( A + B ) < ( C + B ) )
11 2 4 3 6 ltadd2dd
 |-  ( ph -> ( C + B ) < ( C + D ) )
12 7 8 9 10 11 lttrd
 |-  ( ph -> ( A + B ) < ( C + D ) )