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 < ( 𝐴 ↑ 𝐵 ) ↔ 𝐵 ∈ ℕ ) )