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	|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN0 /\ N e. NN0 ) -> ( M < N <-> ( A rmY M ) < ( A rmY N ) ) )

Proof

Step	Hyp	Ref	Expression
1		nn0z	|- ( b e. NN0 -> b e. ZZ )
2		frmy	|- rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
3	2	fovcl	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY b ) e. ZZ )
4	1 3	sylan2	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmY b ) e. ZZ )
5	4	zred	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmY b ) e. RR )
6		eluzelre	|- ( A e. ( ZZ>= ` 2 ) -> A e. RR )
7	6	adantr	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> A e. RR )
8	5 7	remulcld	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( ( A rmY b ) x. A ) e. RR )
9		frmx	|- rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
10	9	fovcl	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmX b ) e. NN0 )
11	1 10	sylan2	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmX b ) e. NN0 )
12	11	nn0red	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmX b ) e. RR )
13	8 12	readdcld	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( ( ( A rmY b ) x. A ) + ( A rmX b ) ) e. RR )
14		rmxypos	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) )
15	14	simprd	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> 0 <_ ( A rmY b ) )
16		eluz2nn	|- ( A e. ( ZZ>= ` 2 ) -> A e. NN )
17	16	nnge1d	|- ( A e. ( ZZ>= ` 2 ) -> 1 <_ A )
18	17	adantr	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> 1 <_ A )
19	5 7 15 18	lemulge11d	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmY b ) <_ ( ( A rmY b ) x. A ) )
20	14	simpld	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> 0 < ( A rmX b ) )
21	12 8	ltaddposd	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( 0 < ( A rmX b ) <-> ( ( A rmY b ) x. A ) < ( ( ( A rmY b ) x. A ) + ( A rmX b ) ) ) )
22	20 21	mpbid	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( ( A rmY b ) x. A ) < ( ( ( A rmY b ) x. A ) + ( A rmX b ) ) )
23	5 8 13 19 22	lelttrd	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmY b ) < ( ( ( A rmY b ) x. A ) + ( A rmX b ) ) )
24		rmyp1	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY ( b + 1 ) ) = ( ( ( A rmY b ) x. A ) + ( A rmX b ) ) )
25	1 24	sylan2	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmY ( b + 1 ) ) = ( ( ( A rmY b ) x. A ) + ( A rmX b ) ) )
26	23 25	breqtrrd	|- ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmY b ) < ( A rmY ( b + 1 ) ) )
27		nn0z	|- ( a e. NN0 -> a e. ZZ )
28	2	fovcl	|- ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ ) -> ( A rmY a ) e. ZZ )
29	27 28	sylan2	|- ( ( A e. ( ZZ>= ` 2 ) /\ a e. NN0 ) -> ( A rmY a ) e. ZZ )
30	29	zred	|- ( ( A e. ( ZZ>= ` 2 ) /\ a e. NN0 ) -> ( A rmY a ) e. RR )
31		nn0uz	|- NN0 = ( ZZ>= ` 0 )
32		oveq2	|- ( a = ( b + 1 ) -> ( A rmY a ) = ( A rmY ( b + 1 ) ) )
33		oveq2	|- ( a = b -> ( A rmY a ) = ( A rmY b ) )
34		oveq2	|- ( a = M -> ( A rmY a ) = ( A rmY M ) )
35		oveq2	|- ( a = N -> ( A rmY a ) = ( A rmY N ) )
36	26 30 31 32 33 34 35	monotuz	|- ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( M < N <-> ( A rmY M ) < ( A rmY N ) ) )
37	36	3impb	|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN0 /\ N e. NN0 ) -> ( M < N <-> ( A rmY M ) < ( A rmY N ) ) )