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	$$⊢\phi \to N\in \mathbb{N}$$
	knoppndvlem1.j	$$⊢\phi \to J\in \mathbb{Z}$$
	knoppndvlem1.m	$$⊢\phi \to M\in \mathbb{Z}$$
Assertion	knoppndvlem1	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem1.n	$$⊢\phi \to N\in \mathbb{N}$$
2		knoppndvlem1.j	$$⊢\phi \to J\in \mathbb{Z}$$
3		knoppndvlem1.m	$$⊢\phi \to M\in \mathbb{Z}$$
4		2re	$$⊢2\in ℝ$$
5	4	a1i	$$⊢\phi \to 2\in ℝ$$
6		nnz	$$⊢N\in \mathbb{N}\to N\in \mathbb{Z}$$
7	1 6	syl	$$⊢\phi \to N\in \mathbb{Z}$$
8	7	zred	$$⊢\phi \to N\in ℝ$$
9	5 8	remulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
10	5	recnd	$$⊢\phi \to 2\in ℂ$$
11	8	recnd	$$⊢\phi \to N\in ℂ$$
12		2ne0	$$⊢2\ne 0$$
13	12	a1i	$$⊢\phi \to 2\ne 0$$
14		0red	$$⊢\phi \to 0\in ℝ$$
15		1red	$$⊢\phi \to 1\in ℝ$$
16		0lt1	$$⊢0<1$$
17	16	a1i	$$⊢\phi \to 0<1$$
18		nnge1	$$⊢N\in \mathbb{N}\to 1\le N$$
19	1 18	syl	$$⊢\phi \to 1\le N$$
20	14 15 8 17 19	ltletrd	$$⊢\phi \to 0<N$$
21	14 20	ltned	$$⊢\phi \to 0\ne N$$
22	21	necomd	$$⊢\phi \to N\ne 0$$
23	10 11 13 22	mulne0d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0$$
24	2	znegcld	$$⊢\phi \to -J\in \mathbb{Z}$$
25	9 23 24	reexpclzd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\in ℝ$$
26	25 5 13	redivcld	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\in ℝ$$
27	3	zred	$$⊢\phi \to M\in ℝ$$
28	26 27	remulcld	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℝ$$