Metamath Proof Explorer

Theorem knoppndvlem10

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

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

Proof

Step Hyp Ref Expression
1 knoppndvlem10.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 knoppndvlem10.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
3 knoppndvlem10.a ⊢ A = 2 ⋅ N − J 2 ⋅ M
4 knoppndvlem10.b ⊢ B = 2 ⋅ N − J 2 ⁢ M + 1
5 knoppndvlem10.c ⊢ φ → C ∈ − 1 1
6 knoppndvlem10.j ⊢ φ → J ∈ ℕ 0
7 knoppndvlem10.m ⊢ φ → M ∈ ℤ
8 knoppndvlem10.n ⊢ φ → N ∈ ℕ
9 5 adantr ⊢ φ ∧ 2 ∥ M → C ∈ − 1 1
10 6 adantr ⊢ φ ∧ 2 ∥ M → J ∈ ℕ 0
11 7 peano2zd ⊢ φ → M + 1 ∈ ℤ
12 11 adantr ⊢ φ ∧ 2 ∥ M → M + 1 ∈ ℤ
13 8 adantr ⊢ φ ∧ 2 ∥ M → N ∈ ℕ
14 notnot ⊢ 2 ∥ M → ¬ ¬ 2 ∥ M
15 14 adantl ⊢ φ ∧ 2 ∥ M → ¬ ¬ 2 ∥ M
16 7 adantr ⊢ φ ∧ 2 ∥ M → M ∈ ℤ
17 oddp1even ⊢ M ∈ ℤ → ¬ 2 ∥ M ↔ 2 ∥ M + 1
18 16 17 syl ⊢ φ ∧ 2 ∥ M → ¬ 2 ∥ M ↔ 2 ∥ M + 1
19 15 18 mtbid ⊢ φ ∧ 2 ∥ M → ¬ 2 ∥ M + 1
20 1 2 4 9 10 12 13 19 knoppndvlem9 ⊢ φ ∧ 2 ∥ M → F ⁡ B ⁡ J = C J 2
21 15 notnotrd ⊢ φ ∧ 2 ∥ M → 2 ∥ M
22 1 2 3 9 10 16 13 21 knoppndvlem8 ⊢ φ ∧ 2 ∥ M → F ⁡ A ⁡ J = 0
23 20 22 oveq12d ⊢ φ ∧ 2 ∥ M → F ⁡ B ⁡ J − F ⁡ A ⁡ J = C J 2 − 0
24 5 knoppndvlem3 ⊢ φ → C ∈ ℝ ∧ C < 1
25 24 simpld ⊢ φ → C ∈ ℝ
26 25 recnd ⊢ φ → C ∈ ℂ
27 26 6 expcld ⊢ φ → C J ∈ ℂ
28 2cnd ⊢ φ → 2 ∈ ℂ
29 2ne0 ⊢ 2 ≠ 0
30 29 a1i ⊢ φ → 2 ≠ 0
31 27 28 30 divcld ⊢ φ → C J 2 ∈ ℂ
32 31 subid1d ⊢ φ → C J 2 − 0 = C J 2
33 32 adantr ⊢ φ ∧ 2 ∥ M → C J 2 − 0 = C J 2
34 23 33 eqtrd ⊢ φ ∧ 2 ∥ M → F ⁡ B ⁡ J − F ⁡ A ⁡ J = C J 2
35 34 fveq2d ⊢ φ ∧ 2 ∥ M → F ⁡ B ⁡ J − F ⁡ A ⁡ J = C J 2
36 4 a1i ⊢ φ → B = 2 ⋅ N − J 2 ⁢ M + 1
37 6 nn0zd ⊢ φ → J ∈ ℤ
38 8 37 11 knoppndvlem1 ⊢ φ → 2 ⋅ N − J 2 ⁢ M + 1 ∈ ℝ
39 36 38 eqeltrd ⊢ φ → B ∈ ℝ
40 1 2 8 25 39 6 knoppcnlem3 ⊢ φ → F ⁡ B ⁡ J ∈ ℝ
41 40 recnd ⊢ φ → F ⁡ B ⁡ J ∈ ℂ
42 3 a1i ⊢ φ → A = 2 ⋅ N − J 2 ⋅ M
43 8 37 7 knoppndvlem1 ⊢ φ → 2 ⋅ N − J 2 ⋅ M ∈ ℝ
44 42 43 eqeltrd ⊢ φ → A ∈ ℝ
45 1 2 8 25 44 6 knoppcnlem3 ⊢ φ → F ⁡ A ⁡ J ∈ ℝ
46 45 recnd ⊢ φ → F ⁡ A ⁡ J ∈ ℂ
47 41 46 abssubd ⊢ φ → F ⁡ B ⁡ J − F ⁡ A ⁡ J = F ⁡ A ⁡ J − F ⁡ B ⁡ J
48 47 adantr ⊢ φ ∧ ¬ 2 ∥ M → F ⁡ B ⁡ J − F ⁡ A ⁡ J = F ⁡ A ⁡ J − F ⁡ B ⁡ J
49 5 adantr ⊢ φ ∧ ¬ 2 ∥ M → C ∈ − 1 1
50 6 adantr ⊢ φ ∧ ¬ 2 ∥ M → J ∈ ℕ 0
51 7 adantr ⊢ φ ∧ ¬ 2 ∥ M → M ∈ ℤ
52 8 adantr ⊢ φ ∧ ¬ 2 ∥ M → N ∈ ℕ
53 simpr ⊢ φ ∧ ¬ 2 ∥ M → ¬ 2 ∥ M
54 1 2 3 49 50 51 52 53 knoppndvlem9 ⊢ φ ∧ ¬ 2 ∥ M → F ⁡ A ⁡ J = C J 2
55 11 adantr ⊢ φ ∧ ¬ 2 ∥ M → M + 1 ∈ ℤ
56 51 17 syl ⊢ φ ∧ ¬ 2 ∥ M → ¬ 2 ∥ M ↔ 2 ∥ M + 1
57 53 56 mpbid ⊢ φ ∧ ¬ 2 ∥ M → 2 ∥ M + 1
58 1 2 4 49 50 55 52 57 knoppndvlem8 ⊢ φ ∧ ¬ 2 ∥ M → F ⁡ B ⁡ J = 0
59 54 58 oveq12d ⊢ φ ∧ ¬ 2 ∥ M → F ⁡ A ⁡ J − F ⁡ B ⁡ J = C J 2 − 0
60 32 adantr ⊢ φ ∧ ¬ 2 ∥ M → C J 2 − 0 = C J 2
61 59 60 eqtrd ⊢ φ ∧ ¬ 2 ∥ M → F ⁡ A ⁡ J − F ⁡ B ⁡ J = C J 2
62 61 fveq2d ⊢ φ ∧ ¬ 2 ∥ M → F ⁡ A ⁡ J − F ⁡ B ⁡ J = C J 2
63 48 62 eqtrd ⊢ φ ∧ ¬ 2 ∥ M → F ⁡ B ⁡ J − F ⁡ A ⁡ J = C J 2
64 35 63 pm2.61dan ⊢ φ → F ⁡ B ⁡ J − F ⁡ A ⁡ J = C J 2
65 27 28 30 absdivd ⊢ φ → C J 2 = C J 2
66 26 6 absexpd ⊢ φ → C J = C J
67 0le2 ⊢ 0 ≤ 2
68 2re ⊢ 2 ∈ ℝ
69 68 absidi ⊢ 0 ≤ 2 → 2 = 2
70 67 69 ax-mp ⊢ 2 = 2
71 70 a1i ⊢ φ → 2 = 2
72 66 71 oveq12d ⊢ φ → C J 2 = C J 2
73 65 72 eqtrd ⊢ φ → C J 2 = C J 2
74 64 73 eqtrd ⊢ φ → F ⁡ B ⁡ J − F ⁡ A ⁡ J = C J 2