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