Metamath Proof Explorer

Theorem dnicn

Description: The "distance to nearest integer" function is continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021)

Ref Expression
Hypothesis dnicn.1 ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
Assertion dnicn 𝑇 ∈ ( ℝ –cn→ ℝ )

Proof

Step Hyp Ref Expression
1 dnicn.1 ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 1 dnif ⊢ 𝑇 : ℝ ⟶ ℝ
3 simpr ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) → 𝑒 ∈ ℝ+ )
4 simplr ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → 𝑧 ∈ ℝ )
5 1 4 dnicld2 ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → ( 𝑇 ‘ 𝑧 ) ∈ ℝ )
6 simplll ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → 𝑦 ∈ ℝ )
7 1 6 dnicld2 ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → ( 𝑇 ‘ 𝑦 ) ∈ ℝ )
8 5 7 resubcld ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
9 8 recnd ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 𝑦 ) ) ∈ ℂ )
10 9 abscld ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 𝑦 ) ) ) ∈ ℝ )
11 4 6 resubcld ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → ( 𝑧 − 𝑦 ) ∈ ℝ )
12 11 recnd ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → ( 𝑧 − 𝑦 ) ∈ ℂ )
13 12 abscld ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → ( abs ‘ ( 𝑧 − 𝑦 ) ) ∈ ℝ )
14 3 ad2antrr ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → 𝑒 ∈ ℝ+ )
15 14 rpred ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → 𝑒 ∈ ℝ )
16 1 6 4 dnibnd ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 𝑦 ) ) ) ≤ ( abs ‘ ( 𝑧 − 𝑦 ) ) )
17 simpr ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 )
18 10 13 15 16 17 lelttrd ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 𝑦 ) ) ) < 𝑒 )
19 18 ex ⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ ) → ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 𝑦 ) ) ) < 𝑒 ) )
20 19 ralrimiva ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) → ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 𝑦 ) ) ) < 𝑒 ) )
21 breq2 ⊢ ( 𝑑 = 𝑒 → ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ↔ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) )
22 21 rspceaimv ⊢ ( ( 𝑒 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 𝑦 ) ) ) < 𝑒 ) ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 𝑦 ) ) ) < 𝑒 ) )
23 3 20 22 syl2anc ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 𝑦 ) ) ) < 𝑒 ) )
24 23 rgen2 ⊢ ∀ 𝑦 ∈ ℝ ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 𝑦 ) ) ) < 𝑒 )
25 ax-resscn ⊢ ℝ ⊆ ℂ
26 elcncf2 ⊢ ( ( ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝑇 ∈ ( ℝ –cn→ ℝ ) ↔ ( 𝑇 : ℝ ⟶ ℝ ∧ ∀ 𝑦 ∈ ℝ ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 𝑦 ) ) ) < 𝑒 ) ) ) )
27 25 25 26 mp2an ⊢ ( 𝑇 ∈ ( ℝ –cn→ ℝ ) ↔ ( 𝑇 : ℝ ⟶ ℝ ∧ ∀ 𝑦 ∈ ℝ ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 𝑦 ) ) ) < 𝑒 ) ) )
28 2 24 27 mpbir2an ⊢ 𝑇 ∈ ( ℝ –cn→ ℝ )