dnicn

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

		Ref	Expression
	Hypothesis	dnicn.1	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
	Assertion	dnicn	$⊢ T : ℝ \underset{cn}{⟶} ℝ$

Proof

Step	Hyp	Ref	Expression
1		dnicn.1	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
2	1	dnif	$⊢ T : ℝ ⟶ ℝ$
3		simpr	$⊢ (y \in ℝ \land e \in ℝ^{+}) \to e \in ℝ^{+}$
4		simplr	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to z \in ℝ$
5	1 4	dnicld2	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to T (z) \in ℝ$
6		simplll	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to y \in ℝ$
7	1 6	dnicld2	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to T (y) \in ℝ$
8	5 7	resubcld	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to T (z) - T (y) \in ℝ$
9	8	recnd	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to T (z) - T (y) \in ℂ$
10	9	abscld	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to \|T (z) - T (y)\| \in ℝ$
11	4 6	resubcld	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to z - y \in ℝ$
12	11	recnd	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to z - y \in ℂ$
13	12	abscld	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to \|z - y\| \in ℝ$
14	3	ad2antrr	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to e \in ℝ^{+}$
15	14	rpred	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to e \in ℝ$
16	1 6 4	dnibnd	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to \|T (z) - T (y)\| \leq \|z - y\|$
17		simpr	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to \|z - y\| < e$
18	10 13 15 16 17	lelttrd	$⊢ (((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \land \|z - y\| < e) \to \|T (z) - T (y)\| < e$
19	18	ex	$⊢ ((y \in ℝ \land e \in ℝ^{+}) \land z \in ℝ) \to (\|z - y\| < e \to \|T (z) - T (y)\| < e)$
20	19	ralrimiva	$⊢ (y \in ℝ \land e \in ℝ^{+}) \to \forall z \in ℝ (\|z - y\| < e \to \|T (z) - T (y)\| < e)$
21		breq2	$⊢ d = e \to (\|z - y\| < d \leftrightarrow \|z - y\| < e)$
22	21	rspceaimv	$⊢ (e \in ℝ^{+} \land \forall z \in ℝ (\|z - y\| < e \to \|T (z) - T (y)\| < e)) \to \exists d \in ℝ^{+} \forall z \in ℝ (\|z - y\| < d \to \|T (z) - T (y)\| < e)$
23	3 20 22	syl2anc	$⊢ (y \in ℝ \land e \in ℝ^{+}) \to \exists d \in ℝ^{+} \forall z \in ℝ (\|z - y\| < d \to \|T (z) - T (y)\| < e)$
24	23	rgen2	$⊢ \forall y \in ℝ \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall z \in ℝ (\|z - y\| < d \to \|T (z) - T (y)\| < e)$
25		ax-resscn	$⊢ ℝ \subseteq ℂ$
26		elcncf2	$⊢ (ℝ \subseteq ℂ \land ℝ \subseteq ℂ) \to (T : ℝ \underset{cn}{⟶} ℝ \leftrightarrow (T : ℝ ⟶ ℝ \land \forall y \in ℝ \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall z \in ℝ (\|z - y\| < d \to \|T (z) - T (y)\| < e)))$
27	25 25 26	mp2an	$⊢ T : ℝ \underset{cn}{⟶} ℝ \leftrightarrow (T : ℝ ⟶ ℝ \land \forall y \in ℝ \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall z \in ℝ (\|z - y\| < d \to \|T (z) - T (y)\| < e))$
28	2 24 27	mpbir2an	$⊢ T : ℝ \underset{cn}{⟶} ℝ$

Metamath Proof Explorer

Theorem dnicn

Proof