Theorem ltrmy

Description: The Y-sequence is strictly monotonic over ZZ . (Contributed by Stefan O'Rear, 25-Sep-2014)

	Ref	Expression
Assertion	ltrmy	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(M<N\leftrightarrow A{Y}_{\mathrm{rm}}M<A{Y}_{\mathrm{rm}}N\right)$$

Proof

Step	Hyp	Ref	Expression
1		ltrmynn0	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\right)\to \left(a<b\leftrightarrow A{Y}_{\mathrm{rm}}a<A{Y}_{\mathrm{rm}}b\right)$$
2	1	biimpd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\right)\to \left(a<b\to A{Y}_{\mathrm{rm}}a<A{Y}_{\mathrm{rm}}b\right)$$
3		frmy	$$⊢Y_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶\mathbb{Z}$$
4	3	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}a\in \mathbb{Z}$$
5	4	zred	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}a\in ℝ$$
6		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)$$
7		oveq2	$$⊢a=M\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}M$$
8		oveq2	$$⊢a=N\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}N$$
9		oveq2	$$⊢a=b\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}b$$
10		oveq2	$$⊢a=-b\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}\left(-b\right)$$
11	2 5 6 7 8 9 10	monotoddzz	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(M<N\leftrightarrow A{Y}_{\mathrm{rm}}M<A{Y}_{\mathrm{rm}}N\right)$$