Metamath Proof Explorer

Theorem knoppndvlem17

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

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

Proof

Step Hyp Ref Expression
1 knoppndvlem17.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 knoppndvlem17.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
3 knoppndvlem17.w ⊢ W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
4 knoppndvlem17.a ⊢ A = 2 ⋅ N − J 2 ⋅ M
5 knoppndvlem17.b ⊢ B = 2 ⋅ N − J 2 ⁢ M + 1
6 knoppndvlem17.c ⊢ φ → C ∈ − 1 1
7 knoppndvlem17.j ⊢ φ → J ∈ ℕ 0
8 knoppndvlem17.m ⊢ φ → M ∈ ℤ
9 knoppndvlem17.n ⊢ φ → N ∈ ℕ
10 knoppndvlem17.1 ⊢ φ → 1 < N ⁢ C
11 6 knoppndvlem3 ⊢ φ → C ∈ ℝ ∧ C < 1
12 11 simpld ⊢ φ → C ∈ ℝ
13 12 recnd ⊢ φ → C ∈ ℂ
14 13 abscld ⊢ φ → C ∈ ℝ
15 14 7 reexpcld ⊢ φ → C J ∈ ℝ
16 2re ⊢ 2 ∈ ℝ
17 16 a1i ⊢ φ → 2 ∈ ℝ
18 2ne0 ⊢ 2 ≠ 0
19 18 a1i ⊢ φ → 2 ≠ 0
20 15 17 19 redivcld ⊢ φ → C J 2 ∈ ℝ
21 20 recnd ⊢ φ → C J 2 ∈ ℂ
22 1red ⊢ φ → 1 ∈ ℝ
23 9 nnred ⊢ φ → N ∈ ℝ
24 17 23 remulcld ⊢ φ → 2 ⋅ N ∈ ℝ
25 24 14 remulcld ⊢ φ → 2 ⋅ N ⁢ C ∈ ℝ
26 25 22 resubcld ⊢ φ → 2 ⋅ N ⁢ C − 1 ∈ ℝ
27 0red ⊢ φ → 0 ∈ ℝ
28 0lt1 ⊢ 0 < 1
29 28 a1i ⊢ φ → 0 < 1
30 6 9 10 knoppndvlem12 ⊢ φ → 2 ⋅ N ⁢ C ≠ 1 ∧ 1 < 2 ⋅ N ⁢ C − 1
31 30 simprd ⊢ φ → 1 < 2 ⋅ N ⁢ C − 1
32 27 22 26 29 31 lttrd ⊢ φ → 0 < 2 ⋅ N ⁢ C − 1
33 26 32 jca ⊢ φ → 2 ⋅ N ⁢ C − 1 ∈ ℝ ∧ 0 < 2 ⋅ N ⁢ C − 1
34 gt0ne0 ⊢ 2 ⋅ N ⁢ C − 1 ∈ ℝ ∧ 0 < 2 ⋅ N ⁢ C − 1 → 2 ⋅ N ⁢ C − 1 ≠ 0
35 33 34 syl ⊢ φ → 2 ⋅ N ⁢ C − 1 ≠ 0
36 22 26 35 redivcld ⊢ φ → 1 2 ⋅ N ⁢ C − 1 ∈ ℝ
37 22 36 resubcld ⊢ φ → 1 − 1 2 ⋅ N ⁢ C − 1 ∈ ℝ
38 37 recnd ⊢ φ → 1 − 1 2 ⋅ N ⁢ C − 1 ∈ ℂ
39 21 38 mulcomd ⊢ φ → C J 2 ⁢ 1 − 1 2 ⋅ N ⁢ C − 1 = 1 − 1 2 ⋅ N ⁢ C − 1 ⁢ C J 2
40 39 oveq1d ⊢ φ → C J 2 ⁢ 1 − 1 2 ⋅ N ⁢ C − 1 2 ⋅ N − J 2 = 1 − 1 2 ⋅ N ⁢ C − 1 ⁢ C J 2 2 ⋅ N − J 2
41 2rp ⊢ 2 ∈ ℝ +
42 41 a1i ⊢ φ → 2 ∈ ℝ +
43 9 nnrpd ⊢ φ → N ∈ ℝ +
44 42 43 rpmulcld ⊢ φ → 2 ⋅ N ∈ ℝ +
45 7 nn0zd ⊢ φ → J ∈ ℤ
46 45 znegcld ⊢ φ → − J ∈ ℤ
47 44 46 rpexpcld ⊢ φ → 2 ⋅ N − J ∈ ℝ +
48 47 rphalfcld ⊢ φ → 2 ⋅ N − J 2 ∈ ℝ +
49 48 rpcnd ⊢ φ → 2 ⋅ N − J 2 ∈ ℂ
50 48 rpne0d ⊢ φ → 2 ⋅ N − J 2 ≠ 0
51 38 21 49 50 divassd ⊢ φ → 1 − 1 2 ⋅ N ⁢ C − 1 ⁢ C J 2 2 ⋅ N − J 2 = 1 − 1 2 ⋅ N ⁢ C − 1 ⁢ C J 2 2 ⋅ N − J 2
52 21 49 50 divcld ⊢ φ → C J 2 2 ⋅ N − J 2 ∈ ℂ
53 38 52 mulcomd ⊢ φ → 1 − 1 2 ⋅ N ⁢ C − 1 ⁢ C J 2 2 ⋅ N − J 2 = C J 2 2 ⋅ N − J 2 ⁢ 1 − 1 2 ⋅ N ⁢ C − 1
54 15 recnd ⊢ φ → C J ∈ ℂ
55 47 rpcnd ⊢ φ → 2 ⋅ N − J ∈ ℂ
56 17 recnd ⊢ φ → 2 ∈ ℂ
57 47 rpne0d ⊢ φ → 2 ⋅ N − J ≠ 0
58 54 55 56 57 19 divcan7d ⊢ φ → C J 2 2 ⋅ N − J 2 = C J 2 ⋅ N − J
59 24 recnd ⊢ φ → 2 ⋅ N ∈ ℂ
60 44 rpne0d ⊢ φ → 2 ⋅ N ≠ 0
61 59 60 45 expnegd ⊢ φ → 2 ⋅ N − J = 1 2 ⋅ N J
62 61 oveq2d ⊢ φ → C J 2 ⋅ N − J = C J 1 2 ⋅ N J
63 1cnd ⊢ φ → 1 ∈ ℂ
64 59 7 expcld ⊢ φ → 2 ⋅ N J ∈ ℂ
65 27 29 gtned ⊢ φ → 1 ≠ 0
66 59 60 45 expne0d ⊢ φ → 2 ⋅ N J ≠ 0
67 54 63 64 65 66 divdiv2d ⊢ φ → C J 1 2 ⋅ N J = C J ⁢ 2 ⋅ N J 1
68 54 64 mulcld ⊢ φ → C J ⁢ 2 ⋅ N J ∈ ℂ
69 68 div1d ⊢ φ → C J ⁢ 2 ⋅ N J 1 = C J ⁢ 2 ⋅ N J
70 54 64 mulcomd ⊢ φ → C J ⁢ 2 ⋅ N J = 2 ⋅ N J ⁢ C J
71 59 60 jca ⊢ φ → 2 ⋅ N ∈ ℂ ∧ 2 ⋅ N ≠ 0
72 14 recnd ⊢ φ → C ∈ ℂ
73 6 9 10 knoppndvlem13 ⊢ φ → C ≠ 0
74 13 73 absne0d ⊢ φ → C ≠ 0
75 72 74 jca ⊢ φ → C ∈ ℂ ∧ C ≠ 0
76 71 75 45 3jca ⊢ φ → 2 ⋅ N ∈ ℂ ∧ 2 ⋅ N ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 ∧ J ∈ ℤ
77 mulexpz ⊢ 2 ⋅ N ∈ ℂ ∧ 2 ⋅ N ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 ∧ J ∈ ℤ → 2 ⋅ N ⁢ C J = 2 ⋅ N J ⁢ C J
78 76 77 syl ⊢ φ → 2 ⋅ N ⁢ C J = 2 ⋅ N J ⁢ C J
79 78 eqcomd ⊢ φ → 2 ⋅ N J ⁢ C J = 2 ⋅ N ⁢ C J
80 69 70 79 3eqtrd ⊢ φ → C J ⁢ 2 ⋅ N J 1 = 2 ⋅ N ⁢ C J
81 62 67 80 3eqtrd ⊢ φ → C J 2 ⋅ N − J = 2 ⋅ N ⁢ C J
82 58 81 eqtrd ⊢ φ → C J 2 2 ⋅ N − J 2 = 2 ⋅ N ⁢ C J
83 82 oveq1d ⊢ φ → C J 2 2 ⋅ N − J 2 ⁢ 1 − 1 2 ⋅ N ⁢ C − 1 = 2 ⋅ N ⁢ C J ⁢ 1 − 1 2 ⋅ N ⁢ C − 1
84 53 83 eqtrd ⊢ φ → 1 − 1 2 ⋅ N ⁢ C − 1 ⁢ C J 2 2 ⋅ N − J 2 = 2 ⋅ N ⁢ C J ⁢ 1 − 1 2 ⋅ N ⁢ C − 1
85 40 51 84 3eqtrd ⊢ φ → C J 2 ⁢ 1 − 1 2 ⋅ N ⁢ C − 1 2 ⋅ N − J 2 = 2 ⋅ N ⁢ C J ⁢ 1 − 1 2 ⋅ N ⁢ C − 1
86 85 eqcomd ⊢ φ → 2 ⋅ N ⁢ C J ⁢ 1 − 1 2 ⋅ N ⁢ C − 1 = C J 2 ⁢ 1 − 1 2 ⋅ N ⁢ C − 1 2 ⋅ N − J 2
87 20 37 remulcld ⊢ φ → C J 2 ⁢ 1 − 1 2 ⋅ N ⁢ C − 1 ∈ ℝ
88 5 a1i ⊢ φ → B = 2 ⋅ N − J 2 ⁢ M + 1
89 8 peano2zd ⊢ φ → M + 1 ∈ ℤ
90 9 45 89 knoppndvlem1 ⊢ φ → 2 ⋅ N − J 2 ⁢ M + 1 ∈ ℝ
91 88 90 eqeltrd ⊢ φ → B ∈ ℝ
92 11 simprd ⊢ φ → C < 1
93 1 2 3 91 9 12 92 knoppcld ⊢ φ → W ⁡ B ∈ ℂ
94 4 a1i ⊢ φ → A = 2 ⋅ N − J 2 ⋅ M
95 9 45 8 knoppndvlem1 ⊢ φ → 2 ⋅ N − J 2 ⋅ M ∈ ℝ
96 94 95 eqeltrd ⊢ φ → A ∈ ℝ
97 1 2 3 96 9 12 92 knoppcld ⊢ φ → W ⁡ A ∈ ℂ
98 93 97 subcld ⊢ φ → W ⁡ B − W ⁡ A ∈ ℂ
99 98 abscld ⊢ φ → W ⁡ B − W ⁡ A ∈ ℝ
100 1 2 3 4 5 6 7 8 9 10 knoppndvlem15 ⊢ φ → C J 2 ⁢ 1 − 1 2 ⋅ N ⁢ C − 1 ≤ W ⁡ B − W ⁡ A
101 87 99 48 100 lediv1dd ⊢ φ → C J 2 ⁢ 1 − 1 2 ⋅ N ⁢ C − 1 2 ⋅ N − J 2 ≤ W ⁡ B − W ⁡ A 2 ⋅ N − J 2
102 86 101 eqbrtrd ⊢ φ → 2 ⋅ N ⁢ C J ⁢ 1 − 1 2 ⋅ N ⁢ C − 1 ≤ W ⁡ B − W ⁡ A 2 ⋅ N − J 2
103 4 5 7 8 9 knoppndvlem16 ⊢ φ → B − A = 2 ⋅ N − J 2
104 103 eqcomd ⊢ φ → 2 ⋅ N − J 2 = B − A
105 104 oveq2d ⊢ φ → W ⁡ B − W ⁡ A 2 ⋅ N − J 2 = W ⁡ B − W ⁡ A B − A
106 102 105 breqtrd ⊢ φ → 2 ⋅ N ⁢ C J ⁢ 1 − 1 2 ⋅ N ⁢ C − 1 ≤ W ⁡ B − W ⁡ A B − A