Theorem exple1

Description: A real between 0 and 1 inclusive raised to a nonnegative integer power is less than or equal to 1. (Contributed by Paul Chapman, 29-Dec-2007) (Revised by Mario Carneiro, 5-Jun-2014)

	Ref	Expression
Assertion	exple1	$$⊢\left(\left(A\in ℝ\wedge 0\le A\wedge A\le 1\right)\wedge N\in {\mathbb{N}}_0\right)\to A^N\le 1$$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$$⊢\left(\left(A\in ℝ\wedge 0\le A\wedge A\le 1\right)\wedge N\in {\mathbb{N}}_0\right)\to A\in ℝ$$
2		0nn0	$$⊢0\in {\mathbb{N}}_0$$
3	2	a1i	$$⊢\left(\left(A\in ℝ\wedge 0\le A\wedge A\le 1\right)\wedge N\in {\mathbb{N}}_0\right)\to 0\in {\mathbb{N}}_0$$
4		simpr	$$⊢\left(\left(A\in ℝ\wedge 0\le A\wedge A\le 1\right)\wedge N\in {\mathbb{N}}_0\right)\to N\in {\mathbb{N}}_0$$
5		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
6	4 5	eleqtrdi	$$⊢\left(\left(A\in ℝ\wedge 0\le A\wedge A\le 1\right)\wedge N\in {\mathbb{N}}_0\right)\to N\in {\mathbb{Z}}_{\ge 0}$$
7		simpl2	$$⊢\left(\left(A\in ℝ\wedge 0\le A\wedge A\le 1\right)\wedge N\in {\mathbb{N}}_0\right)\to 0\le A$$
8		simpl3	$$⊢\left(\left(A\in ℝ\wedge 0\le A\wedge A\le 1\right)\wedge N\in {\mathbb{N}}_0\right)\to A\le 1$$
9		leexp2r	$$⊢\left(\left(A\in ℝ\wedge 0\in {\mathbb{N}}_0\wedge N\in {\mathbb{Z}}_{\ge 0}\right)\wedge \left(0\le A\wedge A\le 1\right)\right)\to A^N\le A^0$$
10	1 3 6 7 8 9	syl32anc	$$⊢\left(\left(A\in ℝ\wedge 0\le A\wedge A\le 1\right)\wedge N\in {\mathbb{N}}_0\right)\to A^N\le A^0$$
11	1	recnd	$$⊢\left(\left(A\in ℝ\wedge 0\le A\wedge A\le 1\right)\wedge N\in {\mathbb{N}}_0\right)\to A\in ℂ$$
12		exp0	$$⊢A\in ℂ\to A^0=1$$
13	11 12	syl	$$⊢\left(\left(A\in ℝ\wedge 0\le A\wedge A\le 1\right)\wedge N\in {\mathbb{N}}_0\right)\to A^0=1$$
14	10 13	breqtrd	$$⊢\left(\left(A\in ℝ\wedge 0\le A\wedge A\le 1\right)\wedge N\in {\mathbb{N}}_0\right)\to A^N\le 1$$