Theorem knoppndvlem2

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

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

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem2.n	$$⊢\phi \to N\in \mathbb{N}$$
2		knoppndvlem2.i	$$⊢\phi \to I\in \mathbb{Z}$$
3		knoppndvlem2.j	$$⊢\phi \to J\in \mathbb{Z}$$
4		knoppndvlem2.m	$$⊢\phi \to M\in \mathbb{Z}$$
5		knoppndvlem2.1	$$⊢\phi \to J<I$$
6		2cnd	$$⊢\phi \to 2\in ℂ$$
7		nnz	$$⊢N\in \mathbb{N}\to N\in \mathbb{Z}$$
8	1 7	syl	$$⊢\phi \to N\in \mathbb{Z}$$
9	8	zcnd	$$⊢\phi \to N\in ℂ$$
10	6 9	mulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
11		2ne0	$$⊢2\ne 0$$
12	11	a1i	$$⊢\phi \to 2\ne 0$$
13		0red	$$⊢\phi \to 0\in ℝ$$
14		1red	$$⊢\phi \to 1\in ℝ$$
15	8	zred	$$⊢\phi \to N\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	13 14 15 17 19	ltletrd	$$⊢\phi \to 0<N$$
21	13 20	ltned	$$⊢\phi \to 0\ne N$$
22	21	necomd	$$⊢\phi \to N\ne 0$$
23	6 9 12 22	mulne0d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0$$
24	10 23 2	expclzd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I\in ℂ$$
25	3	znegcld	$$⊢\phi \to -J\in \mathbb{Z}$$
26	10 23 25	expclzd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\in ℂ$$
27	26 6 12	divcld	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\in ℂ$$
28	4	zcnd	$$⊢\phi \to M\in ℂ$$
29	24 27 28	mulassd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
30	29	eqcomd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
31	24 26 6 12	divassd	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)$$
32	31	eqcomd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$
33	10 23	jca	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0\right)$$
34	2 25	jca	$$⊢\phi \to \left(I\in \mathbb{Z}\wedge -J\in \mathbb{Z}\right)$$
35	33 34	jca	$$⊢\phi \to \left(\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0\right)\wedge \left(I\in \mathbb{Z}\wedge -J\in \mathbb{Z}\right)\right)$$
36		expaddz	$$⊢\left(\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0\right)\wedge \left(I\in \mathbb{Z}\wedge -J\in \mathbb{Z}\right)\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I+\mathrm{-<mi\; mathcolor="\#808">J</mi>}}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}$$
37	35 36	syl	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I+\mathrm{-<mi\; mathcolor="\#808">J</mi>}}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}$$
38	37	eqcomd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I+\mathrm{-<mi\; mathcolor="\#808">J</mi>}}$$
39	2	zcnd	$$⊢\phi \to I\in ℂ$$
40	3	zcnd	$$⊢\phi \to J\in ℂ$$
41	39 40	negsubd	$$⊢\phi \to I+\mathrm{-<mi\; mathcolor="\#808">J</mi>}=I-J$$
42	41	oveq2d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I+\mathrm{-<mi\; mathcolor="\#808">J</mi>}}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J}$$
43	3 2	jca	$$⊢\phi \to \left(J\in \mathbb{Z}\wedge I\in \mathbb{Z}\right)$$
44		znnsub	$$⊢\left(J\in \mathbb{Z}\wedge I\in \mathbb{Z}\right)\to \left(J<I\leftrightarrow I-J\in \mathbb{N}\right)$$
45	43 44	syl	$$⊢\phi \to \left(J<I\leftrightarrow I-J\in \mathbb{N}\right)$$
46	5 45	mpbid	$$⊢\phi \to I-J\in \mathbb{N}$$
47	10 46	jca	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge I-J\in \mathbb{N}\right)$$
48		expm1t	$$⊢\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ\wedge I-J\in \mathbb{N}\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
49	47 48	syl	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
50	38 42 49	3eqtrd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
51	50	oveq1d	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{2}$$
52	2 3	jca	$$⊢\phi \to \left(I\in \mathbb{Z}\wedge J\in \mathbb{Z}\right)$$
53		zsubcl	$$⊢\left(I\in \mathbb{Z}\wedge J\in \mathbb{Z}\right)\to I-J\in \mathbb{Z}$$
54	52 53	syl	$$⊢\phi \to I-J\in \mathbb{Z}$$
55		peano2zm	$$⊢I-J\in \mathbb{Z}\to I-J-1\in \mathbb{Z}$$
56	54 55	syl	$$⊢\phi \to I-J-1\in \mathbb{Z}$$
57	3	zred	$$⊢\phi \to J\in ℝ$$
58	2	zred	$$⊢\phi \to I\in ℝ$$
59	57 58	posdifd	$$⊢\phi \to \left(J<I\leftrightarrow 0<I-J\right)$$
60	5 59	mpbid	$$⊢\phi \to 0<I-J$$
61		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
62	61 54	jca	$$⊢\phi \to \left(0\in \mathbb{Z}\wedge I-J\in \mathbb{Z}\right)$$
63		zltlem1	$$⊢\left(0\in \mathbb{Z}\wedge I-J\in \mathbb{Z}\right)\to \left(0<I-J\leftrightarrow 0\le I-J-1\right)$$
64	62 63	syl	$$⊢\phi \to \left(0<I-J\leftrightarrow 0\le I-J-1\right)$$
65	60 64	mpbid	$$⊢\phi \to 0\le I-J-1$$
66	56 65	jca	$$⊢\phi \to \left(I-J-1\in \mathbb{Z}\wedge 0\le I-J-1\right)$$
67		elnn0z	$$⊢I-J-1\in {\mathbb{N}}_0\leftrightarrow \left(I-J-1\in \mathbb{Z}\wedge 0\le I-J-1\right)$$
68	66 67	sylibr	$$⊢\phi \to I-J-1\in {\mathbb{N}}_0$$
69	10 68	expcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}\in ℂ$$
70	69 10 6 12	divassd	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{2}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{2}\right)$$
71	9 6 12	divcan3d	$$⊢\phi \to \frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{2}=N$$
72	71	oveq2d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}\left(\frac{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{2}\right)={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
73	70 72	eqtrd	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}{2}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
74	32 51 73	3eqtrd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
75	74	oveq1d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
76	30 75	eqtrd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
77		2z	$$⊢2\in \mathbb{Z}$$
78	77	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
79	78 8	jca	$$⊢\phi \to \left(2\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)$$
80		zmulcl	$$⊢\left(2\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{Z}$$
81	79 80	syl	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{Z}$$
82	81 68	jca	$$⊢\phi \to \left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{Z}\wedge I-J-1\in {\mathbb{N}}_0\right)$$
83		zexpcl	$$⊢\left(2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{Z}\wedge I-J-1\in {\mathbb{N}}_0\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}\in \mathbb{Z}$$
84	82 83	syl	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}\in \mathbb{Z}$$
85	84 8	zmulcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{Z}$$
86	85 4	zmulcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{I-J-1}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in \mathbb{Z}$$
87	76 86	eqeltrd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^I\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in \mathbb{Z}$$