Theorem expge1

Description: A real greater than or equal to 1 raised to a nonnegative integer is greater than or equal to 1. (Contributed by NM, 21-Feb-2005) (Revised by Mario Carneiro, 4-Jun-2014)

	Ref	Expression
Assertion	expge1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝐴 ) → 1 ≤ ( 𝐴 ↑ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑧 = 𝐴 → ( 1 ≤ 𝑧 ↔ 1 ≤ 𝐴 ) )
2	1	elrab	⊢ ( 𝐴 ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } ↔ ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) )
3		ssrab2	⊢ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } ⊆ ℝ
4		ax-resscn	⊢ ℝ ⊆ ℂ
5	3 4	sstri	⊢ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } ⊆ ℂ
6		breq2	⊢ ( 𝑧 = 𝑥 → ( 1 ≤ 𝑧 ↔ 1 ≤ 𝑥 ) )
7	6	elrab	⊢ ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) )
8		breq2	⊢ ( 𝑧 = 𝑦 → ( 1 ≤ 𝑧 ↔ 1 ≤ 𝑦 ) )
9	8	elrab	⊢ ( 𝑦 ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } ↔ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) )
10		breq2	⊢ ( 𝑧 = ( 𝑥 · 𝑦 ) → ( 1 ≤ 𝑧 ↔ 1 ≤ ( 𝑥 · 𝑦 ) ) )
11		remulcl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
12	11	ad2ant2r	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
13		1t1e1	⊢ ( 1 · 1 ) = 1
14		1re	⊢ 1 ∈ ℝ
15		0le1	⊢ 0 ≤ 1
16	14 15	pm3.2i	⊢ ( 1 ∈ ℝ ∧ 0 ≤ 1 )
17	16	jctl	⊢ ( 𝑥 ∈ ℝ → ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ 𝑥 ∈ ℝ ) )
18	16	jctl	⊢ ( 𝑦 ∈ ℝ → ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ 𝑦 ∈ ℝ ) )
19		lemul12a	⊢ ( ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ 𝑥 ∈ ℝ ) ∧ ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ 𝑦 ∈ ℝ ) ) → ( ( 1 ≤ 𝑥 ∧ 1 ≤ 𝑦 ) → ( 1 · 1 ) ≤ ( 𝑥 · 𝑦 ) ) )
20	17 18 19	syl2an	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 1 ≤ 𝑥 ∧ 1 ≤ 𝑦 ) → ( 1 · 1 ) ≤ ( 𝑥 · 𝑦 ) ) )
21	20	imp	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 1 ≤ 𝑥 ∧ 1 ≤ 𝑦 ) ) → ( 1 · 1 ) ≤ ( 𝑥 · 𝑦 ) )
22	13 21	eqbrtrrid	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 1 ≤ 𝑥 ∧ 1 ≤ 𝑦 ) ) → 1 ≤ ( 𝑥 · 𝑦 ) )
23	22	an4s	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 1 ≤ ( 𝑥 · 𝑦 ) )
24	10 12 23	elrabd	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( 𝑥 · 𝑦 ) ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } )
25	7 9 24	syl2anb	⊢ ( ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } ∧ 𝑦 ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } ) → ( 𝑥 · 𝑦 ) ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } )
26		1le1	⊢ 1 ≤ 1
27		breq2	⊢ ( 𝑧 = 1 → ( 1 ≤ 𝑧 ↔ 1 ≤ 1 ) )
28	27	elrab	⊢ ( 1 ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } ↔ ( 1 ∈ ℝ ∧ 1 ≤ 1 ) )
29	14 26 28	mpbir2an	⊢ 1 ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 }
30	5 25 29	expcllem	⊢ ( ( 𝐴 ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } )
31	2 30	sylanbr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } )
32	31	3impa	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } )
33	32	3com23	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝐴 ) → ( 𝐴 ↑ 𝑁 ) ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } )
34		breq2	⊢ ( 𝑧 = ( 𝐴 ↑ 𝑁 ) → ( 1 ≤ 𝑧 ↔ 1 ≤ ( 𝐴 ↑ 𝑁 ) ) )
35	34	elrab	⊢ ( ( 𝐴 ↑ 𝑁 ) ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } ↔ ( ( 𝐴 ↑ 𝑁 ) ∈ ℝ ∧ 1 ≤ ( 𝐴 ↑ 𝑁 ) ) )
36	35	simprbi	⊢ ( ( 𝐴 ↑ 𝑁 ) ∈ { 𝑧 ∈ ℝ ∣ 1 ≤ 𝑧 } → 1 ≤ ( 𝐴 ↑ 𝑁 ) )
37	33 36	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝐴 ) → 1 ≤ ( 𝐴 ↑ 𝑁 ) )