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

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 ( 2 logb 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 ) → ( 2 logb 3 ) ∈ ( ℝ ∖ ℚ ) )
7 1 2 5 6 mp3an ⊢ ( 2 logb 3 ) ∈ ( ℝ ∖ ℚ )