| 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 36499 | . . 3
⊢ (𝜑 → seq0( ∘f
+ , (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) ∈ dom
(⇝𝑢‘ℝ)) | 
| 7 |  | seqex 14044 | . . . 4
⊢ seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) ∈ V | 
| 8 | 7 | eldm 5911 | . . 3
⊢ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) ∈ dom
(⇝𝑢‘ℝ) ↔ ∃𝑓seq0( ∘f + , (𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ
↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) | 
| 9 | 6, 8 | sylib 218 | . 2
⊢ (𝜑 → ∃𝑓seq0( ∘f + , (𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ
↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) | 
| 10 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) → seq0( ∘f + ,
(𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ ↦
((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) | 
| 11 |  | ulmcl 26424 | . . . . . . . 8
⊢ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓 → 𝑓:ℝ⟶ℂ) | 
| 12 | 11 | feqmptd 6977 | . . . . . . 7
⊢ (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓 → 𝑓 = (𝑤 ∈ ℝ ↦ (𝑓‘𝑤))) | 
| 13 | 12 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) → 𝑓 = (𝑤 ∈ ℝ ↦ (𝑓‘𝑤))) | 
| 14 |  | nn0uz 12920 | . . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) | 
| 15 |  | 0zd 12625 | . . . . . . . . 9
⊢ (((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → 0 ∈
ℤ) | 
| 16 |  | eqidd 2738 | . . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → ((𝐹‘𝑤)‘𝑖) = ((𝐹‘𝑤)‘𝑖)) | 
| 17 | 3 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → 𝑁 ∈
ℕ) | 
| 18 | 4 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → 𝐶 ∈
ℝ) | 
| 19 |  | simplr 769 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → 𝑤 ∈
ℝ) | 
| 20 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
ℕ0) | 
| 21 | 1, 2, 17, 18, 19, 20 | knoppcnlem3 36496 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → ((𝐹‘𝑤)‘𝑖) ∈ ℝ) | 
| 22 | 21 | adantllr 719 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → ((𝐹‘𝑤)‘𝑖) ∈ ℝ) | 
| 23 | 22 | recnd 11289 | . . . . . . . . 9
⊢ ((((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑖 ∈ ℕ0) → ((𝐹‘𝑤)‘𝑖) ∈ ℂ) | 
| 24 | 1, 2, 3, 4 | knoppcnlem8 36501 | . . . . . . . . . . 11
⊢ (𝜑 → seq0( ∘f
+ , (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))):ℕ0⟶(ℂ
↑m ℝ)) | 
| 25 | 24 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → seq0( ∘f +
, (𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ ↦
((𝐹‘𝑧)‘𝑚)))):ℕ0⟶(ℂ
↑m ℝ)) | 
| 26 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ) | 
| 27 |  | seqex 14044 | . . . . . . . . . . 11
⊢ seq0( + ,
(𝐹‘𝑤)) ∈ V | 
| 28 | 27 | a1i 11 | . . . . . . . . . 10
⊢ (((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → seq0( + , (𝐹‘𝑤)) ∈ V) | 
| 29 | 3 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → 𝑁 ∈
ℕ) | 
| 30 | 4 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈
ℝ) | 
| 31 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) | 
| 32 | 1, 2, 29, 30, 31 | knoppcnlem7 36500 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → (seq0(
∘f + , (𝑚
∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘) = (𝑣 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑣))‘𝑘))) | 
| 33 | 32 | adantllr 719 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → (seq0(
∘f + , (𝑚 ∈
ℕ0 ↦ (𝑧
∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘) = (𝑣 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑣))‘𝑘))) | 
| 34 | 33 | fveq1d 6908 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → ((seq0(
∘f + , (𝑚 ∈
ℕ0 ↦ (𝑧
∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)‘𝑤) = ((𝑣 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑣))‘𝑘))‘𝑤)) | 
| 35 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ (𝑣 ∈ ℝ ↦ (seq0( +
, (𝐹‘𝑣))‘𝑘)) = (𝑣 ∈ ℝ ↦ (seq0( + , (𝐹‘𝑣))‘𝑘)) | 
| 36 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑤 → (𝐹‘𝑣) = (𝐹‘𝑤)) | 
| 37 | 36 | seqeq3d 14050 | . . . . . . . . . . . . 13
⊢ (𝑣 = 𝑤 → seq0( + , (𝐹‘𝑣)) = seq0( + , (𝐹‘𝑤))) | 
| 38 | 37 | fveq1d 6908 | . . . . . . . . . . . 12
⊢ (𝑣 = 𝑤 → (seq0( + , (𝐹‘𝑣))‘𝑘) = (seq0( + , (𝐹‘𝑤))‘𝑘)) | 
| 39 | 26 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → 𝑤 ∈ ℝ) | 
| 40 |  | fvexd 6921 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → (seq0( + ,
(𝐹‘𝑤))‘𝑘) ∈ V) | 
| 41 | 35, 38, 39, 40 | fvmptd3 7039 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → ((𝑣 ∈ ℝ ↦ (seq0( + ,
(𝐹‘𝑣))‘𝑘))‘𝑤) = (seq0( + , (𝐹‘𝑤))‘𝑘)) | 
| 42 | 34, 41 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) ∧ 𝑘 ∈ ℕ0) → ((seq0(
∘f + , (𝑚 ∈
ℕ0 ↦ (𝑧
∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))‘𝑘)‘𝑤) = (seq0( + , (𝐹‘𝑤))‘𝑘)) | 
| 43 |  | simplr 769 | . . . . . . . . . 10
⊢ (((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → seq0( ∘f +
, (𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ ↦
((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) | 
| 44 | 14, 15, 25, 26, 28, 42, 43 | ulmclm 26430 | . . . . . . . . 9
⊢ (((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → seq0( + , (𝐹‘𝑤)) ⇝ (𝑓‘𝑤)) | 
| 45 | 14, 15, 16, 23, 44 | isumclim 15793 | . . . . . . . 8
⊢ (((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖) = (𝑓‘𝑤)) | 
| 46 | 45 | eqcomd 2743 | . . . . . . 7
⊢ (((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) ∧ 𝑤 ∈ ℝ) → (𝑓‘𝑤) = Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) | 
| 47 | 46 | mpteq2dva 5242 | . . . . . 6
⊢ ((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) → (𝑤 ∈ ℝ ↦ (𝑓‘𝑤)) = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))) | 
| 48 |  | knoppcnlem9.w | . . . . . . . 8
⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0
((𝐹‘𝑤)‘𝑖)) | 
| 49 | 48 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) → 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖))) | 
| 50 | 49 | eqcomd 2743 | . . . . . 6
⊢ ((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) → (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖)) = 𝑊) | 
| 51 | 13, 47, 50 | 3eqtrd 2781 | . . . . 5
⊢ ((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) → 𝑓 = 𝑊) | 
| 52 | 10, 51 | breqtrd 5169 | . . . 4
⊢ ((𝜑 ∧ seq0( ∘f +
, (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓) → seq0( ∘f + ,
(𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ ↦
((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑊) | 
| 53 | 52 | ex 412 | . . 3
⊢ (𝜑 → (seq0( ∘f
+ , (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓 → seq0( ∘f + ,
(𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ ↦
((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑊)) | 
| 54 | 53 | exlimdv 1933 | . 2
⊢ (𝜑 → (∃𝑓seq0( ∘f + , (𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ
↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑓 → seq0( ∘f + ,
(𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ ↦
((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑊)) | 
| 55 | 9, 54 | mpd 15 | 1
⊢ (𝜑 → seq0( ∘f
+ , (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))))(⇝𝑢‘ℝ)𝑊) |