# 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 ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\to \left(1<{{A}}^{{B}}↔{B}\in ℕ\right)$

### Proof

Step Hyp Ref Expression
1 eluz2nn ${⊢}{A}\in {ℤ}_{\ge 2}\to {A}\in ℕ$
2 1 adantr ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\to {A}\in ℕ$
3 2 adantr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\wedge 1<{{A}}^{{B}}\right)\to {A}\in ℕ$
4 simplr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\wedge 1<{{A}}^{{B}}\right)\to {B}\in ℤ$
5 simpr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\wedge 1<{{A}}^{{B}}\right)\to 1<{{A}}^{{B}}$
6 expnngt1 ${⊢}\left({A}\in ℕ\wedge {B}\in ℤ\wedge 1<{{A}}^{{B}}\right)\to {B}\in ℕ$
7 3 4 5 6 syl3anc ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\wedge 1<{{A}}^{{B}}\right)\to {B}\in ℕ$
8 2 nnred ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\to {A}\in ℝ$
9 8 adantr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\wedge {B}\in ℕ\right)\to {A}\in ℝ$
10 simpr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\wedge {B}\in ℕ\right)\to {B}\in ℕ$
11 eluz2gt1 ${⊢}{A}\in {ℤ}_{\ge 2}\to 1<{A}$
12 11 adantr ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\to 1<{A}$
13 12 adantr ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\wedge {B}\in ℕ\right)\to 1<{A}$
14 expgt1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℕ\wedge 1<{A}\right)\to 1<{{A}}^{{B}}$
15 9 10 13 14 syl3anc ${⊢}\left(\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\wedge {B}\in ℕ\right)\to 1<{{A}}^{{B}}$
16 7 15 impbida ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {B}\in ℤ\right)\to \left(1<{{A}}^{{B}}↔{B}\in ℕ\right)$