Metamath Proof Explorer

Theorem knoppndvlem22

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

Ref Expression
Hypotheses knoppndvlem22.t ⊢T=x∈ℝ⟼x+12−x
knoppndvlem22.f ⊢F=y∈ℝ⟼n∈ℕ0⟼Cn⁢T⁡2⋅ Nn⁢y
knoppndvlem22.w ⊢W=w∈ℝ⟼∑i∈ℕ0F⁡w⁡i
knoppndvlem22.c ⊢φ→C∈−11
knoppndvlem22.d ⊢φ→D∈ℝ+
knoppndvlem22.e ⊢φ→E∈ℝ+
knoppndvlem22.h ⊢φ→H∈ℝ
knoppndvlem22.n ⊢φ→N∈ℕ
knoppndvlem22.1 ⊢φ→1<N⁢C
Assertion knoppndvlem22 ⊢φ→∃a∈ℝ∃b∈ℝa≤H∧H≤b∧b−a<D∧a≠b∧E≤W⁡b−W⁡ab−a

Proof

Step Hyp Ref Expression
1 knoppndvlem22.t ⊢T=x∈ℝ⟼x+12−x
2 knoppndvlem22.f ⊢F=y∈ℝ⟼n∈ℕ0⟼Cn⁢T⁡2⋅ Nn⁢y
3 knoppndvlem22.w ⊢W=w∈ℝ⟼∑i∈ℕ0F⁡w⁡i
4 knoppndvlem22.c ⊢φ→C∈−11
5 knoppndvlem22.d ⊢φ→D∈ℝ+
6 knoppndvlem22.e ⊢φ→E∈ℝ+
7 knoppndvlem22.h ⊢φ→H∈ℝ
8 knoppndvlem22.n ⊢φ→N∈ℕ
9 knoppndvlem22.1 ⊢φ→1<N⁢C
10 4 8 9 knoppndvlem20 ⊢φ→1−12⋅ N⁢C−1∈ℝ+
11 4 8 5 6 10 9 knoppndvlem18 ⊢φ→∃j∈ℕ02⋅ N−j2<D∧E≤2⋅ N⁢Cj⁢1−12⋅ N⁢C−1
12 eqid ⊢1−12⋅ N⁢C−1=1−12⋅ N⁢C−1
13 4 adantr ⊢φ∧j∈ℕ0∧2⋅ N−j2<D∧E≤2⋅ N⁢Cj⁢1−12⋅ N⁢C−1→C∈−11
14 5 adantr ⊢φ∧j∈ℕ0∧2⋅ N−j2<D∧E≤2⋅ N⁢Cj⁢1−12⋅ N⁢C−1→D∈ℝ+
15 6 adantr ⊢φ∧j∈ℕ0∧2⋅ N−j2<D∧E≤2⋅ N⁢Cj⁢1−12⋅ N⁢C−1→E∈ℝ+
16 7 adantr ⊢φ∧j∈ℕ0∧2⋅ N−j2<D∧E≤2⋅ N⁢Cj⁢1−12⋅ N⁢C−1→H∈ℝ
17 simprl ⊢φ∧j∈ℕ0∧2⋅ N−j2<D∧E≤2⋅ N⁢Cj⁢1−12⋅ N⁢C−1→j∈ℕ0
18 8 adantr ⊢φ∧j∈ℕ0∧2⋅ N−j2<D∧E≤2⋅ N⁢Cj⁢1−12⋅ N⁢C−1→N∈ℕ
19 9 adantr ⊢φ∧j∈ℕ0∧2⋅ N−j2<D∧E≤2⋅ N⁢Cj⁢1−12⋅ N⁢C−1→1<N⁢C
20 simprrl ⊢φ∧j∈ℕ0∧2⋅ N−j2<D∧E≤2⋅ N⁢Cj⁢1−12⋅ N⁢C−1→2⋅ N−j2<D
21 simprrr ⊢φ∧j∈ℕ0∧2⋅ N−j2<D∧E≤2⋅ N⁢Cj⁢1−12⋅ N⁢C−1→E≤2⋅ N⁢Cj⁢1−12⋅ N⁢C−1
22 1 2 3 12 13 14 15 16 17 18 19 20 21 knoppndvlem21 ⊢φ∧j∈ℕ0∧2⋅ N−j2<D∧E≤2⋅ N⁢Cj⁢1−12⋅ N⁢C−1→∃a∈ℝ∃b∈ℝa≤H∧H≤b∧b−a<D∧a≠b∧E≤W⁡b−W⁡ab−a
23 11 22 rexlimddv ⊢φ→∃a∈ℝ∃b∈ℝa≤H∧H≤b∧b−a<D∧a≠b∧E≤W⁡b−W⁡ab−a