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

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

Proof

Step Hyp Ref Expression
1 eluz2nn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ )
2 1 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℕ )
3 2 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) ∧ 1 < ( 𝐴 ↑ 𝐵 ) ) → 𝐴 ∈ ℕ )
4 simplr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) ∧ 1 < ( 𝐴 ↑ 𝐵 ) ) → 𝐵 ∈ ℤ )
5 simpr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) ∧ 1 < ( 𝐴 ↑ 𝐵 ) ) → 1 < ( 𝐴 ↑ 𝐵 ) )
6 expnngt1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 1 < ( 𝐴 ↑ 𝐵 ) ) → 𝐵 ∈ ℕ )
7 3 4 5 6 syl3anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) ∧ 1 < ( 𝐴 ↑ 𝐵 ) ) → 𝐵 ∈ ℕ )
8 2 nnred ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℝ )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℝ )
10 simpr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℕ )
11 eluz2gt1 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐴 )
12 11 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) → 1 < 𝐴 )
13 12 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) ∧ 𝐵 ∈ ℕ ) → 1 < 𝐴 )
14 expgt1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 1 < 𝐴 ) → 1 < ( 𝐴 ↑ 𝐵 ) )
15 9 10 13 14 syl3anc ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) ∧ 𝐵 ∈ ℕ ) → 1 < ( 𝐴 ↑ 𝐵 ) )
16 7 15 impbida ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ℤ ) → ( 1 < ( 𝐴 ↑ 𝐵 ) ↔ 𝐵 ∈ ℕ ) )