Metamath Proof Explorer

Theorem lermxnn0

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

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( a = b -> ( A rmX a ) = ( A rmX b ) )
2 oveq2 
 |-  ( a = M -> ( A rmX a ) = ( A rmX M ) )
3 oveq2 
 |-  ( a = N -> ( A rmX a ) = ( A rmX N ) )
4 nn0ssre 
 |-  NN0 C_ RR
5 nn0z 
 |-  ( a e. NN0 -> a e. ZZ )
6 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
7 6 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ ) -> ( A rmX a ) e. NN0 )
8 5 7 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. NN0 ) -> ( A rmX a ) e. NN0 )
9 8 nn0red 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. NN0 ) -> ( A rmX a ) e. RR )
10 ltrmxnn0 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. NN0 /\ b e. NN0 ) -> ( a < b <-> ( A rmX a ) < ( A rmX b ) ) )
11 10 biimpd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. NN0 /\ b e. NN0 ) -> ( a < b -> ( A rmX a ) < ( A rmX b ) ) )
12 11 3expb 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( a e. NN0 /\ b e. NN0 ) ) -> ( a < b -> ( A rmX a ) < ( A rmX b ) ) )
13 1 2 3 4 9 12 leord1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( M <_ N <-> ( A rmX M ) <_ ( A rmX N ) ) )
14 13 3impb 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN0 /\ N e. NN0 ) -> ( M <_ N <-> ( A rmX M ) <_ ( A rmX N ) ) )