Theorem rmyabs

Description: rmY commutes with abs . (Contributed by Stefan O'Rear, 26-Sep-2014)

	Ref	Expression
Assertion	rmyabs	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in \mathbb{Z}\right)\to \left|A{Y}_{\mathrm{rm}}B\right|=A{Y}_{\mathrm{rm}}\left|B\right|$$

Proof

Step	Hyp	Ref	Expression
1		frmy	$$⊢Y_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶\mathbb{Z}$$
2	1	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}a\in \mathbb{Z}$$
3	2	zred	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}a\in ℝ$$
4		simp1	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in \mathbb{Z}\wedge 0\le a\right)\to A\in {\mathbb{Z}}_{\ge 2}$$
5		elnn0z	$$⊢a\in {\mathbb{N}}_0\leftrightarrow \left(a\in \mathbb{Z}\wedge 0\le a\right)$$
6	5	biimpri	$$⊢\left(a\in \mathbb{Z}\wedge 0\le a\right)\to a\in {\mathbb{N}}_0$$
7	6	3adant1	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in \mathbb{Z}\wedge 0\le a\right)\to a\in {\mathbb{N}}_0$$
8		rmxypos	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in {\mathbb{N}}_0\right)\to \left(0<A{X}_{\mathrm{rm}}a\wedge 0\le A{Y}_{\mathrm{rm}}a\right)$$
9	4 7 8	syl2anc	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in \mathbb{Z}\wedge 0\le a\right)\to \left(0<A{X}_{\mathrm{rm}}a\wedge 0\le A{Y}_{\mathrm{rm}}a\right)$$
10	9	simprd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in \mathbb{Z}\wedge 0\le a\right)\to 0\le A{Y}_{\mathrm{rm}}a$$
11		rmyneg	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}\left(-b\right)=-\left(A{Y}_{\mathrm{rm}}b\right)$$
12		oveq2	$$⊢a=b\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}b$$
13		oveq2	$$⊢a=-b\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}\left(-b\right)$$
14		oveq2	$$⊢a=B\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}B$$
15		oveq2	$$⊢a=\left|B\right|\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}\left|B\right|$$
16	3 10 11 12 13 14 15	oddcomabszz	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge B\in \mathbb{Z}\right)\to \left|A{Y}_{\mathrm{rm}}B\right|=A{Y}_{\mathrm{rm}}\left|B\right|$$