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<AB→B∈ℕ

Proof

Step Hyp Ref Expression
1 elznn ⊢B∈ℤ↔B∈ℝ∧B∈ℕ∨−B∈ℕ0
2 2a1 ⊢B∈ℕ→A∈ℕ→1<AB→B∈ℕ
3 2 a1d ⊢B∈ℕ→B∈ℝ→A∈ℕ→1<AB→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→AB=1A−B
10 5 7 8 9 syl3anc ⊢−B∈ℕ0∧B∈ℝ∧A∈ℕ→AB=1A−B
11 10 breq2d ⊢−B∈ℕ0∧B∈ℝ∧A∈ℕ→1<AB↔1<1A−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<1A−B
26 24 25 syl ⊢−B∈ℕ0∧B∈ℝ∧A∈ℕ→A−B<1↔1<1A−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 syl6bi ⊢−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<1A−B→B∈ℕ
38 11 37 sylbid ⊢−B∈ℕ0∧B∈ℝ∧A∈ℕ→1<AB→B∈ℕ
39 38 3exp ⊢−B∈ℕ0→B∈ℝ→A∈ℕ→1<AB→B∈ℕ
40 3 39 jaoi ⊢B∈ℕ∨−B∈ℕ0→B∈ℝ→A∈ℕ→1<AB→B∈ℕ
41 40 impcom ⊢B∈ℝ∧B∈ℕ∨−B∈ℕ0→A∈ℕ→1<AB→B∈ℕ
42 1 41 sylbi ⊢B∈ℤ→A∈ℕ→1<AB→B∈ℕ
43 42 3imp21 ⊢A∈ℕ∧B∈ℤ∧1<AB→B∈ℕ