Metamath Proof Explorer

Theorem ltrmxnn0

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

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

Proof

Step Hyp Ref Expression
1 nn0z 
 |-  ( b e. NN0 -> b e. ZZ )
2 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
3 2 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmX b ) e. NN0 )
4 1 3 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmX b ) e. NN0 )
5 4 nn0red 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmX 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 rmX b ) x. A ) e. RR )
9 1 peano2zd 
 |-  ( b e. NN0 -> ( b + 1 ) e. ZZ )
10 2 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( b + 1 ) e. ZZ ) -> ( A rmX ( b + 1 ) ) e. NN0 )
11 9 10 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmX ( b + 1 ) ) e. NN0 )
12 11 nn0red 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmX ( b + 1 ) ) e. RR )
13 eluz2b2 
 |-  ( A e. ( ZZ>= ` 2 ) <-> ( A e. NN /\ 1 < A ) )
14 13 simprbi 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 < A )
15 14 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> 1 < A )
16 rmxypos 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( 0 < ( A rmX b ) /\ 0 <_ ( A rmY b ) ) )
17 16 simpld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> 0 < ( A rmX b ) )
18 ltmulgt11 
 |-  ( ( ( A rmX b ) e. RR /\ A e. RR /\ 0 < ( A rmX b ) ) -> ( 1 < A <-> ( A rmX b ) < ( ( A rmX b ) x. A ) ) )
19 5 7 17 18 syl3anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( 1 < A <-> ( A rmX b ) < ( ( A rmX b ) x. A ) ) )
20 15 19 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmX b ) < ( ( A rmX b ) x. A ) )
21 rmspecnonsq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )
22 21 eldifad 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. NN )
23 22 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( ( A ^ 2 ) - 1 ) e. NN )
24 23 nnred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( ( A ^ 2 ) - 1 ) e. RR )
25 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
26 25 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmY b ) e. ZZ )
27 1 26 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmY b ) e. ZZ )
28 27 zred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmY b ) e. RR )
29 23 nnnn0d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( ( A ^ 2 ) - 1 ) e. NN0 )
30 29 nn0ge0d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> 0 <_ ( ( A ^ 2 ) - 1 ) )
31 16 simprd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> 0 <_ ( A rmY b ) )
32 24 28 30 31 mulge0d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> 0 <_ ( ( ( A ^ 2 ) - 1 ) x. ( A rmY b ) ) )
33 24 28 remulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( ( ( A ^ 2 ) - 1 ) x. ( A rmY b ) ) e. RR )
34 8 33 addge01d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( 0 <_ ( ( ( A ^ 2 ) - 1 ) x. ( A rmY b ) ) <-> ( ( A rmX b ) x. A ) <_ ( ( ( A rmX b ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A rmY b ) ) ) ) )
35 32 34 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( ( A rmX b ) x. A ) <_ ( ( ( A rmX b ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A rmY b ) ) ) )
36 rmxp1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( A rmX ( b + 1 ) ) = ( ( ( A rmX b ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A rmY b ) ) ) )
37 1 36 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmX ( b + 1 ) ) = ( ( ( A rmX b ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A rmY b ) ) ) )
38 35 37 breqtrrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( ( A rmX b ) x. A ) <_ ( A rmX ( b + 1 ) ) )
39 5 8 12 20 38 ltletrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ b e. NN0 ) -> ( A rmX b ) < ( A rmX ( b + 1 ) ) )
40 nn0z 
 |-  ( a e. NN0 -> a e. ZZ )
41 2 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. ZZ ) -> ( A rmX a ) e. NN0 )
42 40 41 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. NN0 ) -> ( A rmX a ) e. NN0 )
43 42 nn0red 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ a e. NN0 ) -> ( A rmX a ) e. RR )
44 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
45 oveq2 
 |-  ( a = ( b + 1 ) -> ( A rmX a ) = ( A rmX ( b + 1 ) ) )
46 oveq2 
 |-  ( a = b -> ( A rmX a ) = ( A rmX b ) )
47 oveq2 
 |-  ( a = M -> ( A rmX a ) = ( A rmX M ) )
48 oveq2 
 |-  ( a = N -> ( A rmX a ) = ( A rmX N ) )
49 39 43 44 45 46 47 48 monotuz 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( M < N <-> ( A rmX M ) < ( A rmX N ) ) )
50 49 3impb 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN0 /\ N e. NN0 ) -> ( M < N <-> ( A rmX M ) < ( A rmX N ) ) )