Theorem ltrmxnn0

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

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

Proof

Step	Hyp	Ref	Expression
1		nn0z	$$⊢b\in {\mathbb{N}}_0\to b\in \mathbb{Z}$$
2		frmx	$$⊢X_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶{\mathbb{N}}_0$$
3	2	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in \mathbb{Z}\right)\to A{X}_{\mathrm{rm}}b\in {\mathbb{N}}_0$$
4	1 3	sylan2	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{X}_{\mathrm{rm}}b\in {\mathbb{N}}_0$$
5	4	nn0red	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{X}_{\mathrm{rm}}b\in ℝ$$
6		eluzelre	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in ℝ$$
7	6	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A\in ℝ$$
8	5 7	remulcld	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to \left(A{X}_{\mathrm{rm}}b\right)A\in ℝ$$
9	1	peano2zd	$$⊢b\in {\mathbb{N}}_0\to b+1\in \mathbb{Z}$$
10	2	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b+1\in \mathbb{Z}\right)\to A{X}_{\mathrm{rm}}\left(b+1\right)\in {\mathbb{N}}_0$$
11	9 10	sylan2	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{X}_{\mathrm{rm}}\left(b+1\right)\in {\mathbb{N}}_0$$
12	11	nn0red	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{X}_{\mathrm{rm}}\left(b+1\right)\in ℝ$$
13		eluz2b2	$$⊢A\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(A\in \mathbb{N}\wedge 1<A\right)$$
14	13	simprbi	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1<A$$
15	14	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to 1<A$$
16		rmxypos	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to \left(0<A{X}_{\mathrm{rm}}b\wedge 0\le A{Y}_{\mathrm{rm}}b\right)$$
17	16	simpld	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to 0<A{X}_{\mathrm{rm}}b$$
18		ltmulgt11	$$⊢\left(A{X}_{\mathrm{rm}}b\in ℝ\wedge A\in ℝ\wedge 0<A{X}_{\mathrm{rm}}b\right)\to \left(1<A\leftrightarrow A{X}_{\mathrm{rm}}b<\left(A{X}_{\mathrm{rm}}b\right)A\right)$$
19	5 7 17 18	syl3anc	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to \left(1<A\leftrightarrow A{X}_{\mathrm{rm}}b<\left(A{X}_{\mathrm{rm}}b\right)A\right)$$
20	15 19	mpbid	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{X}_{\mathrm{rm}}b<\left(A{X}_{\mathrm{rm}}b\right)A$$
21		rmspecnonsq	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-1\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)$$
22	21	eldifad	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A^2-1\in \mathbb{N}$$
23	22	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A^2-1\in \mathbb{N}$$
24	23	nnred	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A^2-1\in ℝ$$
25		frmy	$$⊢Y_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶\mathbb{Z}$$
26	25	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}b\in \mathbb{Z}$$
27	1 26	sylan2	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{Y}_{\mathrm{rm}}b\in \mathbb{Z}$$
28	27	zred	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{Y}_{\mathrm{rm}}b\in ℝ$$
29	23	nnnn0d	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A^2-1\in {\mathbb{N}}_0$$
30	29	nn0ge0d	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to 0\le A^2-1$$
31	16	simprd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to 0\le A{Y}_{\mathrm{rm}}b$$
32	24 28 30 31	mulge0d	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to 0\le \left(A^2-1\right)\left(A{Y}_{\mathrm{rm}}b\right)$$
33	24 28	remulcld	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to \left(A^2-1\right)\left(A{Y}_{\mathrm{rm}}b\right)\in ℝ$$
34	8 33	addge01d	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to \left(0\le \left(A^2-1\right)\left(A{Y}_{\mathrm{rm}}b\right)\leftrightarrow \left(A{X}_{\mathrm{rm}}b\right)A\le \left(A{X}_{\mathrm{rm}}b\right)A+\left(A^2-1\right)\left(A{Y}_{\mathrm{rm}}b\right)\right)$$
35	32 34	mpbid	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to \left(A{X}_{\mathrm{rm}}b\right)A\le \left(A{X}_{\mathrm{rm}}b\right)A+\left(A^2-1\right)\left(A{Y}_{\mathrm{rm}}b\right)$$
36		rmxp1	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in \mathbb{Z}\right)\to A{X}_{\mathrm{rm}}\left(b+1\right)=\left(A{X}_{\mathrm{rm}}b\right)A+\left(A^2-1\right)\left(A{Y}_{\mathrm{rm}}b\right)$$
37	1 36	sylan2	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{X}_{\mathrm{rm}}\left(b+1\right)=\left(A{X}_{\mathrm{rm}}b\right)A+\left(A^2-1\right)\left(A{Y}_{\mathrm{rm}}b\right)$$
38	35 37	breqtrrd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to \left(A{X}_{\mathrm{rm}}b\right)A\le A{X}_{\mathrm{rm}}\left(b+1\right)$$
39	5 8 12 20 38	ltletrd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{X}_{\mathrm{rm}}b<A{X}_{\mathrm{rm}}\left(b+1\right)$$
40		nn0z	$$⊢a\in {\mathbb{N}}_0\to a\in \mathbb{Z}$$
41	2	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in \mathbb{Z}\right)\to A{X}_{\mathrm{rm}}a\in {\mathbb{N}}_0$$
42	40 41	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$$
43	42	nn0red	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in {\mathbb{N}}_0\right)\to A{X}_{\mathrm{rm}}a\in ℝ$$
44		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
45		oveq2	$$⊢a=b+1\to A{X}_{\mathrm{rm}}a=A{X}_{\mathrm{rm}}\left(b+1\right)$$
46		oveq2	$$⊢a=b\to A{X}_{\mathrm{rm}}a=A{X}_{\mathrm{rm}}b$$
47		oveq2	$$⊢a=M\to A{X}_{\mathrm{rm}}a=A{X}_{\mathrm{rm}}M$$
48		oveq2	$$⊢a=N\to A{X}_{\mathrm{rm}}a=A{X}_{\mathrm{rm}}N$$
49	39 43 44 45 46 47 48	monotuz	$$⊢\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<N\leftrightarrow A{X}_{\mathrm{rm}}M<A{X}_{\mathrm{rm}}N\right)$$
50	49	3impb	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(M<N\leftrightarrow A{X}_{\mathrm{rm}}M<A{X}_{\mathrm{rm}}N\right)$$