This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ltexp2r

Description: The integer powers of a fixed positive real less than 1 decrease as the exponent increases. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 5-Jun-2014)

Ref Expression
Assertion ltexp2r 
|- ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> ( M < N <-> ( A ^ N ) < ( A ^ M ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> A e. RR+ )
2 1 rpcnd 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> A e. CC )
3 1 rpne0d 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> A =/= 0 )
4 simpl2 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> M e. ZZ )
5 exprec 
 |-  ( ( A e. CC /\ A =/= 0 /\ M e. ZZ ) -> ( ( 1 / A ) ^ M ) = ( 1 / ( A ^ M ) ) )
6 2 3 4 5 syl3anc 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> ( ( 1 / A ) ^ M ) = ( 1 / ( A ^ M ) ) )
7 simpl3 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> N e. ZZ )
8 exprec 
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( ( 1 / A ) ^ N ) = ( 1 / ( A ^ N ) ) )
9 2 3 7 8 syl3anc 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> ( ( 1 / A ) ^ N ) = ( 1 / ( A ^ N ) ) )
10 6 9 breq12d 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> ( ( ( 1 / A ) ^ M ) < ( ( 1 / A ) ^ N ) <-> ( 1 / ( A ^ M ) ) < ( 1 / ( A ^ N ) ) ) )
11 1 rprecred 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> ( 1 / A ) e. RR )
12 simpr 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> A < 1 )
13 1 reclt1d 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> ( A < 1 <-> 1 < ( 1 / A ) ) )
14 12 13 mpbid 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> 1 < ( 1 / A ) )
15 ltexp2 
 |-  ( ( ( ( 1 / A ) e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < ( 1 / A ) ) -> ( M < N <-> ( ( 1 / A ) ^ M ) < ( ( 1 / A ) ^ N ) ) )
16 11 4 7 14 15 syl31anc 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> ( M < N <-> ( ( 1 / A ) ^ M ) < ( ( 1 / A ) ^ N ) ) )
17 rpexpcl 
 |-  ( ( A e. RR+ /\ N e. ZZ ) -> ( A ^ N ) e. RR+ )
18 1 7 17 syl2anc 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> ( A ^ N ) e. RR+ )
19 rpexpcl 
 |-  ( ( A e. RR+ /\ M e. ZZ ) -> ( A ^ M ) e. RR+ )
20 1 4 19 syl2anc 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> ( A ^ M ) e. RR+ )
21 18 20 ltrecd 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> ( ( A ^ N ) < ( A ^ M ) <-> ( 1 / ( A ^ M ) ) < ( 1 / ( A ^ N ) ) ) )
22 10 16 21 3bitr4d 
 |-  ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> ( M < N <-> ( A ^ N ) < ( A ^ M ) ) )