Metamath Proof Explorer

Theorem itcovalt2lem2lem1

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

Ref Expression
Assertion itcovalt2lem2lem1 ⊢ Y ∈ ℕ ∧ C ∈ ℕ 0 ∧ N ∈ ℕ 0 → N + C ⁢ Y − C ∈ ℕ 0

Proof

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