This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )