Theorem ltrmynn0

Description: The Y-sequence is strictly monotonic on NN0 . Strengthened by ltrmy . (Contributed by Stefan O'Rear, 24-Sep-2014)

	Ref	Expression
Assertion	ltrmynn0	$$⊢\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{Y}_{\mathrm{rm}}M<A{Y}_{\mathrm{rm}}N\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$$⊢b\in {\mathbb{N}}_0\to b\in \mathbb{Z}$$
2		frmy	$$⊢Y_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶\mathbb{Z}$$
3	2	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}b\in \mathbb{Z}$$
4	1 3	sylan2	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{Y}_{\mathrm{rm}}b\in \mathbb{Z}$$
5	4	zred	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{Y}_{\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{Y}_{\mathrm{rm}}b\right)A\in ℝ$$
9		frmx	$$⊢X_{\mathrm{rm}}:{\mathbb{Z}}_{\ge 2}\times \mathbb{Z}⟶{\mathbb{N}}_0$$
10	9	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in \mathbb{Z}\right)\to A{X}_{\mathrm{rm}}b\in {\mathbb{N}}_0$$
11	1 10	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$$
12	11	nn0red	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{X}_{\mathrm{rm}}b\in ℝ$$
13	8 12	readdcld	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to \left(A{Y}_{\mathrm{rm}}b\right)A+\left(A{X}_{\mathrm{rm}}b\right)\in ℝ$$
14		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)$$
15	14	simprd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to 0\le A{Y}_{\mathrm{rm}}b$$
16		eluz2nn	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to A\in \mathbb{N}$$
17	16	nnge1d	$$⊢A\in {\mathbb{Z}}_{\ge 2}\to 1\le A$$
18	17	adantr	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to 1\le A$$
19	5 7 15 18	lemulge11d	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{Y}_{\mathrm{rm}}b\le \left(A{Y}_{\mathrm{rm}}b\right)A$$
20	14	simpld	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to 0<A{X}_{\mathrm{rm}}b$$
21	12 8	ltaddposd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to \left(0<A{X}_{\mathrm{rm}}b\leftrightarrow \left(A{Y}_{\mathrm{rm}}b\right)A<\left(A{Y}_{\mathrm{rm}}b\right)A+\left(A{X}_{\mathrm{rm}}b\right)\right)$$
22	20 21	mpbid	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to \left(A{Y}_{\mathrm{rm}}b\right)A<\left(A{Y}_{\mathrm{rm}}b\right)A+\left(A{X}_{\mathrm{rm}}b\right)$$
23	5 8 13 19 22	lelttrd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{Y}_{\mathrm{rm}}b<\left(A{Y}_{\mathrm{rm}}b\right)A+\left(A{X}_{\mathrm{rm}}b\right)$$
24		rmyp1	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}\left(b+1\right)=\left(A{Y}_{\mathrm{rm}}b\right)A+\left(A{X}_{\mathrm{rm}}b\right)$$
25	1 24	sylan2	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{Y}_{\mathrm{rm}}\left(b+1\right)=\left(A{Y}_{\mathrm{rm}}b\right)A+\left(A{X}_{\mathrm{rm}}b\right)$$
26	23 25	breqtrrd	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge b\in {\mathbb{N}}_0\right)\to A{Y}_{\mathrm{rm}}b<A{Y}_{\mathrm{rm}}\left(b+1\right)$$
27		nn0z	$$⊢a\in {\mathbb{N}}_0\to a\in \mathbb{Z}$$
28	2	fovcl	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in \mathbb{Z}\right)\to A{Y}_{\mathrm{rm}}a\in \mathbb{Z}$$
29	27 28	sylan2	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in {\mathbb{N}}_0\right)\to A{Y}_{\mathrm{rm}}a\in \mathbb{Z}$$
30	29	zred	$$⊢\left(A\in {\mathbb{Z}}_{\ge 2}\wedge a\in {\mathbb{N}}_0\right)\to A{Y}_{\mathrm{rm}}a\in ℝ$$
31		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
32		oveq2	$$⊢a=b+1\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}\left(b+1\right)$$
33		oveq2	$$⊢a=b\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}b$$
34		oveq2	$$⊢a=M\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}M$$
35		oveq2	$$⊢a=N\to A{Y}_{\mathrm{rm}}a=A{Y}_{\mathrm{rm}}N$$
36	26 30 31 32 33 34 35	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{Y}_{\mathrm{rm}}M<A{Y}_{\mathrm{rm}}N\right)$$
37	36	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{Y}_{\mathrm{rm}}M<A{Y}_{\mathrm{rm}}N\right)$$