2logb9irr

Description: Example for logbgcd1irr . The logarithm of nine to base two is irrational. (Contributed by AV, 29-Dec-2022)

		Ref	Expression
	Assertion	2logb9irr	$⊢ \log_{2} 9 \in (ℝ ∖ ℚ)$

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		9nn	$⊢ 9 \in ℕ$
3	2	nnzi	$⊢ 9 \in ℤ$
4		2re	$⊢ 2 \in ℝ$
5		9re	$⊢ 9 \in ℝ$
6		2lt9	$⊢ 2 < 9$
7	4 5 6	ltleii	$⊢ 2 \leq 9$
8		eluz2	$⊢ 9 \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land 9 \in ℤ \land 2 \leq 9)$
9	1 3 7 8	mpbir3an	$⊢ 9 \in ℤ_{\geq 2}$
10		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
11	1 10	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
12		sq3	$⊢ 3^{2} = 9$
13	12	eqcomi	$⊢ 9 = 3^{2}$
14	13	oveq1i	$⊢ 9 \gcd 2 = 3^{2} \gcd 2$
15		2lt3	$⊢ 2 < 3$
16	4 15	gtneii	$⊢ 3 \neq 2$
17		3prm	$⊢ 3 \in ℙ$
18		2prm	$⊢ 2 \in ℙ$
19		prmrp	$⊢ (3 \in ℙ \land 2 \in ℙ) \to (3 \gcd 2 = 1 \leftrightarrow 3 \neq 2)$
20	17 18 19	mp2an	$⊢ 3 \gcd 2 = 1 \leftrightarrow 3 \neq 2$
21	16 20	mpbir	$⊢ 3 \gcd 2 = 1$
22		3z	$⊢ 3 \in ℤ$
23		2nn0	$⊢ 2 \in ℕ_{0}$
24		rpexp1i	$⊢ (3 \in ℤ \land 2 \in ℤ \land 2 \in ℕ_{0}) \to (3 \gcd 2 = 1 \to 3^{2} \gcd 2 = 1)$
25	22 1 23 24	mp3an	$⊢ 3 \gcd 2 = 1 \to 3^{2} \gcd 2 = 1$
26	21 25	ax-mp	$⊢ 3^{2} \gcd 2 = 1$
27	14 26	eqtri	$⊢ 9 \gcd 2 = 1$
28		logbgcd1irr	$⊢ (9 \in ℤ_{\geq 2} \land 2 \in ℤ_{\geq 2} \land 9 \gcd 2 = 1) \to \log_{2} 9 \in (ℝ ∖ ℚ)$
29	9 11 27 28	mp3an	$⊢ \log_{2} 9 \in (ℝ ∖ ℚ)$

Metamath Proof Explorer