Theorem leexp2rd

Description: Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	resqcld.1	$$⊢\phi \to A\in ℝ$$
	leexp2rd.2	$$⊢\phi \to M\in {\mathbb{N}}_0$$
	leexp2rd.3	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
	leexp2rd.4	$$⊢\phi \to 0\le A$$
	leexp2rd.5	$$⊢\phi \to A\le 1$$
Assertion	leexp2rd	$$⊢\phi \to A^N\le A^M$$

Proof

Step	Hyp	Ref	Expression
1		resqcld.1	$$⊢\phi \to A\in ℝ$$
2		leexp2rd.2	$$⊢\phi \to M\in {\mathbb{N}}_0$$
3		leexp2rd.3	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
4		leexp2rd.4	$$⊢\phi \to 0\le A$$
5		leexp2rd.5	$$⊢\phi \to A\le 1$$
6		leexp2r	$$⊢\left(\left(A\in ℝ\wedge M\in {\mathbb{N}}_0\wedge N\in {\mathbb{Z}}_{\ge M}\right)\wedge \left(0\le A\wedge A\le 1\right)\right)\to A^N\le A^M$$
7	1 2 3 4 5 6	syl32anc	$$⊢\phi \to A^N\le A^M$$