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	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ) \to (1 < A^{B} \leftrightarrow B \in ℕ)$

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	$⊢ A \in ℤ_{\geq 2} \to A \in ℕ$
2	1	adantr	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ) \to A \in ℕ$
3	2	adantr	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℤ) \land 1 < A^{B}) \to A \in ℕ$
4		simplr	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℤ) \land 1 < A^{B}) \to B \in ℤ$
5		simpr	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℤ) \land 1 < A^{B}) \to 1 < A^{B}$
6		expnngt1	$⊢ (A \in ℕ \land B \in ℤ \land 1 < A^{B}) \to B \in ℕ$
7	3 4 5 6	syl3anc	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℤ) \land 1 < A^{B}) \to B \in ℕ$
8	2	nnred	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ) \to A \in ℝ$
9	8	adantr	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℤ) \land B \in ℕ) \to A \in ℝ$
10		simpr	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℤ) \land B \in ℕ) \to B \in ℕ$
11		eluz2gt1	$⊢ A \in ℤ_{\geq 2} \to 1 < A$
12	11	adantr	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ) \to 1 < A$
13	12	adantr	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℤ) \land B \in ℕ) \to 1 < A$
14		expgt1	$⊢ (A \in ℝ \land B \in ℕ \land 1 < A) \to 1 < A^{B}$
15	9 10 13 14	syl3anc	$⊢ ((A \in ℤ_{\geq 2} \land B \in ℤ) \land B \in ℕ) \to 1 < A^{B}$
16	7 15	impbida	$⊢ (A \in ℤ_{\geq 2} \land B \in ℤ) \to (1 < A^{B} \leftrightarrow B \in ℕ)$