Metamath Proof Explorer

Theorem cnndvlem1

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

Ref Expression
Hypotheses cnndvlem1.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
cnndvlem1.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ 1 2 n ⁢ T ⁡ 2 ⋅ 3 n ⁢ y
cnndvlem1.w ⊢ W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
Assertion cnndvlem1 ⊢ W : ℝ ⟶cn ℝ ∧ dom ⁡ W ℝ ′ = ∅

Proof

Step Hyp Ref Expression
1 cnndvlem1.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 cnndvlem1.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ 1 2 n ⁢ T ⁡ 2 ⋅ 3 n ⁢ y
3 cnndvlem1.w ⊢ W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
4 3nn ⊢ 3 ∈ ℕ
5 4 a1i ⊢ ⊤ → 3 ∈ ℕ
6 neg1rr ⊢ − 1 ∈ ℝ
7 6 rexri ⊢ − 1 ∈ ℝ *
8 1re ⊢ 1 ∈ ℝ
9 8 rexri ⊢ 1 ∈ ℝ *
10 halfre ⊢ 1 2 ∈ ℝ
11 10 rexri ⊢ 1 2 ∈ ℝ *
12 7 9 11 3pm3.2i ⊢ − 1 ∈ ℝ * ∧ 1 ∈ ℝ * ∧ 1 2 ∈ ℝ *
13 neg1lt0 ⊢ − 1 < 0
14 halfgt0 ⊢ 0 < 1 2
15 13 14 pm3.2i ⊢ − 1 < 0 ∧ 0 < 1 2
16 0re ⊢ 0 ∈ ℝ
17 6 16 10 lttri ⊢ − 1 < 0 ∧ 0 < 1 2 → − 1 < 1 2
18 15 17 ax-mp ⊢ − 1 < 1 2
19 halflt1 ⊢ 1 2 < 1
20 18 19 pm3.2i ⊢ − 1 < 1 2 ∧ 1 2 < 1
21 12 20 pm3.2i ⊢ − 1 ∈ ℝ * ∧ 1 ∈ ℝ * ∧ 1 2 ∈ ℝ * ∧ − 1 < 1 2 ∧ 1 2 < 1
22 elioo3g ⊢ 1 2 ∈ − 1 1 ↔ − 1 ∈ ℝ * ∧ 1 ∈ ℝ * ∧ 1 2 ∈ ℝ * ∧ − 1 < 1 2 ∧ 1 2 < 1
23 21 22 mpbir ⊢ 1 2 ∈ − 1 1
24 23 a1i ⊢ ⊤ → 1 2 ∈ − 1 1
25 1 2 3 5 24 knoppcn2 ⊢ ⊤ → W : ℝ ⟶cn ℝ
26 25 mptru ⊢ W : ℝ ⟶cn ℝ
27 2cn ⊢ 2 ∈ ℂ
28 27 mulid2i ⊢ 1 ⋅ 2 = 2
29 2lt3 ⊢ 2 < 3
30 28 29 eqbrtri ⊢ 1 ⋅ 2 < 3
31 2pos ⊢ 0 < 2
32 4 nnrei ⊢ 3 ∈ ℝ
33 2re ⊢ 2 ∈ ℝ
34 8 32 33 ltmuldivi ⊢ 0 < 2 → 1 ⋅ 2 < 3 ↔ 1 < 3 2
35 31 34 ax-mp ⊢ 1 ⋅ 2 < 3 ↔ 1 < 3 2
36 30 35 mpbi ⊢ 1 < 3 2
37 16 10 14 ltleii ⊢ 0 ≤ 1 2
38 10 absidi ⊢ 0 ≤ 1 2 → 1 2 = 1 2
39 37 38 ax-mp ⊢ 1 2 = 1 2
40 39 oveq2i ⊢ 3 ⁢ 1 2 = 3 ⁢ 1 2
41 4 nncni ⊢ 3 ∈ ℂ
42 2ne0 ⊢ 2 ≠ 0
43 41 27 42 divreci ⊢ 3 2 = 3 ⁢ 1 2
44 43 eqcomi ⊢ 3 ⁢ 1 2 = 3 2
45 40 44 eqtri ⊢ 3 ⁢ 1 2 = 3 2
46 36 45 breqtrri ⊢ 1 < 3 ⁢ 1 2
47 46 a1i ⊢ ⊤ → 1 < 3 ⁢ 1 2
48 1 2 3 24 5 47 knoppndv ⊢ ⊤ → dom ⁡ W ℝ ′ = ∅
49 48 mptru ⊢ dom ⁡ W ℝ ′ = ∅
50 26 49 pm3.2i ⊢ W : ℝ ⟶cn ℝ ∧ dom ⁡ W ℝ ′ = ∅