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	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) → ( ( 𝑎 + 𝑏 ) < 𝑐 → 𝑏 < 𝑐 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0re	⊢ ( 𝑎 ∈ ℕ0 → 𝑎 ∈ ℝ )
2		nn0re	⊢ ( 𝑏 ∈ ℕ0 → 𝑏 ∈ ℝ )
3		nn0re	⊢ ( 𝑐 ∈ ℕ0 → 𝑐 ∈ ℝ )
4		ltaddsub2	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( ( 𝑎 + 𝑏 ) < 𝑐 ↔ 𝑏 < ( 𝑐 − 𝑎 ) ) )
5	1 2 3 4	syl3an	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) → ( ( 𝑎 + 𝑏 ) < 𝑐 ↔ 𝑏 < ( 𝑐 − 𝑎 ) ) )
6		nn0ge0	⊢ ( 𝑎 ∈ ℕ0 → 0 ≤ 𝑎 )
7	6	3ad2ant1	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) → 0 ≤ 𝑎 )
8	1 3	anim12ci	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) → ( 𝑐 ∈ ℝ ∧ 𝑎 ∈ ℝ ) )
9	8	3adant2	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) → ( 𝑐 ∈ ℝ ∧ 𝑎 ∈ ℝ ) )
10		subge02	⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑎 ∈ ℝ ) → ( 0 ≤ 𝑎 ↔ ( 𝑐 − 𝑎 ) ≤ 𝑐 ) )
11	10	bicomd	⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑎 ∈ ℝ ) → ( ( 𝑐 − 𝑎 ) ≤ 𝑐 ↔ 0 ≤ 𝑎 ) )
12	9 11	syl	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) → ( ( 𝑐 − 𝑎 ) ≤ 𝑐 ↔ 0 ≤ 𝑎 ) )
13	7 12	mpbird	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) → ( 𝑐 − 𝑎 ) ≤ 𝑐 )
14	2	3ad2ant2	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) → 𝑏 ∈ ℝ )
15		nn0resubcl	⊢ ( ( 𝑐 ∈ ℕ0 ∧ 𝑎 ∈ ℕ0 ) → ( 𝑐 − 𝑎 ) ∈ ℝ )
16	15	ancoms	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) → ( 𝑐 − 𝑎 ) ∈ ℝ )
17	16	3adant2	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) → ( 𝑐 − 𝑎 ) ∈ ℝ )
18	3	3ad2ant3	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) → 𝑐 ∈ ℝ )
19		ltletr	⊢ ( ( 𝑏 ∈ ℝ ∧ ( 𝑐 − 𝑎 ) ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( ( 𝑏 < ( 𝑐 − 𝑎 ) ∧ ( 𝑐 − 𝑎 ) ≤ 𝑐 ) → 𝑏 < 𝑐 ) )
20	14 17 18 19	syl3anc	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) → ( ( 𝑏 < ( 𝑐 − 𝑎 ) ∧ ( 𝑐 − 𝑎 ) ≤ 𝑐 ) → 𝑏 < 𝑐 ) )
21	13 20	mpan2d	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) → ( 𝑏 < ( 𝑐 − 𝑎 ) → 𝑏 < 𝑐 ) )
22	5 21	sylbid	⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) → ( ( 𝑎 + 𝑏 ) < 𝑐 → 𝑏 < 𝑐 ) )