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 ⊢ A ∈ ℕ ∧ B ∈ ℤ ∧ 1 < A B → B ∈ ℕ

Proof

Step Hyp Ref Expression
1 elznn ⊢ B ∈ ℤ ↔ B ∈ ℝ ∧ B ∈ ℕ ∨ − B ∈ ℕ 0
2 2a1 ⊢ B ∈ ℕ → A ∈ ℕ → 1 < A B → B ∈ ℕ
3 2 a1d ⊢ B ∈ ℕ → B ∈ ℝ → A ∈ ℕ → 1 < A B → B ∈ ℕ
4 nncn ⊢ A ∈ ℕ → A ∈ ℂ
5 4 3ad2ant3 ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → A ∈ ℂ
6 recn ⊢ B ∈ ℝ → B ∈ ℂ
7 6 3ad2ant2 ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → B ∈ ℂ
8 simp1 ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → − B ∈ ℕ 0
9 expneg2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ − B ∈ ℕ 0 → A B = 1 A − B
10 5 7 8 9 syl3anc ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → A B = 1 A − B
11 10 breq2d ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → 1 < A B ↔ 1 < 1 A − B
12 nnre ⊢ A ∈ ℕ → A ∈ ℝ
13 reexpcl ⊢ A ∈ ℝ ∧ − B ∈ ℕ 0 → A − B ∈ ℝ
14 12 13 sylan ⊢ A ∈ ℕ ∧ − B ∈ ℕ 0 → A − B ∈ ℝ
15 14 ancoms ⊢ − B ∈ ℕ 0 ∧ A ∈ ℕ → A − B ∈ ℝ
16 12 adantl ⊢ − B ∈ ℕ 0 ∧ A ∈ ℕ → A ∈ ℝ
17 nn0z ⊢ − B ∈ ℕ 0 → − B ∈ ℤ
18 17 adantr ⊢ − B ∈ ℕ 0 ∧ A ∈ ℕ → − B ∈ ℤ
19 nngt0 ⊢ A ∈ ℕ → 0 < A
20 19 adantl ⊢ − B ∈ ℕ 0 ∧ A ∈ ℕ → 0 < A
21 expgt0 ⊢ A ∈ ℝ ∧ − B ∈ ℤ ∧ 0 < A → 0 < A − B
22 16 18 20 21 syl3anc ⊢ − B ∈ ℕ 0 ∧ A ∈ ℕ → 0 < A − B
23 15 22 jca ⊢ − B ∈ ℕ 0 ∧ A ∈ ℕ → A − B ∈ ℝ ∧ 0 < A − B
24 23 3adant2 ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → A − B ∈ ℝ ∧ 0 < A − B
25 reclt1 ⊢ A − B ∈ ℝ ∧ 0 < A − B → A − B < 1 ↔ 1 < 1 A − B
26 24 25 syl ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → A − B < 1 ↔ 1 < 1 A − B
27 12 3ad2ant3 ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → A ∈ ℝ
28 nnge1 ⊢ A ∈ ℕ → 1 ≤ A
29 28 3ad2ant3 ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → 1 ≤ A
30 27 8 29 expge1d ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → 1 ≤ A − B
31 1red ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → 1 ∈ ℝ
32 15 3adant2 ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → A − B ∈ ℝ
33 31 32 lenltd ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → 1 ≤ A − B ↔ ¬ A − B < 1
34 pm2.21 ⊢ ¬ A − B < 1 → A − B < 1 → B ∈ ℕ
35 33 34 biimtrdi ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → 1 ≤ A − B → A − B < 1 → B ∈ ℕ
36 30 35 mpd ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → A − B < 1 → B ∈ ℕ
37 26 36 sylbird ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → 1 < 1 A − B → B ∈ ℕ
38 11 37 sylbid ⊢ − B ∈ ℕ 0 ∧ B ∈ ℝ ∧ A ∈ ℕ → 1 < A B → B ∈ ℕ
39 38 3exp ⊢ − B ∈ ℕ 0 → B ∈ ℝ → A ∈ ℕ → 1 < A B → B ∈ ℕ
40 3 39 jaoi ⊢ B ∈ ℕ ∨ − B ∈ ℕ 0 → B ∈ ℝ → A ∈ ℕ → 1 < A B → B ∈ ℕ
41 40 impcom ⊢ B ∈ ℝ ∧ B ∈ ℕ ∨ − B ∈ ℕ 0 → A ∈ ℕ → 1 < A B → B ∈ ℕ
42 1 41 sylbi ⊢ B ∈ ℤ → A ∈ ℕ → 1 < A B → B ∈ ℕ
43 42 3imp21 ⊢ A ∈ ℕ ∧ B ∈ ℤ ∧ 1 < A B → B ∈ ℕ