Metamath Proof Explorer

Theorem knoppndvlem8

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

Ref Expression
Hypotheses knoppndvlem8.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
knoppndvlem8.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
knoppndvlem8.a ⊢ A = 2 ⋅ N − J 2 ⋅ M
knoppndvlem8.c ⊢ φ → C ∈ − 1 1
knoppndvlem8.j ⊢ φ → J ∈ ℕ 0
knoppndvlem8.m ⊢ φ → M ∈ ℤ
knoppndvlem8.n ⊢ φ → N ∈ ℕ
knoppndvlem8.1 ⊢ φ → 2 ∥ M
Assertion knoppndvlem8 ⊢ φ → F ⁡ A ⁡ J = 0

Proof

Step Hyp Ref Expression
1 knoppndvlem8.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 knoppndvlem8.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
3 knoppndvlem8.a ⊢ A = 2 ⋅ N − J 2 ⋅ M
4 knoppndvlem8.c ⊢ φ → C ∈ − 1 1
5 knoppndvlem8.j ⊢ φ → J ∈ ℕ 0
6 knoppndvlem8.m ⊢ φ → M ∈ ℤ
7 knoppndvlem8.n ⊢ φ → N ∈ ℕ
8 knoppndvlem8.1 ⊢ φ → 2 ∥ M
9 1 2 3 5 6 7 knoppndvlem7 ⊢ φ → F ⁡ A ⁡ J = C J ⁢ T ⁡ M 2
10 2z ⊢ 2 ∈ ℤ
11 10 a1i ⊢ φ → 2 ∈ ℤ
12 2ne0 ⊢ 2 ≠ 0
13 12 a1i ⊢ φ → 2 ≠ 0
14 11 13 6 3jca ⊢ φ → 2 ∈ ℤ ∧ 2 ≠ 0 ∧ M ∈ ℤ
15 dvdsval2 ⊢ 2 ∈ ℤ ∧ 2 ≠ 0 ∧ M ∈ ℤ → 2 ∥ M ↔ M 2 ∈ ℤ
16 14 15 syl ⊢ φ → 2 ∥ M ↔ M 2 ∈ ℤ
17 8 16 mpbid ⊢ φ → M 2 ∈ ℤ
18 1 17 dnizeq0 ⊢ φ → T ⁡ M 2 = 0
19 18 oveq2d ⊢ φ → C J ⁢ T ⁡ M 2 = C J ⋅ 0
20 4 knoppndvlem3 ⊢ φ → C ∈ ℝ ∧ C < 1
21 20 simpld ⊢ φ → C ∈ ℝ
22 21 recnd ⊢ φ → C ∈ ℂ
23 22 5 expcld ⊢ φ → C J ∈ ℂ
24 23 mul01d ⊢ φ → C J ⋅ 0 = 0
25 9 19 24 3eqtrd ⊢ φ → F ⁡ A ⁡ J = 0