# Metamath Proof Explorer

## 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 ${⊢}{\mathrm{log}}_{2}9\in \left(ℝ\setminus ℚ\right)$

### Proof

Step Hyp Ref Expression
1 sq3 ${⊢}{3}^{2}=9$
2 1 eqcomi ${⊢}9={3}^{2}$
3 2 oveq2i ${⊢}{\mathrm{log}}_{2}9={\mathrm{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)↔\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 ℤ$
12 relogbzexp ${⊢}\left(2\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge 3\in {ℝ}^{+}\wedge 2\in ℤ\right)\to {\mathrm{log}}_{2}{3}^{2}=2{\mathrm{log}}_{2}3$
13 9 10 11 12 mp3an ${⊢}{\mathrm{log}}_{2}{3}^{2}=2{\mathrm{log}}_{2}3$
14 3 13 eqtri ${⊢}{\mathrm{log}}_{2}9=2{\mathrm{log}}_{2}3$
15 3cn ${⊢}3\in ℂ$
16 3ne0 ${⊢}3\ne 0$
17 eldifsn ${⊢}3\in \left(ℂ\setminus \left\{0\right\}\right)↔\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 {\mathrm{log}}_{2}3\in ℂ$
20 9 18 19 mp2an ${⊢}{\mathrm{log}}_{2}3\in ℂ$
21 4 20 mulcomi ${⊢}2{\mathrm{log}}_{2}3={\mathrm{log}}_{2}3\cdot 2$
22 2logb3irr ${⊢}{\mathrm{log}}_{2}3\in \left(ℝ\setminus ℚ\right)$
23 zq ${⊢}2\in ℤ\to 2\in ℚ$
24 11 23 ax-mp ${⊢}2\in ℚ$
25 irrmul ${⊢}\left({\mathrm{log}}_{2}3\in \left(ℝ\setminus ℚ\right)\wedge 2\in ℚ\wedge 2\ne 0\right)\to {\mathrm{log}}_{2}3\cdot 2\in \left(ℝ\setminus ℚ\right)$
26 22 24 5 25 mp3an ${⊢}{\mathrm{log}}_{2}3\cdot 2\in \left(ℝ\setminus ℚ\right)$
27 21 26 eqeltri ${⊢}2{\mathrm{log}}_{2}3\in \left(ℝ\setminus ℚ\right)$
28 14 27 eqeltri ${⊢}{\mathrm{log}}_{2}9\in \left(ℝ\setminus ℚ\right)$