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

Metamath Proof Explorer

Theorem lesub3d

Description: The result of subtracting a number less than or equal to an intermediate number from a number greater than or equal to a third number increased by the intermediate number is greater than or equal to the third number. (Contributed by AV, 13-Aug-2020)

Ref Expression
Hypotheses leidd.1 
|- ( ph -> A e. RR )
ltnegd.2 
|- ( ph -> B e. RR )
ltadd1d.3 
|- ( ph -> C e. RR )
lesub3d.x 
|- ( ph -> X e. RR )
lesub3d.g 
|- ( ph -> ( X + C ) <_ A )
lesub3d.l 
|- ( ph -> B <_ X )
Assertion lesub3d 
|- ( ph -> C <_ ( A - B ) )

Proof

Step Hyp Ref Expression
1 leidd.1 
 |-  ( ph -> A e. RR )
2 ltnegd.2 
 |-  ( ph -> B e. RR )
3 ltadd1d.3 
 |-  ( ph -> C e. RR )
4 lesub3d.x 
 |-  ( ph -> X e. RR )
5 lesub3d.g 
 |-  ( ph -> ( X + C ) <_ A )
6 lesub3d.l 
 |-  ( ph -> B <_ X )
7 3 2 readdcld 
 |-  ( ph -> ( C + B ) e. RR )
8 4 3 readdcld 
 |-  ( ph -> ( X + C ) e. RR )
9 3 recnd 
 |-  ( ph -> C e. CC )
10 2 recnd 
 |-  ( ph -> B e. CC )
11 9 10 addcomd 
 |-  ( ph -> ( C + B ) = ( B + C ) )
12 2 4 3 6 leadd1dd 
 |-  ( ph -> ( B + C ) <_ ( X + C ) )
13 11 12 eqbrtrd 
 |-  ( ph -> ( C + B ) <_ ( X + C ) )
14 7 8 1 13 5 letrd 
 |-  ( ph -> ( C + B ) <_ A )
15 leaddsub 
 |-  ( ( C e. RR /\ B e. RR /\ A e. RR ) -> ( ( C + B ) <_ A <-> C <_ ( A - B ) ) )
16 3 2 1 15 syl3anc 
 |-  ( ph -> ( ( C + B ) <_ A <-> C <_ ( A - B ) ) )
17 14 16 mpbid 
 |-  ( ph -> C <_ ( A - B ) )