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	$$⊢\left(a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\wedge c\in {\mathbb{N}}_0\right)\to \left(a+b<c\to b<c\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$$⊢a\in {\mathbb{N}}_0\to a\in ℝ$$
2		nn0re	$$⊢b\in {\mathbb{N}}_0\to b\in ℝ$$
3		nn0re	$$⊢c\in {\mathbb{N}}_0\to c\in ℝ$$
4		ltaddsub2	$$⊢\left(a\in ℝ\wedge b\in ℝ\wedge c\in ℝ\right)\to \left(a+b<c\leftrightarrow b<c-a\right)$$
5	1 2 3 4	syl3an	$$⊢\left(a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\wedge c\in {\mathbb{N}}_0\right)\to \left(a+b<c\leftrightarrow b<c-a\right)$$
6		nn0ge0	$$⊢a\in {\mathbb{N}}_0\to 0\le a$$
7	6	3ad2ant1	$$⊢\left(a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\wedge c\in {\mathbb{N}}_0\right)\to 0\le a$$
8	1 3	anim12ci	$$⊢\left(a\in {\mathbb{N}}_0\wedge c\in {\mathbb{N}}_0\right)\to \left(c\in ℝ\wedge a\in ℝ\right)$$
9	8	3adant2	$$⊢\left(a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\wedge c\in {\mathbb{N}}_0\right)\to \left(c\in ℝ\wedge a\in ℝ\right)$$
10		subge02	$$⊢\left(c\in ℝ\wedge a\in ℝ\right)\to \left(0\le a\leftrightarrow c-a\le c\right)$$
11	10	bicomd	$$⊢\left(c\in ℝ\wedge a\in ℝ\right)\to \left(c-a\le c\leftrightarrow 0\le a\right)$$
12	9 11	syl	$$⊢\left(a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\wedge c\in {\mathbb{N}}_0\right)\to \left(c-a\le c\leftrightarrow 0\le a\right)$$
13	7 12	mpbird	$$⊢\left(a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\wedge c\in {\mathbb{N}}_0\right)\to c-a\le c$$
14	2	3ad2ant2	$$⊢\left(a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\wedge c\in {\mathbb{N}}_0\right)\to b\in ℝ$$
15		nn0resubcl	$$⊢\left(c\in {\mathbb{N}}_0\wedge a\in {\mathbb{N}}_0\right)\to c-a\in ℝ$$
16	15	ancoms	$$⊢\left(a\in {\mathbb{N}}_0\wedge c\in {\mathbb{N}}_0\right)\to c-a\in ℝ$$
17	16	3adant2	$$⊢\left(a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\wedge c\in {\mathbb{N}}_0\right)\to c-a\in ℝ$$
18	3	3ad2ant3	$$⊢\left(a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\wedge c\in {\mathbb{N}}_0\right)\to c\in ℝ$$
19		ltletr	$$⊢\left(b\in ℝ\wedge c-a\in ℝ\wedge c\in ℝ\right)\to \left(\left(b<c-a\wedge c-a\le c\right)\to b<c\right)$$
20	14 17 18 19	syl3anc	$$⊢\left(a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\wedge c\in {\mathbb{N}}_0\right)\to \left(\left(b<c-a\wedge c-a\le c\right)\to b<c\right)$$
21	13 20	mpan2d	$$⊢\left(a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\wedge c\in {\mathbb{N}}_0\right)\to \left(b<c-a\to b<c\right)$$
22	5 21	sylbid	$$⊢\left(a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\wedge c\in {\mathbb{N}}_0\right)\to \left(a+b<c\to b<c\right)$$