[proofplan] We use the standard first-order presentation of Peano arithmetic in the language $\mathcal{L}_{\mathrm{PA}}=\{0,S,+,\cdot,=\}$ where addition is introduced by the recursion axioms $\forall x\,(x+0=x)$ and $\forall x\forall y\,(x+S(y)=S(x+y))$. Under this convention, the target sentence is exactly the base recursion axiom for addition. Since every axiom of a formal theory has a derivation with no undischarged assumptions, the sentence is immediately a theorem of $\mathrm{PA}$. [/proofplan] [step:Identify the displayed sentence as an axiom in the chosen presentation of Peano arithmetic] Let $\mathcal{L}_{\mathrm{PA}} = \{0,S,+,\cdot,=\}$ denote the first-order language of Peano arithmetic, and let $\mathrm{PA}$ denote the standard first-order theory in this language whose addition axioms are the recursion equations $\forall x\,(x+0=x)$ and $\forall x\forall y\,(x+S(y)=S(x+y))$. By the first addition recursion axiom of this presentation, the universally quantified sentence $\forall x\,(x+0=x)$ belongs to the axiom set of $\mathrm{PA}$. [/step] [step:Derive the axiom as a theorem of the theory] By the definition of formal derivability from a theory, every axiom of the theory has a derivation with no open assumptions: the one-line derivation whose sole formula is that axiom. Since $\forall x\,(x+0=x)$ is an axiom of $\mathrm{PA}$, it follows that $\mathrm{PA}\vdash \forall x\,(x+0=x)$. [/step] [step:Conclude the right identity law for addition] The preceding derivation is exactly the asserted statement that Peano arithmetic proves $\forall x\,(x+0=x)$. Thus zero is a right identity for addition in $\mathrm{PA}$. [/step]