# Metamath Proof Explorer

## Theorem knoppndvlem1

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 15-Jun-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppndvlem1.n $⊢ φ → N ∈ ℕ$
knoppndvlem1.j $⊢ φ → J ∈ ℤ$
knoppndvlem1.m $⊢ φ → M ∈ ℤ$
Assertion knoppndvlem1 $⊢ φ → 2 ⋅ N − J 2 ⋅ M ∈ ℝ$

### Proof

Step Hyp Ref Expression
1 knoppndvlem1.n $⊢ φ → N ∈ ℕ$
2 knoppndvlem1.j $⊢ φ → J ∈ ℤ$
3 knoppndvlem1.m $⊢ φ → M ∈ ℤ$
4 2re $⊢ 2 ∈ ℝ$
5 4 a1i $⊢ φ → 2 ∈ ℝ$
6 nnz $⊢ N ∈ ℕ → N ∈ ℤ$
7 1 6 syl $⊢ φ → N ∈ ℤ$
8 7 zred $⊢ φ → N ∈ ℝ$
9 5 8 remulcld $⊢ φ → 2 ⋅ N ∈ ℝ$
10 5 recnd $⊢ φ → 2 ∈ ℂ$
11 8 recnd $⊢ φ → N ∈ ℂ$
12 2ne0 $⊢ 2 ≠ 0$
13 12 a1i $⊢ φ → 2 ≠ 0$
14 0red $⊢ φ → 0 ∈ ℝ$
15 1red $⊢ φ → 1 ∈ ℝ$
16 0lt1 $⊢ 0 < 1$
17 16 a1i $⊢ φ → 0 < 1$
18 nnge1 $⊢ N ∈ ℕ → 1 ≤ N$
19 1 18 syl $⊢ φ → 1 ≤ N$
20 14 15 8 17 19 ltletrd $⊢ φ → 0 < N$
21 14 20 ltned $⊢ φ → 0 ≠ N$
22 21 necomd $⊢ φ → N ≠ 0$
23 10 11 13 22 mulne0d $⊢ φ → 2 ⋅ N ≠ 0$
24 2 znegcld $⊢ φ → − J ∈ ℤ$
25 9 23 24 reexpclzd $⊢ φ → 2 ⋅ N − J ∈ ℝ$
26 25 5 13 redivcld $⊢ φ → 2 ⋅ N − J 2 ∈ ℝ$
27 3 zred $⊢ φ → M ∈ ℝ$
28 26 27 remulcld $⊢ φ → 2 ⋅ N − J 2 ⋅ M ∈ ℝ$