Theorem itcovalt2lem2lem1

Description: Lemma 1 for itcovalt2lem2 . (Contributed by AV, 6-May-2024)

	Ref	Expression
Assertion	itcovalt2lem2lem1	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑁 + 𝐶 ) · 𝑌 ) − 𝐶 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		nn0re	⊢ ( 𝐶 ∈ ℕ0 → 𝐶 ∈ ℝ )
2	1	adantl	⊢ ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℝ )
3	2	adantr	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐶 ∈ ℝ )
4		simpr	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
5		simpr	⊢ ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℕ0 )
6	5	adantr	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐶 ∈ ℕ0 )
7	4 6	nn0addcld	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 𝐶 ) ∈ ℕ0 )
8	7	nn0red	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 𝐶 ) ∈ ℝ )
9		nnnn0	⊢ ( 𝑌 ∈ ℕ → 𝑌 ∈ ℕ0 )
10	9	ad2antrr	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑌 ∈ ℕ0 )
11	7 10	nn0mulcld	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 + 𝐶 ) · 𝑌 ) ∈ ℕ0 )
12	11	nn0red	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 + 𝐶 ) · 𝑌 ) ∈ ℝ )
13		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
14	13	adantl	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ 𝑁 )
15	6	nn0red	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐶 ∈ ℝ )
16	4	nn0red	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
17	15 16	addge02d	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 0 ≤ 𝑁 ↔ 𝐶 ≤ ( 𝑁 + 𝐶 ) ) )
18	14 17	mpbid	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐶 ≤ ( 𝑁 + 𝐶 ) )
19		simpll	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑌 ∈ ℕ )
20	19	nnred	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑌 ∈ ℝ )
21	7	nn0ge0d	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ ( 𝑁 + 𝐶 ) )
22		nnge1	⊢ ( 𝑌 ∈ ℕ → 1 ≤ 𝑌 )
23	22	ad2antrr	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 1 ≤ 𝑌 )
24	8 20 21 23	lemulge11d	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 𝐶 ) ≤ ( ( 𝑁 + 𝐶 ) · 𝑌 ) )
25	3 8 12 18 24	letrd	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐶 ≤ ( ( 𝑁 + 𝐶 ) · 𝑌 ) )
26		nn0sub	⊢ ( ( 𝐶 ∈ ℕ0 ∧ ( ( 𝑁 + 𝐶 ) · 𝑌 ) ∈ ℕ0 ) → ( 𝐶 ≤ ( ( 𝑁 + 𝐶 ) · 𝑌 ) ↔ ( ( ( 𝑁 + 𝐶 ) · 𝑌 ) − 𝐶 ) ∈ ℕ0 ) )
27	6 11 26	syl2anc	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐶 ≤ ( ( 𝑁 + 𝐶 ) · 𝑌 ) ↔ ( ( ( 𝑁 + 𝐶 ) · 𝑌 ) − 𝐶 ) ∈ ℕ0 ) )
28	25 27	mpbid	⊢ ( ( ( 𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑁 + 𝐶 ) · 𝑌 ) − 𝐶 ) ∈ ℕ0 )