Metamath Proof Explorer

Theorem knoppndvlem22

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

Ref Expression
Hypotheses knoppndvlem22.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
knoppndvlem22.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
knoppndvlem22.w ⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
knoppndvlem22.c ⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
knoppndvlem22.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
knoppndvlem22.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
knoppndvlem22.h ⊢ ( 𝜑 → 𝐻 ∈ ℝ )
knoppndvlem22.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
knoppndvlem22.1 ⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
Assertion knoppndvlem22 ( 𝜑 → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( ( 𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏 ) ∧ ( ( 𝑏 − 𝑎 ) < 𝐷 ∧ 𝑎 ≠ 𝑏 ) ∧ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) ) )

Proof

Step Hyp Ref Expression
1 knoppndvlem22.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 knoppndvlem22.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3 knoppndvlem22.w ⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4 knoppndvlem22.c ⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
5 knoppndvlem22.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
6 knoppndvlem22.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
7 knoppndvlem22.h ⊢ ( 𝜑 → 𝐻 ∈ ℝ )
8 knoppndvlem22.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9 knoppndvlem22.1 ⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
10 4 8 9 knoppndvlem20 ⊢ ( 𝜑 → ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ∈ ℝ+ )
11 4 8 5 6 10 9 knoppndvlem18 ⊢ ( 𝜑 → ∃ 𝑗 ∈ ℕ0 ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ) )
12 eqid ⊢ ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) = ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) )
13 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ) ) ) → 𝐶 ∈ ( - 1 (,) 1 ) )
14 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ) ) ) → 𝐷 ∈ ℝ+ )
15 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ) ) ) → 𝐸 ∈ ℝ+ )
16 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ) ) ) → 𝐻 ∈ ℝ )
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ) ) ) → 𝑗 ∈ ℕ0 )
18 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ) ) ) → 𝑁 ∈ ℕ )
19 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ) ) ) → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
20 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ) ) ) → ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 )
21 simprrr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ) ) ) → 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) )
22 1 2 3 12 13 14 15 16 17 18 19 20 21 knoppndvlem21 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℕ0 ∧ ( ( ( ( 2 · 𝑁 ) ↑ - 𝑗 ) / 2 ) < 𝐷 ∧ 𝐸 ≤ ( ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) ↑ 𝑗 ) · ( 1 − ( 1 / ( ( ( 2 · 𝑁 ) · ( abs ‘ 𝐶 ) ) − 1 ) ) ) ) ) ) ) → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( ( 𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏 ) ∧ ( ( 𝑏 − 𝑎 ) < 𝐷 ∧ 𝑎 ≠ 𝑏 ) ∧ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) ) )
23 11 22 rexlimddv ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( ( 𝑎 ≤ 𝐻 ∧ 𝐻 ≤ 𝑏 ) ∧ ( ( 𝑏 − 𝑎 ) < 𝐷 ∧ 𝑎 ≠ 𝑏 ) ∧ 𝐸 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) ) )