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	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	knoppndvlem1.j	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
	knoppndvlem1.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
Assertion	knoppndvlem1	⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		knoppndvlem1.j	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
3		knoppndvlem1.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		2re	⊢ 2 ∈ ℝ
5	4	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
6		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
7	1 6	syl	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
8	7	zred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
9	5 8	remulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
10	5	recnd	⊢ ( 𝜑 → 2 ∈ ℂ )
11	8	recnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
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	⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
19	1 18	syl	⊢ ( 𝜑 → 1 ≤ 𝑁 )
20	14 15 8 17 19	ltletrd	⊢ ( 𝜑 → 0 < 𝑁 )
21	14 20	ltned	⊢ ( 𝜑 → 0 ≠ 𝑁 )
22	21	necomd	⊢ ( 𝜑 → 𝑁 ≠ 0 )
23	10 11 13 22	mulne0d	⊢ ( 𝜑 → ( 2 · 𝑁 ) ≠ 0 )
24	2	znegcld	⊢ ( 𝜑 → - 𝐽 ∈ ℤ )
25	9 23 24	reexpclzd	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ∈ ℝ )
26	25 5 13	redivcld	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ∈ ℝ )
27	3	zred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
28	26 27	remulcld	⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ∈ ℝ )