Theorem lermxnn0

Description: The X-sequence is monotonic on NN0 . (Contributed by Stefan O'Rear, 4-Oct-2014)

	Ref	Expression
Assertion	lermxnn0	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(M\le N\leftrightarrow A{X}_{\mathrm{rm}}M\le A{X}_{\mathrm{rm}}N\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢a=b\to A{X}_{\mathrm{rm}}a=A{X}_{\mathrm{rm}}b$$
2		oveq2	$$⊢a=M\to A{X}_{\mathrm{rm}}a=A{X}_{\mathrm{rm}}M$$
3		oveq2	$$⊢a=N\to A{X}_{\mathrm{rm}}a=A{X}_{\mathrm{rm}}N$$
4		nn0ssre	$$⊢{\mathbb{N}}_0\subseteq ℝ$$
5		nn0z	$$⊢a\in {\mathbb{N}}_0\to a\in \mathbb{Z}$$
6		frmx	$$⊢X_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶{\mathbb{N}}_0$$
7	6	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in \mathbb{Z}\right)\to A{X}_{\mathrm{rm}}a\in {\mathbb{N}}_0$$
8	5 7	sylan2	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in {\mathbb{N}}_0\right)\to A{X}_{\mathrm{rm}}a\in {\mathbb{N}}_0$$
9	8	nn0red	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in {\mathbb{N}}_0\right)\to A{X}_{\mathrm{rm}}a\in ℝ$$
10		ltrmxnn0	$$⊢\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{X}_{\mathrm{rm}}a<A{X}_{\mathrm{rm}}b\right)$$
11	10	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{X}_{\mathrm{rm}}a<A{X}_{\mathrm{rm}}b\right)$$
12	11	3expb	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge \left(a\in {\mathbb{N}}_0\wedge b\in {\mathbb{N}}_0\right)\right)\to \left(a<b\to A{X}_{\mathrm{rm}}a<A{X}_{\mathrm{rm}}b\right)$$
13	1 2 3 4 9 12	leord1	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge \left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\right)\to \left(M\le N\leftrightarrow A{X}_{\mathrm{rm}}M\le A{X}_{\mathrm{rm}}N\right)$$
14	13	3impb	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(M\le N\leftrightarrow A{X}_{\mathrm{rm}}M\le A{X}_{\mathrm{rm}}N\right)$$