Theorem ltexp2rd

Description: The power of a positive number smaller than 1 decreases as its exponent increases. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	rpexpcld.1	|- ( ph -> A e. RR+ )
	rpexpcld.2	|- ( ph -> N e. ZZ )
	ltexp2rd.3	|- ( ph -> M e. ZZ )
	ltexp2rd.4	|- ( ph -> A < 1 )
Assertion	ltexp2rd	|- ( ph -> ( M < N <-> ( A ^ N ) < ( A ^ M ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpexpcld.1	|- ( ph -> A e. RR+ )
2		rpexpcld.2	|- ( ph -> N e. ZZ )
3		ltexp2rd.3	|- ( ph -> M e. ZZ )
4		ltexp2rd.4	|- ( ph -> A < 1 )
5		ltexp2r	|- ( ( ( A e. RR+ /\ M e. ZZ /\ N e. ZZ ) /\ A < 1 ) -> ( M < N <-> ( A ^ N ) < ( A ^ M ) ) )
6	1 3 2 4 5	syl31anc	|- ( ph -> ( M < N <-> ( A ^ N ) < ( A ^ M ) ) )