Metamath Proof Explorer

Theorem lermy

Description: Y is monotonic (non-strict). (Contributed by Stefan O'Rear, 3-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( a = b -> ( A rmY a ) = ( A rmY b ) )
2 oveq2 
 |-  ( a = M -> ( A rmY a ) = ( A rmY M ) )
3 oveq2 
 |-  ( a = N -> ( A rmY a ) = ( A rmY N ) )
4 zssre 
 |-  ZZ C_ RR
5 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
6 5 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ ) -> ( A rmY a ) e. ZZ )
7 6 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ ) -> ( A rmY a ) e. RR )
8 ltrmy 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ /\ b e. ZZ ) -> ( a < b <-> ( A rmY a ) < ( A rmY b ) ) )
9 8 biimpd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ /\ b e. ZZ ) -> ( a < b -> ( A rmY a ) < ( A rmY b ) ) )
10 9 3expb 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a < b -> ( A rmY a ) < ( A rmY b ) ) )
11 1 2 3 4 7 10 leord1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M <_ N <-> ( A rmY M ) <_ ( A rmY N ) ) )
12 11 3impb 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( A rmY M ) <_ ( A rmY N ) ) )