This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ≤ ( 𝐴 ↑ 𝑁 ) )