Metamath Proof Explorer

Theorem 2logb3irr

Description: Example for logbprmirr . The logarithm of three to base two is irrational. (Contributed by AV, 31-Dec-2022)

Ref Expression
Assertion 2logb3irr ⊢ log 2 3 ∈ ℝ ∖ ℚ

Proof

Step Hyp Ref Expression
1 3prm ⊢ 3 ∈ ℙ
2 2prm ⊢ 2 ∈ ℙ
3 2re ⊢ 2 ∈ ℝ
4 2lt3 ⊢ 2 < 3
5 3 4 gtneii ⊢ 3 ≠ 2
6 logbprmirr ⊢ 3 ∈ ℙ ∧ 2 ∈ ℙ ∧ 3 ≠ 2 → log 2 3 ∈ ℝ ∖ ℚ
7 1 2 5 6 mp3an ⊢ log 2 3 ∈ ℝ ∖ ℚ