Metamath Proof Explorer

Theorem logbprmirr

Description: The logarithm of a prime to a different prime base is an irrational number. For example, ( 2 logb 3 ) e. ( RR \ QQ ) (see 2logb3irr ). (Contributed by AV, 31-Dec-2022)

		Ref	Expression
	Assertion	logbprmirr	$⊢ (X \in ℙ \land B \in ℙ \land X \neq B) \to \log_{B} X \in (ℝ ∖ ℚ)$

Proof

Step	Hyp	Ref	Expression
1		prmuz2	$⊢ X \in ℙ \to X \in ℤ_{\geq 2}$
2	1	3ad2ant1	$⊢ (X \in ℙ \land B \in ℙ \land X \neq B) \to X \in ℤ_{\geq 2}$
3		prmuz2	$⊢ B \in ℙ \to B \in ℤ_{\geq 2}$
4	3	3ad2ant2	$⊢ (X \in ℙ \land B \in ℙ \land X \neq B) \to B \in ℤ_{\geq 2}$
5		prmrp	$⊢ (X \in ℙ \land B \in ℙ) \to (X \gcd B = 1 \leftrightarrow X \neq B)$
6	5	biimp3ar	$⊢ (X \in ℙ \land B \in ℙ \land X \neq B) \to X \gcd B = 1$
7		logbgcd1irr	$⊢ (X \in ℤ_{\geq 2} \land B \in ℤ_{\geq 2} \land X \gcd B = 1) \to \log_{B} X \in (ℝ ∖ ℚ)$
8	2 4 6 7	syl3anc	$⊢ (X \in ℙ \land B \in ℙ \land X \neq B) \to \log_{B} X \in (ℝ ∖ ℚ)$