Metamath Proof Explorer

Theorem ltrmy

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

Ref Expression
Assertion ltrmy 
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( A rmY M ) < ( A rmY N ) ) )

Proof

Step Hyp Ref Expression
1 ltrmynn0 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. NN0 /\ b e. NN0 ) -> ( a < b <-> ( A rmY a ) < ( A rmY b ) ) )
2 1 biimpd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. NN0 /\ b e. NN0 ) -> ( a < b -> ( A rmY a ) < ( A rmY b ) ) )
3 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
4 3 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ ) -> ( A rmY a ) e. ZZ )
5 4 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ ) -> ( A rmY a ) e. RR )
6 rmyneg 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY -u b ) = -u ( A rmY b ) )
7 oveq2 
 |-  ( a = M -> ( A rmY a ) = ( A rmY M ) )
8 oveq2 
 |-  ( a = N -> ( A rmY a ) = ( A rmY N ) )
9 oveq2 
 |-  ( a = b -> ( A rmY a ) = ( A rmY b ) )
10 oveq2 
 |-  ( a = -u b -> ( A rmY a ) = ( A rmY -u b ) )
11 2 5 6 7 8 9 10 monotoddzz 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( A rmY M ) < ( A rmY N ) ) )