Theorem nn0sumltlt

Description: If the sum of two nonnegative integers is less than a third integer, then one of the summands is already less than this third integer. (Contributed by AV, 19-Oct-2019)

	Ref	Expression
Assertion	nn0sumltlt	|- ( ( a e. NN0 /\ b e. NN0 /\ c e. NN0 ) -> ( ( a + b ) < c -> b < c ) )

Proof

Step	Hyp	Ref	Expression
1		nn0re	|- ( a e. NN0 -> a e. RR )
2		nn0re	|- ( b e. NN0 -> b e. RR )
3		nn0re	|- ( c e. NN0 -> c e. RR )
4		ltaddsub2	|- ( ( a e. RR /\ b e. RR /\ c e. RR ) -> ( ( a + b ) < c <-> b < ( c - a ) ) )
5	1 2 3 4	syl3an	|- ( ( a e. NN0 /\ b e. NN0 /\ c e. NN0 ) -> ( ( a + b ) < c <-> b < ( c - a ) ) )
6		nn0ge0	|- ( a e. NN0 -> 0 <_ a )
7	6	3ad2ant1	|- ( ( a e. NN0 /\ b e. NN0 /\ c e. NN0 ) -> 0 <_ a )
8	1 3	anim12ci	|- ( ( a e. NN0 /\ c e. NN0 ) -> ( c e. RR /\ a e. RR ) )
9	8	3adant2	|- ( ( a e. NN0 /\ b e. NN0 /\ c e. NN0 ) -> ( c e. RR /\ a e. RR ) )
10		subge02	|- ( ( c e. RR /\ a e. RR ) -> ( 0 <_ a <-> ( c - a ) <_ c ) )
11	10	bicomd	|- ( ( c e. RR /\ a e. RR ) -> ( ( c - a ) <_ c <-> 0 <_ a ) )
12	9 11	syl	|- ( ( a e. NN0 /\ b e. NN0 /\ c e. NN0 ) -> ( ( c - a ) <_ c <-> 0 <_ a ) )
13	7 12	mpbird	|- ( ( a e. NN0 /\ b e. NN0 /\ c e. NN0 ) -> ( c - a ) <_ c )
14	2	3ad2ant2	|- ( ( a e. NN0 /\ b e. NN0 /\ c e. NN0 ) -> b e. RR )
15		nn0resubcl	|- ( ( c e. NN0 /\ a e. NN0 ) -> ( c - a ) e. RR )
16	15	ancoms	|- ( ( a e. NN0 /\ c e. NN0 ) -> ( c - a ) e. RR )
17	16	3adant2	|- ( ( a e. NN0 /\ b e. NN0 /\ c e. NN0 ) -> ( c - a ) e. RR )
18	3	3ad2ant3	|- ( ( a e. NN0 /\ b e. NN0 /\ c e. NN0 ) -> c e. RR )
19		ltletr	|- ( ( b e. RR /\ ( c - a ) e. RR /\ c e. RR ) -> ( ( b < ( c - a ) /\ ( c - a ) <_ c ) -> b < c ) )
20	14 17 18 19	syl3anc	|- ( ( a e. NN0 /\ b e. NN0 /\ c e. NN0 ) -> ( ( b < ( c - a ) /\ ( c - a ) <_ c ) -> b < c ) )
21	13 20	mpan2d	|- ( ( a e. NN0 /\ b e. NN0 /\ c e. NN0 ) -> ( b < ( c - a ) -> b < c ) )
22	5 21	sylbid	|- ( ( a e. NN0 /\ b e. NN0 /\ c e. NN0 ) -> ( ( a + b ) < c -> b < c ) )