Metamath Proof Explorer


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 )