Theorem cnndvlem2

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

	Ref	Expression
Hypotheses	cnndvlem2.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
	cnndvlem2.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 1 / 2 ) ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 3 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
	cnndvlem2.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
Assertion	cnndvlem2	⊢ ∃ 𝑓 ( 𝑓 ∈ ( ℝ –cn→ ℝ ) ∧ dom ( ℝ D 𝑓 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		cnndvlem2.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		cnndvlem2.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 1 / 2 ) ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 3 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		cnndvlem2.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4	1 2 3	cnndvlem1	⊢ ( 𝑊 ∈ ( ℝ –cn→ ℝ ) ∧ dom ( ℝ D 𝑊 ) = ∅ )
5		reex	⊢ ℝ ∈ V
6	5	mptex	⊢ ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) ) ∈ V
7	3 6	eqeltri	⊢ 𝑊 ∈ V
8		eleq1	⊢ ( 𝑓 = 𝑊 → ( 𝑓 ∈ ( ℝ –cn→ ℝ ) ↔ 𝑊 ∈ ( ℝ –cn→ ℝ ) ) )
9		oveq2	⊢ ( 𝑓 = 𝑊 → ( ℝ D 𝑓 ) = ( ℝ D 𝑊 ) )
10	9	dmeqd	⊢ ( 𝑓 = 𝑊 → dom ( ℝ D 𝑓 ) = dom ( ℝ D 𝑊 ) )
11	10	eqeq1d	⊢ ( 𝑓 = 𝑊 → ( dom ( ℝ D 𝑓 ) = ∅ ↔ dom ( ℝ D 𝑊 ) = ∅ ) )
12	8 11	anbi12d	⊢ ( 𝑓 = 𝑊 → ( ( 𝑓 ∈ ( ℝ –cn→ ℝ ) ∧ dom ( ℝ D 𝑓 ) = ∅ ) ↔ ( 𝑊 ∈ ( ℝ –cn→ ℝ ) ∧ dom ( ℝ D 𝑊 ) = ∅ ) ) )
13	7 12	spcev	⊢ ( ( 𝑊 ∈ ( ℝ –cn→ ℝ ) ∧ dom ( ℝ D 𝑊 ) = ∅ ) → ∃ 𝑓 ( 𝑓 ∈ ( ℝ –cn→ ℝ ) ∧ dom ( ℝ D 𝑓 ) = ∅ ) )
14	4 13	ax-mp	⊢ ∃ 𝑓 ( 𝑓 ∈ ( ℝ –cn→ ℝ ) ∧ dom ( ℝ D 𝑓 ) = ∅ )