# Metamath Proof Explorer

## Theorem expnngt1

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

Ref Expression
Assertion expnngt1 ${⊢}\left({A}\in ℕ\wedge {B}\in ℤ\wedge 1<{{A}}^{{B}}\right)\to {B}\in ℕ$

### Proof

Step Hyp Ref Expression
1 elznn ${⊢}{B}\in ℤ↔\left({B}\in ℝ\wedge \left({B}\in ℕ\vee -{B}\in {ℕ}_{0}\right)\right)$
2 2a1 ${⊢}{B}\in ℕ\to \left({A}\in ℕ\to \left(1<{{A}}^{{B}}\to {B}\in ℕ\right)\right)$
3 2 a1d ${⊢}{B}\in ℕ\to \left({B}\in ℝ\to \left({A}\in ℕ\to \left(1<{{A}}^{{B}}\to {B}\in ℕ\right)\right)\right)$
4 nncn ${⊢}{A}\in ℕ\to {A}\in ℂ$
5 4 3ad2ant3 ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to {A}\in ℂ$
6 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
7 6 3ad2ant2 ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to {B}\in ℂ$
8 simp1 ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to -{B}\in {ℕ}_{0}$
9 expneg2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge -{B}\in {ℕ}_{0}\right)\to {{A}}^{{B}}=\frac{1}{{{A}}^{-{B}}}$
10 5 7 8 9 syl3anc ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to {{A}}^{{B}}=\frac{1}{{{A}}^{-{B}}}$
11 10 breq2d ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to \left(1<{{A}}^{{B}}↔1<\frac{1}{{{A}}^{-{B}}}\right)$
12 nnre ${⊢}{A}\in ℕ\to {A}\in ℝ$
13 reexpcl ${⊢}\left({A}\in ℝ\wedge -{B}\in {ℕ}_{0}\right)\to {{A}}^{-{B}}\in ℝ$
14 12 13 sylan ${⊢}\left({A}\in ℕ\wedge -{B}\in {ℕ}_{0}\right)\to {{A}}^{-{B}}\in ℝ$
15 14 ancoms ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {A}\in ℕ\right)\to {{A}}^{-{B}}\in ℝ$
16 12 adantl ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {A}\in ℕ\right)\to {A}\in ℝ$
17 nn0z ${⊢}-{B}\in {ℕ}_{0}\to -{B}\in ℤ$
18 17 adantr ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {A}\in ℕ\right)\to -{B}\in ℤ$
19 nngt0 ${⊢}{A}\in ℕ\to 0<{A}$
20 19 adantl ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {A}\in ℕ\right)\to 0<{A}$
21 expgt0 ${⊢}\left({A}\in ℝ\wedge -{B}\in ℤ\wedge 0<{A}\right)\to 0<{{A}}^{-{B}}$
22 16 18 20 21 syl3anc ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {A}\in ℕ\right)\to 0<{{A}}^{-{B}}$
23 15 22 jca ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {A}\in ℕ\right)\to \left({{A}}^{-{B}}\in ℝ\wedge 0<{{A}}^{-{B}}\right)$
24 23 3adant2 ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to \left({{A}}^{-{B}}\in ℝ\wedge 0<{{A}}^{-{B}}\right)$
25 reclt1 ${⊢}\left({{A}}^{-{B}}\in ℝ\wedge 0<{{A}}^{-{B}}\right)\to \left({{A}}^{-{B}}<1↔1<\frac{1}{{{A}}^{-{B}}}\right)$
26 24 25 syl ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to \left({{A}}^{-{B}}<1↔1<\frac{1}{{{A}}^{-{B}}}\right)$
27 12 3ad2ant3 ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to {A}\in ℝ$
28 nnge1 ${⊢}{A}\in ℕ\to 1\le {A}$
29 28 3ad2ant3 ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to 1\le {A}$
30 27 8 29 expge1d ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to 1\le {{A}}^{-{B}}$
31 1red ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to 1\in ℝ$
32 15 3adant2 ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to {{A}}^{-{B}}\in ℝ$
33 31 32 lenltd ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to \left(1\le {{A}}^{-{B}}↔¬{{A}}^{-{B}}<1\right)$
34 pm2.21 ${⊢}¬{{A}}^{-{B}}<1\to \left({{A}}^{-{B}}<1\to {B}\in ℕ\right)$
35 33 34 syl6bi ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to \left(1\le {{A}}^{-{B}}\to \left({{A}}^{-{B}}<1\to {B}\in ℕ\right)\right)$
36 30 35 mpd ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to \left({{A}}^{-{B}}<1\to {B}\in ℕ\right)$
37 26 36 sylbird ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to \left(1<\frac{1}{{{A}}^{-{B}}}\to {B}\in ℕ\right)$
38 11 37 sylbid ${⊢}\left(-{B}\in {ℕ}_{0}\wedge {B}\in ℝ\wedge {A}\in ℕ\right)\to \left(1<{{A}}^{{B}}\to {B}\in ℕ\right)$
39 38 3exp ${⊢}-{B}\in {ℕ}_{0}\to \left({B}\in ℝ\to \left({A}\in ℕ\to \left(1<{{A}}^{{B}}\to {B}\in ℕ\right)\right)\right)$
40 3 39 jaoi ${⊢}\left({B}\in ℕ\vee -{B}\in {ℕ}_{0}\right)\to \left({B}\in ℝ\to \left({A}\in ℕ\to \left(1<{{A}}^{{B}}\to {B}\in ℕ\right)\right)\right)$
41 40 impcom ${⊢}\left({B}\in ℝ\wedge \left({B}\in ℕ\vee -{B}\in {ℕ}_{0}\right)\right)\to \left({A}\in ℕ\to \left(1<{{A}}^{{B}}\to {B}\in ℕ\right)\right)$
42 1 41 sylbi ${⊢}{B}\in ℤ\to \left({A}\in ℕ\to \left(1<{{A}}^{{B}}\to {B}\in ℕ\right)\right)$
43 42 3imp21 ${⊢}\left({A}\in ℕ\wedge {B}\in ℤ\wedge 1<{{A}}^{{B}}\right)\to {B}\in ℕ$