This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )