Metamath Proof Explorer

Theorem expnngt1b

Description: An integer power with an integer base greater than 1 is greater than 1 iff the exponent is positive. (Contributed by AV, 28-Dec-2022)

Ref Expression
Assertion expnngt1b ⊢ A ∈ ℤ ≥ 2 ∧ B ∈ ℤ → 1 < A B ↔ B ∈ ℕ

Proof

Step Hyp Ref Expression
1 eluz2nn ⊢ A ∈ ℤ ≥ 2 → A ∈ ℕ
2 1 adantr ⊢ A ∈ ℤ ≥ 2 ∧ B ∈ ℤ → A ∈ ℕ
3 2 adantr ⊢ A ∈ ℤ ≥ 2 ∧ B ∈ ℤ ∧ 1 < A B → A ∈ ℕ
4 simplr ⊢ A ∈ ℤ ≥ 2 ∧ B ∈ ℤ ∧ 1 < A B → B ∈ ℤ
5 simpr ⊢ A ∈ ℤ ≥ 2 ∧ B ∈ ℤ ∧ 1 < A B → 1 < A B
6 expnngt1 ⊢ A ∈ ℕ ∧ B ∈ ℤ ∧ 1 < A B → B ∈ ℕ
7 3 4 5 6 syl3anc ⊢ A ∈ ℤ ≥ 2 ∧ B ∈ ℤ ∧ 1 < A B → B ∈ ℕ
8 2 nnred ⊢ A ∈ ℤ ≥ 2 ∧ B ∈ ℤ → A ∈ ℝ
9 8 adantr ⊢ A ∈ ℤ ≥ 2 ∧ B ∈ ℤ ∧ B ∈ ℕ → A ∈ ℝ
10 simpr ⊢ A ∈ ℤ ≥ 2 ∧ B ∈ ℤ ∧ B ∈ ℕ → B ∈ ℕ
11 eluz2gt1 ⊢ A ∈ ℤ ≥ 2 → 1 < A
12 11 adantr ⊢ A ∈ ℤ ≥ 2 ∧ B ∈ ℤ → 1 < A
13 12 adantr ⊢ A ∈ ℤ ≥ 2 ∧ B ∈ ℤ ∧ B ∈ ℕ → 1 < A
14 expgt1 ⊢ A ∈ ℝ ∧ B ∈ ℕ ∧ 1 < A → 1 < A B
15 9 10 13 14 syl3anc ⊢ A ∈ ℤ ≥ 2 ∧ B ∈ ℤ ∧ B ∈ ℕ → 1 < A B
16 7 15 impbida ⊢ A ∈ ℤ ≥ 2 ∧ B ∈ ℤ → 1 < A B ↔ B ∈ ℕ