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