Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $n\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{n-1}$ be distinct set variables, and let $i,j,k<n$, not necessarily distinct. Each clause states that a condition on $x_{0},\dots,x_{n-1}$ is predicative: expressed by a predicative formula, with $x_{0},\dots,x_{n-1}$ in place of the variables $x_{1},\dots,x_{N}$ of Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables. Here $\mathbb{R}$, $\le$, $+$, $\cdot$, $0$ and $1$ are as in The Real Numbers (i), The Real Numbers (iii) and The Real Numbers (iv), and $<$ is the strict order associated with $\le$.

(i) Differences. "$x_{i}\in\mathbb{R}$, $x_{j}\in\mathbb{R}$ and $x_{k}=x_{i}-x_{j}$".

(ii) Quotients. "$x_{i},x_{j}\in\mathbb{R}$, $x_{j}\neq0$ and $x_{k}=x_{i}/x_{j}$".

(iii) Absolute values. "$x_{i}\in\mathbb{R}$ and $x_{k}=|x_{i}|$".

(iv) Distances. "$x_{i},x_{j}\in\mathbb{R}$ and $x_{k}=|x_{i}-x_{j}|$".

(v) The strict order. "$x_{i}<x_{j}$".

(vi) Positivity. "$0<x_{j}$".