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

Metamath Proof Explorer

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 ∈ ℤ ≥ 2 → B ∈ ℝ + ∧ B ≠ 0 ∧ B ≠ 1

Proof

Step Hyp Ref Expression
1 eluz2nn ⊢ B ∈ ℤ ≥ 2 → B ∈ ℕ
2 1 nnrpd ⊢ B ∈ ℤ ≥ 2 → B ∈ ℝ +
3 eluz2n0 ⊢ B ∈ ℤ ≥ 2 → B ≠ 0
4 1nuz2 ⊢ ¬ 1 ∈ ℤ ≥ 2
5 nelne2 ⊢ B ∈ ℤ ≥ 2 ∧ ¬ 1 ∈ ℤ ≥ 2 → B ≠ 1
6 4 5 mpan2 ⊢ B ∈ ℤ ≥ 2 → B ≠ 1
7 2 3 6 3jca ⊢ B ∈ ℤ ≥ 2 → B ∈ ℝ + ∧ B ≠ 0 ∧ B ≠ 1