Step |
Hyp |
Ref |
Expression |
1 |
|
knoppndvlem16.a |
⊢ 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) |
2 |
|
knoppndvlem16.b |
⊢ 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) |
3 |
|
knoppndvlem16.j |
⊢ ( 𝜑 → 𝐽 ∈ ℕ0 ) |
4 |
|
knoppndvlem16.m |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
5 |
|
knoppndvlem16.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
6 |
2
|
a1i |
⊢ ( 𝜑 → 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) ) |
7 |
1
|
a1i |
⊢ ( 𝜑 → 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) |
8 |
6 7
|
oveq12d |
⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) ) |
9 |
|
2cnd |
⊢ ( 𝜑 → 2 ∈ ℂ ) |
10 |
5
|
nncnd |
⊢ ( 𝜑 → 𝑁 ∈ ℂ ) |
11 |
9 10
|
mulcld |
⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ ) |
12 |
|
2ne0 |
⊢ 2 ≠ 0 |
13 |
12
|
a1i |
⊢ ( 𝜑 → 2 ≠ 0 ) |
14 |
5
|
nnne0d |
⊢ ( 𝜑 → 𝑁 ≠ 0 ) |
15 |
9 10 13 14
|
mulne0d |
⊢ ( 𝜑 → ( 2 · 𝑁 ) ≠ 0 ) |
16 |
3
|
nn0zd |
⊢ ( 𝜑 → 𝐽 ∈ ℤ ) |
17 |
16
|
znegcld |
⊢ ( 𝜑 → - 𝐽 ∈ ℤ ) |
18 |
11 15 17
|
expclzd |
⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ∈ ℂ ) |
19 |
9 10 15
|
mulne0bad |
⊢ ( 𝜑 → 2 ≠ 0 ) |
20 |
18 9 19
|
divcld |
⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ∈ ℂ ) |
21 |
4
|
zcnd |
⊢ ( 𝜑 → 𝑀 ∈ ℂ ) |
22 |
|
1cnd |
⊢ ( 𝜑 → 1 ∈ ℂ ) |
23 |
21 22
|
addcld |
⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℂ ) |
24 |
20 23 21
|
subdid |
⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( 𝑀 + 1 ) − 𝑀 ) ) = ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) ) |
25 |
24
|
eqcomd |
⊢ ( 𝜑 → ( ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) ) − ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( 𝑀 + 1 ) − 𝑀 ) ) ) |
26 |
21 22
|
pncan2d |
⊢ ( 𝜑 → ( ( 𝑀 + 1 ) − 𝑀 ) = 1 ) |
27 |
26
|
oveq2d |
⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( 𝑀 + 1 ) − 𝑀 ) ) = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 1 ) ) |
28 |
20
|
mulid1d |
⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 1 ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) |
29 |
27 28
|
eqtrd |
⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( 𝑀 + 1 ) − 𝑀 ) ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) |
30 |
8 25 29
|
3eqtrd |
⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) |