Theorem 2logb9irrALT

Description: Alternate proof of 2logb9irr : The logarithm of nine to base two is irrational. (Contributed by AV, 31-Dec-2022) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	2logb9irrALT	$$⊢{\log }_{2}9\in \left(ℝ\setminus \mathbb{Q}\right)$$

Proof

Step	Hyp	Ref	Expression
1		sq3	$$⊢3^2=9$$
2	1	eqcomi	$$⊢9=3^2$$
3	2	oveq2i	$$⊢{\log }_{2}9={\log }_2{3}^2$$
4		2cn	$$⊢2\in ℂ$$
5		2ne0	$$⊢2\ne 0$$
6		1ne2	$$⊢1\ne 2$$
7	6	necomi	$$⊢2\ne 1$$
8		eldifpr	$$⊢2\in \left(ℂ\setminus \left\{0,1\right\}\right)\leftrightarrow \left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)$$
9	4 5 7 8	mpbir3an	$$⊢2\in \left(ℂ\setminus \left\{0,1\right\}\right)$$
10		3rp	$$⊢3\in {ℝ}^{+}$$
11		2z	$$⊢2\in \mathbb{Z}$$
12		relogbzexp	$$⊢\left(2\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge 3\in {ℝ}^{+}\wedge 2\in \mathbb{Z}\right)\to {\log }_2{3}^2=2{\log }_{2}3$$
13	9 10 11 12	mp3an	$$⊢{\log }_2{3}^2=2{\log }_{2}3$$
14	3 13	eqtri	$$⊢{\log }_{2}9=2{\log }_{2}3$$
15		3cn	$$⊢3\in ℂ$$
16		3ne0	$$⊢3\ne 0$$
17		eldifsn	$$⊢3\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(3\in ℂ\wedge 3\ne 0\right)$$
18	15 16 17	mpbir2an	$$⊢3\in \left(ℂ\setminus \left\{0\right\}\right)$$
19		logbcl	$$⊢\left(2\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge 3\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to {\log }_{2}3\in ℂ$$
20	9 18 19	mp2an	$$⊢{\log }_{2}3\in ℂ$$
21	4 20	mulcomi	$$⊢2{\log }_{2}3={\log }_{2}3\cdot 2$$
22		2logb3irr	$$⊢{\log }_{2}3\in \left(ℝ\setminus \mathbb{Q}\right)$$
23		zq	$$⊢2\in \mathbb{Z}\to 2\in \mathbb{Q}$$
24	11 23	ax-mp	$$⊢2\in \mathbb{Q}$$
25		irrmul	$$⊢\left({\log }_{2}3\in \left(ℝ\setminus \mathbb{Q}\right)\wedge 2\in \mathbb{Q}\wedge 2\ne 0\right)\to {\log }_{2}3\cdot 2\in \left(ℝ\setminus \mathbb{Q}\right)$$
26	22 24 5 25	mp3an	$$⊢{\log }_{2}3\cdot 2\in \left(ℝ\setminus \mathbb{Q}\right)$$
27	21 26	eqeltri	$$⊢2{\log }_{2}3\in \left(ℝ\setminus \mathbb{Q}\right)$$
28	14 27	eqeltri	$$⊢{\log }_{2}9\in \left(ℝ\setminus \mathbb{Q}\right)$$