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 ⊢ A ∈ ℝ ∧ N ∈ ℕ 0 ∧ 1 ≤ A → 1 ≤ A N

Proof

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