Metamath Proof Explorer

Theorem knoppndvlem16

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

Ref Expression
Hypotheses knoppndvlem16.a ⊢ 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 )
knoppndvlem16.b ⊢ 𝐵 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( 𝑀 + 1 ) )
knoppndvlem16.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
knoppndvlem16.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
knoppndvlem16.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion knoppndvlem16 ( 𝜑 → ( 𝐵 − 𝐴 ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )

Proof

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 mulridd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 1 ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
29 27 28 eqtrd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · ( ( 𝑀 + 1 ) − 𝑀 ) ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )
30 8 25 29 3eqtrd ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) )