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

Metamath Proof Explorer

Theorem difgtsumgt

Description: If the difference of a real number and a nonnegative integer is greater than another real number, the sum of the real number and the nonnegative integer is also greater than the other real number. (Contributed by AV, 13-Aug-2021)

Ref Expression
Assertion difgtsumgt 
|- ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> ( C < ( A - B ) -> C < ( A + B ) ) )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 nn0cn 
 |-  ( B e. NN0 -> B e. CC )
3 1 2 anim12i 
 |-  ( ( A e. RR /\ B e. NN0 ) -> ( A e. CC /\ B e. CC ) )
4 3 3adant3 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> ( A e. CC /\ B e. CC ) )
5 negsub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
6 4 5 syl 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> ( A + -u B ) = ( A - B ) )
7 6 eqcomd 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> ( A - B ) = ( A + -u B ) )
8 7 breq2d 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> ( C < ( A - B ) <-> C < ( A + -u B ) ) )
9 simp3 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> C e. RR )
10 simp1 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> A e. RR )
11 nn0re 
 |-  ( B e. NN0 -> B e. RR )
12 11 renegcld 
 |-  ( B e. NN0 -> -u B e. RR )
13 12 3ad2ant2 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> -u B e. RR )
14 10 13 readdcld 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> ( A + -u B ) e. RR )
15 11 3ad2ant2 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> B e. RR )
16 10 15 readdcld 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> ( A + B ) e. RR )
17 9 14 16 3jca 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> ( C e. RR /\ ( A + -u B ) e. RR /\ ( A + B ) e. RR ) )
18 nn0negleid 
 |-  ( B e. NN0 -> -u B <_ B )
19 18 3ad2ant2 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> -u B <_ B )
20 13 15 10 19 leadd2dd 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> ( A + -u B ) <_ ( A + B ) )
21 17 20 lelttrdi 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> ( C < ( A + -u B ) -> C < ( A + B ) ) )
22 8 21 sylbid 
 |-  ( ( A e. RR /\ B e. NN0 /\ C e. RR ) -> ( C < ( A - B ) -> C < ( A + B ) ) )