Predicative Formulas for the Derivative Condition and for Powers

In the setting of The Real Line: Standing Notation and Background for Calculus on Intervals, with predicative meant for formulas with abbreviations, conditions expressed by a predicative formula are as in Conditions Expressed by a Predicative Formula, and Guards (ii) and guards as in Conditions Expressed by a Predicative Formula, and Guards (iii), with parameters and their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i). This helper is a statement of the metatheory.

(i) Let $I$ be an interval containing two distinct points. The letters $h$, $x$ and $L$ are distinct set variables, and $I$, $\mathbb{R}$, its operations $+$ and $\cdot$, its elements $0$ and $1$, its order $\le$ and the strict order $<$ of $\le$ are parameters. Let $\gamma(h,x,L)$ be the guard $\mu(h,I,\mathbb{R})\wedge x\in I\wedge L\in\mathbb{R}$, with $\mu$ the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii); it holds if and only if $h$ is a map $h:I\to\mathbb{R}$, $x\in I$ and $L\in\mathbb{R}$. Then the condition "$\gamma(h,x,L)$ holds and $L$ is a derivative of $h$ at $x$" on $h$, $x$ and $L$ is expressed by a predicative formula.

(ii) The letters $t$, $m$ and $z$ are distinct set variables, and $\mathbb{R}$, its multiplication $\cdot$ and its element $1$, $\mathbb{N}$, $\mathbb{N}_{0}$, and the order $\le$, the addition $+$ and the element $0$ of $\mathbb{N}_{0}$ are parameters. Then the condition "$t\in\mathbb{R}$, $m\in\mathbb{N}_{0}$ and $z=t^{m}$" on $t$, $m$ and $z$, with the power $t^{m}$ for the multiplication of $\mathbb{R}$ as in Powers with Exponents in the Natural Numbers with Zero (i) and Powers with Exponents in the Natural Numbers with Zero (ii), is expressed by a predicative formula.