Theorem knoppndvlem16

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 19-Jul-2021)

	Ref	Expression
Hypotheses	knoppndvlem16.a	$$⊢A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
	knoppndvlem16.b	$$⊢B=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)$$
	knoppndvlem16.j	$$⊢\phi \to J\in {\mathbb{N}}_0$$
	knoppndvlem16.m	$$⊢\phi \to M\in \mathbb{Z}$$
	knoppndvlem16.n	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	knoppndvlem16	$$⊢\phi \to B-A=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem16.a	$$⊢A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
2		knoppndvlem16.b	$$⊢B=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)$$
3		knoppndvlem16.j	$$⊢\phi \to J\in {\mathbb{N}}_0$$
4		knoppndvlem16.m	$$⊢\phi \to M\in \mathbb{Z}$$
5		knoppndvlem16.n	$$⊢\phi \to N\in \mathbb{N}$$
6	2	a1i	$$⊢\phi \to B=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)$$
7	1	a1i	$$⊢\phi \to A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
8	6 7	oveq12d	$$⊢\phi \to B-A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)-\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
9		2cnd	$$⊢\phi \to 2\in ℂ$$
10	5	nncnd	$$⊢\phi \to N\in ℂ$$
11	9 10	mulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
12		2ne0	$$⊢2\ne 0$$
13	12	a1i	$$⊢\phi \to 2\ne 0$$
14	5	nnne0d	$$⊢\phi \to N\ne 0$$
15	9 10 13 14	mulne0d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0$$
16	3	nn0zd	$$⊢\phi \to J\in \mathbb{Z}$$
17	16	znegcld	$$⊢\phi \to -J\in \mathbb{Z}$$
18	11 15 17	expclzd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\in ℂ$$
19	9 10 15	mulne0bad	$$⊢\phi \to 2\ne 0$$
20	18 9 19	divcld	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\in ℂ$$
21	4	zcnd	$$⊢\phi \to M\in ℂ$$
22		1cnd	$$⊢\phi \to 1\in ℂ$$
23	21 22	addcld	$$⊢\phi \to M+1\in ℂ$$
24	20 23 21	subdid	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1-M\right)=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)-\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
25	24	eqcomd	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1\right)-\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1-M\right)$$
26	21 22	pncan2d	$$⊢\phi \to M+1-M=1$$
27	26	oveq2d	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1-M\right)=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot 1$$
28	20	mulid1d	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot 1=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$
29	27 28	eqtrd	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\left(M+1-M\right)=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$
30	8 25 29	3eqtrd	$$⊢\phi \to B-A=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$