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 \in (ℝ ∖ ℚ)$

Step	Hyp	Ref	Expression
1		3prm	$⊢ 3 \in ℙ$
2		2prm	$⊢ 2 \in ℙ$
3		2re	$⊢ 2 \in ℝ$
4		2lt3	$⊢ 2 < 3$
5	3 4	gtneii	$⊢ 3 \neq 2$
6		logbprmirr	$⊢ (3 \in ℙ \land 2 \in ℙ \land 3 \neq 2) \to \log_{2} 3 \in (ℝ ∖ ℚ)$
7	1 2 5 6	mp3an	$⊢ \log_{2} 3 \in (ℝ ∖ ℚ)$