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

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem2.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		knoppndvlem2.i	⊢ ( 𝜑 → 𝐼 ∈ ℤ )
3		knoppndvlem2.j	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
4		knoppndvlem2.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		knoppndvlem2.1	⊢ ( 𝜑 → 𝐽 < 𝐼 )
6		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
7		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
8	1 7	syl	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
9	8	zcnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
10	6 9	mulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
11		2ne0	⊢ 2 ≠ 0
12	11	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
13		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
14		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
15	8	zred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
16		0lt1	⊢ 0 < 1
17	16	a1i	⊢ ( 𝜑 → 0 < 1 )
18		nnge1	⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
19	1 18	syl	⊢ ( 𝜑 → 1 ≤ 𝑁 )
20	13 14 15 17 19	ltletrd	⊢ ( 𝜑 → 0 < 𝑁 )
21	13 20	ltned	⊢ ( 𝜑 → 0 ≠ 𝑁 )
22	21	necomd	⊢ ( 𝜑 → 𝑁 ≠ 0 )
23	6 9 12 22	mulne0d	⊢ ( 𝜑 → ( 2 · 𝑁 ) ≠ 0 )
24	10 23 2	expclzd	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 𝐼 ) ∈ ℂ )
25	3	znegcld	⊢ ( 𝜑 → - 𝐽 ∈ ℤ )
26	10 23 25	expclzd	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ∈ ℂ )
27	26 6 12	divcld	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ∈ ℂ )
28	4	zcnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
29	24 27 28	mulassd	⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) · 𝑀 ) = ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) )
30	29	eqcomd	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) = ( ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) · 𝑀 ) )
31	24 26 6 12	divassd	⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) / 2 ) = ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) )
32	31	eqcomd	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) = ( ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) / 2 ) )
33	10 23	jca	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ≠ 0 ) )
34	2 25	jca	⊢ ( 𝜑 → ( 𝐼 ∈ ℤ ∧ - 𝐽 ∈ ℤ ) )
35	33 34	jca	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ≠ 0 ) ∧ ( 𝐼 ∈ ℤ ∧ - 𝐽 ∈ ℤ ) ) )
36		expaddz	⊢ ( ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 2 · 𝑁 ) ≠ 0 ) ∧ ( 𝐼 ∈ ℤ ∧ - 𝐽 ∈ ℤ ) ) → ( ( 2 · 𝑁 ) ↑ ( 𝐼 + - 𝐽 ) ) = ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) )
37	35 36	syl	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( 𝐼 + - 𝐽 ) ) = ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) )
38	37	eqcomd	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) = ( ( 2 · 𝑁 ) ↑ ( 𝐼 + - 𝐽 ) ) )
39	2	zcnd	⊢ ( 𝜑 → 𝐼 ∈ ℂ )
40	3	zcnd	⊢ ( 𝜑 → 𝐽 ∈ ℂ )
41	39 40	negsubd	⊢ ( 𝜑 → ( 𝐼 + - 𝐽 ) = ( 𝐼 − 𝐽 ) )
42	41	oveq2d	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( 𝐼 + - 𝐽 ) ) = ( ( 2 · 𝑁 ) ↑ ( 𝐼 − 𝐽 ) ) )
43	3 2	jca	⊢ ( 𝜑 → ( 𝐽 ∈ ℤ ∧ 𝐼 ∈ ℤ ) )
44		znnsub	⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝐽 < 𝐼 ↔ ( 𝐼 − 𝐽 ) ∈ ℕ ) )
45	43 44	syl	⊢ ( 𝜑 → ( 𝐽 < 𝐼 ↔ ( 𝐼 − 𝐽 ) ∈ ℕ ) )
46	5 45	mpbid	⊢ ( 𝜑 → ( 𝐼 − 𝐽 ) ∈ ℕ )
47	10 46	jca	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 𝐼 − 𝐽 ) ∈ ℕ ) )
48		expm1t	⊢ ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( 𝐼 − 𝐽 ) ∈ ℕ ) → ( ( 2 · 𝑁 ) ↑ ( 𝐼 − 𝐽 ) ) = ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · ( 2 · 𝑁 ) ) )
49	47 48	syl	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( 𝐼 − 𝐽 ) ) = ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · ( 2 · 𝑁 ) ) )
50	38 42 49	3eqtrd	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) = ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · ( 2 · 𝑁 ) ) )
51	50	oveq1d	⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) / 2 ) = ( ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · ( 2 · 𝑁 ) ) / 2 ) )
52	2 3	jca	⊢ ( 𝜑 → ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) )
53		zsubcl	⊢ ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐼 − 𝐽 ) ∈ ℤ )
54	52 53	syl	⊢ ( 𝜑 → ( 𝐼 − 𝐽 ) ∈ ℤ )
55		peano2zm	⊢ ( ( 𝐼 − 𝐽 ) ∈ ℤ → ( ( 𝐼 − 𝐽 ) − 1 ) ∈ ℤ )
56	54 55	syl	⊢ ( 𝜑 → ( ( 𝐼 − 𝐽 ) − 1 ) ∈ ℤ )
57	3	zred	⊢ ( 𝜑 → 𝐽 ∈ ℝ )
58	2	zred	⊢ ( 𝜑 → 𝐼 ∈ ℝ )
59	57 58	posdifd	⊢ ( 𝜑 → ( 𝐽 < 𝐼 ↔ 0 < ( 𝐼 − 𝐽 ) ) )
60	5 59	mpbid	⊢ ( 𝜑 → 0 < ( 𝐼 − 𝐽 ) )
61		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
62	61 54	jca	⊢ ( 𝜑 → ( 0 ∈ ℤ ∧ ( 𝐼 − 𝐽 ) ∈ ℤ ) )
63		zltlem1	⊢ ( ( 0 ∈ ℤ ∧ ( 𝐼 − 𝐽 ) ∈ ℤ ) → ( 0 < ( 𝐼 − 𝐽 ) ↔ 0 ≤ ( ( 𝐼 − 𝐽 ) − 1 ) ) )
64	62 63	syl	⊢ ( 𝜑 → ( 0 < ( 𝐼 − 𝐽 ) ↔ 0 ≤ ( ( 𝐼 − 𝐽 ) − 1 ) ) )
65	60 64	mpbid	⊢ ( 𝜑 → 0 ≤ ( ( 𝐼 − 𝐽 ) − 1 ) )
66	56 65	jca	⊢ ( 𝜑 → ( ( ( 𝐼 − 𝐽 ) − 1 ) ∈ ℤ ∧ 0 ≤ ( ( 𝐼 − 𝐽 ) − 1 ) ) )
67		elnn0z	⊢ ( ( ( 𝐼 − 𝐽 ) − 1 ) ∈ ℕ0 ↔ ( ( ( 𝐼 − 𝐽 ) − 1 ) ∈ ℤ ∧ 0 ≤ ( ( 𝐼 − 𝐽 ) − 1 ) ) )
68	66 67	sylibr	⊢ ( 𝜑 → ( ( 𝐼 − 𝐽 ) − 1 ) ∈ ℕ0 )
69	10 68	expcld	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) ∈ ℂ )
70	69 10 6 12	divassd	⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · ( 2 · 𝑁 ) ) / 2 ) = ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · ( ( 2 · 𝑁 ) / 2 ) ) )
71	9 6 12	divcan3d	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) / 2 ) = 𝑁 )
72	71	oveq2d	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · ( ( 2 · 𝑁 ) / 2 ) ) = ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · 𝑁 ) )
73	70 72	eqtrd	⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · ( 2 · 𝑁 ) ) / 2 ) = ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · 𝑁 ) )
74	32 51 73	3eqtrd	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) = ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · 𝑁 ) )
75	74	oveq1d	⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) · 𝑀 ) = ( ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · 𝑁 ) · 𝑀 ) )
76	30 75	eqtrd	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) = ( ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · 𝑁 ) · 𝑀 ) )
77		2z	⊢ 2 ∈ ℤ
78	77	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
79	78 8	jca	⊢ ( 𝜑 → ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
80		zmulcl	⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 · 𝑁 ) ∈ ℤ )
81	79 80	syl	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℤ )
82	81 68	jca	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℤ ∧ ( ( 𝐼 − 𝐽 ) − 1 ) ∈ ℕ0 ) )
83		zexpcl	⊢ ( ( ( 2 · 𝑁 ) ∈ ℤ ∧ ( ( 𝐼 − 𝐽 ) − 1 ) ∈ ℕ0 ) → ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) ∈ ℤ )
84	82 83	syl	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) ∈ ℤ )
85	84 8	zmulcld	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · 𝑁 ) ∈ ℤ )
86	85 4	zmulcld	⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ ( ( 𝐼 − 𝐽 ) − 1 ) ) · 𝑁 ) · 𝑀 ) ∈ ℤ )
87	76 86	eqeltrd	⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐼 ) · ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) ∈ ℤ )