This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 1 < ( 𝐴 ↑ 𝐵 ) ) → 𝐵 ∈ ℕ )

Proof

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