Theorem zgt1rpn0n1

Description: An integer greater than 1 is a positive real number not equal to 0 or 1. Useful for working with integer logarithm bases (which is a common case, e.g., base 2, base 3, or base 10). (Contributed by Thierry Arnoux, 26-Sep-2017) (Proof shortened by AV, 9-Jul-2022)

	Ref	Expression
Assertion	zgt1rpn0n1	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to \left(B\in {ℝ}^{+}\wedge B\ne 0\wedge B\ne 1\right)$$

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to B\in \mathbb{N}$$
2	1	nnrpd	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to B\in {ℝ}^{+}$$
3		eluz2n0	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to B\ne 0$$
4		1nuz2	$$⊢\neg 1\in {\mathbb{Z}}_{\ge 2}$$
5		nelne2	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge \neg 1\in {\mathbb{Z}}_{\ge 2}\right)\to B\ne 1$$
6	4 5	mpan2	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to B\ne 1$$
7	2 3 6	3jca	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to \left(B\in {ℝ}^{+}\wedge B\ne 0\wedge B\ne 1\right)$$