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	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ≤ 1 )

Proof

Step	Hyp	Ref	Expression
1		simpl1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
2		0nn0	⊢ 0 ∈ ℕ0
3	2	a1i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → 0 ∈ ℕ0 )
4		simpr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
5		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
6	4 5	eleqtrdi	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
7		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ 𝐴 )
8		simpl3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ≤ 1 )
9		leexp2r	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 0 ) ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 0 ) )
10	1 3 6 7 8 9	syl32anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ≤ ( 𝐴 ↑ 0 ) )
11	1	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
12		exp0	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
13	11 12	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 0 ) = 1 )
14	10 13	breqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ≤ 1 )