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 ( 2 logb 9 ) ∈ ( ℝ ∖ ℚ )

Proof

Step Hyp Ref Expression
1 sq3 ⊢ ( 3 ↑ 2 ) = 9
2 1 eqcomi ⊢ 9 = ( 3 ↑ 2 )
3 2 oveq2i ⊢ ( 2 logb 9 ) = ( 2 logb ( 3 ↑ 2 ) )
4 2cn ⊢ 2 ∈ ℂ
5 2ne0 ⊢ 2 ≠ 0
6 1ne2 ⊢ 1 ≠ 2
7 6 necomi ⊢ 2 ≠ 1
8 eldifpr ⊢ ( 2 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) )
9 4 5 7 8 mpbir3an ⊢ 2 ∈ ( ℂ ∖ { 0 , 1 } )
10 3rp ⊢ 3 ∈ ℝ+
11 2z ⊢ 2 ∈ ℤ
12 relogbzexp ⊢ ( ( 2 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 3 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 2 logb ( 3 ↑ 2 ) ) = ( 2 · ( 2 logb 3 ) ) )
13 9 10 11 12 mp3an ⊢ ( 2 logb ( 3 ↑ 2 ) ) = ( 2 · ( 2 logb 3 ) )
14 3 13 eqtri ⊢ ( 2 logb 9 ) = ( 2 · ( 2 logb 3 ) )
15 3cn ⊢ 3 ∈ ℂ
16 3ne0 ⊢ 3 ≠ 0
17 eldifsn ⊢ ( 3 ∈ ( ℂ ∖ { 0 } ) ↔ ( 3 ∈ ℂ ∧ 3 ≠ 0 ) )
18 15 16 17 mpbir2an ⊢ 3 ∈ ( ℂ ∖ { 0 } )
19 logbcl ⊢ ( ( 2 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 3 ∈ ( ℂ ∖ { 0 } ) ) → ( 2 logb 3 ) ∈ ℂ )
20 9 18 19 mp2an ⊢ ( 2 logb 3 ) ∈ ℂ
21 4 20 mulcomi ⊢ ( 2 · ( 2 logb 3 ) ) = ( ( 2 logb 3 ) · 2 )
22 2logb3irr ⊢ ( 2 logb 3 ) ∈ ( ℝ ∖ ℚ )
23 zq ⊢ ( 2 ∈ ℤ → 2 ∈ ℚ )
24 11 23 ax-mp ⊢ 2 ∈ ℚ
25 irrmul ⊢ ( ( ( 2 logb 3 ) ∈ ( ℝ ∖ ℚ ) ∧ 2 ∈ ℚ ∧ 2 ≠ 0 ) → ( ( 2 logb 3 ) · 2 ) ∈ ( ℝ ∖ ℚ ) )
26 22 24 5 25 mp3an ⊢ ( ( 2 logb 3 ) · 2 ) ∈ ( ℝ ∖ ℚ )
27 21 26 eqeltri ⊢ ( 2 · ( 2 logb 3 ) ) ∈ ( ℝ ∖ ℚ )
28 14 27 eqeltri ⊢ ( 2 logb 9 ) ∈ ( ℝ ∖ ℚ )