Metamath Proof Explorer

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	$⊢ ((A \in ℝ \land 0 \leq A \land A \leq 1) \land N \in ℕ_{0}) \to A^{N} \leq 1$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in ℝ \land 0 \leq A \land A \leq 1) \land N \in ℕ_{0}) \to A \in ℝ$
2		0nn0	$⊢ 0 \in ℕ_{0}$
3	2	a1i	$⊢ ((A \in ℝ \land 0 \leq A \land A \leq 1) \land N \in ℕ_{0}) \to 0 \in ℕ_{0}$
4		simpr	$⊢ ((A \in ℝ \land 0 \leq A \land A \leq 1) \land N \in ℕ_{0}) \to N \in ℕ_{0}$
5		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
6	4 5	eleqtrdi	$⊢ ((A \in ℝ \land 0 \leq A \land A \leq 1) \land N \in ℕ_{0}) \to N \in ℤ_{\geq 0}$
7		simpl2	$⊢ ((A \in ℝ \land 0 \leq A \land A \leq 1) \land N \in ℕ_{0}) \to 0 \leq A$
8		simpl3	$⊢ ((A \in ℝ \land 0 \leq A \land A \leq 1) \land N \in ℕ_{0}) \to A \leq 1$
9		leexp2r	$⊢ ((A \in ℝ \land 0 \in ℕ_{0} \land N \in ℤ_{\geq 0}) \land (0 \leq A \land A \leq 1)) \to A^{N} \leq A^{0}$
10	1 3 6 7 8 9	syl32anc	$⊢ ((A \in ℝ \land 0 \leq A \land A \leq 1) \land N \in ℕ_{0}) \to A^{N} \leq A^{0}$
11	1	recnd	$⊢ ((A \in ℝ \land 0 \leq A \land A \leq 1) \land N \in ℕ_{0}) \to A \in ℂ$
12		exp0	$⊢ A \in ℂ \to A^{0} = 1$
13	11 12	syl	$⊢ ((A \in ℝ \land 0 \leq A \land A \leq 1) \land N \in ℕ_{0}) \to A^{0} = 1$
14	10 13	breqtrd	$⊢ ((A \in ℝ \land 0 \leq A \land A \leq 1) \land N \in ℕ_{0}) \to A^{N} \leq 1$