Metamath Proof Explorer

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 ) · 𝑀 ) ) ∈ ℤ )