Step | Hyp | Ref
| Expression |
1 | | knoppcnlem9.t |
. . . 4
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) |
2 | | knoppcnlem9.f |
. . . 4
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) |
3 | | knoppcnlem9.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
4 | | knoppcnlem9.1 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℝ) |
5 | | knoppcnlem9.2 |
. . . 4
⊢ (𝜑 → (abs‘𝐶) < 1) |
6 | 1, 2, 3, 4, 5 | knoppcnlem6 31658 |
. . 3
⊢ (𝜑 → seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) ∈ dom
(⇝𝑢‘ℝ)) |
7 | | seqex 12665 |
. . . 4
⊢ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) ∈ V |
8 | 7 | eldm 5243 |
. . 3
⊢ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) ∈ dom
(⇝𝑢‘ℝ) ↔ ∃𝑓seq0( ∘𝑓 + , (𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ
↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) |
9 | 6, 8 | sylib 207 |
. 2
⊢ (𝜑 → ∃𝑓seq0( ∘𝑓 + , (𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ
↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) |
10 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) → seq0(
∘𝑓 + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) |
11 | | ulmcl 23939 |
. . . . . . . 8
⊢ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓 → 𝑓:ℝ⟶ℂ) |
12 | 11 | feqmptd 6159 |
. . . . . . 7
⊢ (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓 → 𝑓 = (𝑤 ∈ ℝ ↦ (𝑓‘𝑤))) |
13 | 12 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) → 𝑓 = (𝑤 ∈ ℝ ↦ (𝑓‘𝑤))) |
14 | | nn0uz 11598 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
15 | | 0zd 11266 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → 0 ∈
ℤ) |
16 | | eqidd 2611 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → ((𝐹‘𝑤)‘𝑖) = ((𝐹‘𝑤)‘𝑖)) |
17 | 3 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → 𝑁 ∈
ℕ) |
18 | 4 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → 𝐶 ∈
ℝ) |
19 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → 𝑤 ∈
ℝ) |
20 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
ℕ0) |
21 | 1, 2, 17, 18, 19, 20 | knoppcnlem3 31655 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → ((𝐹‘𝑤)‘𝑖) ∈ ℝ) |
22 | 21 | adantllr 751 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → ((𝐹‘𝑤)‘𝑖) ∈ ℝ) |
23 | 22 | recnd 9947 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → ((𝐹‘𝑤)‘𝑖) ∈ ℂ) |
24 | 1, 2, 3, 4 | knoppcnlem8 31660 |
. . . . . . . . . . 11
⊢ (𝜑 → seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))):ℕ0⟶(ℂ
↑𝑚 ℝ)) |
25 | 24 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → seq0(
∘𝑓 + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))):ℕ0⟶(ℂ
↑𝑚 ℝ)) |
26 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ) |
27 | | seqex 12665 |
. . . . . . . . . . 11
⊢ seq0( + ,
(𝐹‘𝑤)) ∈ V |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → seq0( + , (𝐹‘𝑤)) ∈ V) |
29 | 3 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → 𝑁 ∈
ℕ) |
30 | 4 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈
ℝ) |
31 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
32 | 1, 2, 29, 30, 31 | knoppcnlem7 31659 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘) = (𝑣 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑣))‘𝑘))) |
33 | 32 | adantllr 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → (seq0(
∘𝑓 + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘) = (𝑣 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑣))‘𝑘))) |
34 | 33 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → ((seq0(
∘𝑓 + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)‘𝑤) = ((𝑣 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑣))‘𝑘))‘𝑤)) |
35 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ℝ ↦ (seq0( +
, (𝐹‘𝑣))‘𝑘)) = (𝑣 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑣))‘𝑘)) |
36 | 35 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → (𝑣 ∈ ℝ ↦ (seq0( + ,
(𝐹‘𝑣))‘𝑘)) = (𝑣 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑣))‘𝑘))) |
37 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑤 → (𝐹‘𝑣) = (𝐹‘𝑤)) |
38 | 37 | seqeq3d 12671 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑤 → seq0( + , (𝐹‘𝑣)) = seq0( + , (𝐹‘𝑤))) |
39 | 38 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑤 → (seq0( + , (𝐹‘𝑣))‘𝑘) = (seq0( + , (𝐹‘𝑤))‘𝑘)) |
40 | 39 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) ∧ 𝑣 = 𝑤) → (seq0( + , (𝐹‘𝑣))‘𝑘) = (seq0( + , (𝐹‘𝑤))‘𝑘)) |
41 | 26 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → 𝑤 ∈ ℝ) |
42 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (seq0( +
, (𝐹‘𝑤))‘𝑘) ∈ V |
43 | 42 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → (seq0( + ,
(𝐹‘𝑤))‘𝑘) ∈ V) |
44 | 36, 40, 41, 43 | fvmptd 6197 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → ((𝑣 ∈ ℝ ↦ (seq0( + ,
(𝐹‘𝑣))‘𝑘))‘𝑤) = (seq0( + , (𝐹‘𝑤))‘𝑘)) |
45 | 34, 44 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → ((seq0(
∘𝑓 + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)‘𝑤) = (seq0( + , (𝐹‘𝑤))‘𝑘)) |
46 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → seq0(
∘𝑓 + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) |
47 | 14, 15, 25, 26, 28, 45, 46 | ulmclm 23945 |
. . . . . . . . 9
⊢ (((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → seq0( + , (𝐹‘𝑤)) ⇝ (𝑓‘𝑤)) |
48 | 14, 15, 16, 23, 47 | isumclim 14330 |
. . . . . . . 8
⊢ (((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖) = (𝑓‘𝑤)) |
49 | 48 | eqcomd 2616 |
. . . . . . 7
⊢ (((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → (𝑓‘𝑤) = Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) |
50 | 49 | mpteq2dva 4672 |
. . . . . 6
⊢ ((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) → (𝑤 ∈ ℝ ↦ (𝑓‘𝑤)) = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))) |
51 | | knoppcnlem9.w |
. . . . . . . 8
⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0
((𝐹‘𝑤)‘𝑖)) |
52 | 51 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) → 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))) |
53 | 52 | eqcomd 2616 |
. . . . . 6
⊢ ((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) → (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) = 𝑊) |
54 | 13, 50, 53 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) → 𝑓 = 𝑊) |
55 | 10, 54 | breqtrd 4609 |
. . . 4
⊢ ((𝜑 ∧ seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) → seq0(
∘𝑓 + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑊) |
56 | 55 | ex 449 |
. . 3
⊢ (𝜑 → (seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓 → seq0(
∘𝑓 + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑊)) |
57 | 56 | exlimdv 1848 |
. 2
⊢ (𝜑 → (∃𝑓seq0( ∘𝑓 + , (𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ
↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓 → seq0(
∘𝑓 + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑊)) |
58 | 9, 57 | mpd 15 |
1
⊢ (𝜑 → seq0(
∘𝑓 + , (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑊) |