Metamath Proof Explorer


Theorem logbgcd1irr

Description: The logarithm of an integer greater than 1 to an integer base greater than 1 is an irrational number if the argument and the base are relatively prime. For example, ( 2 logb 9 ) e. ( RR \ QQ ) (see 2logb9irr ). (Contributed by AV, 29-Dec-2022)

Ref Expression
Assertion logbgcd1irr ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → ( 𝐵 logb 𝑋 ) ∈ ( ℝ ∖ ℚ ) )

Proof

Step Hyp Ref Expression
1 eluz2nn ( 𝐵 ∈ ( ℤ ‘ 2 ) → 𝐵 ∈ ℕ )
2 1 nnrpd ( 𝐵 ∈ ( ℤ ‘ 2 ) → 𝐵 ∈ ℝ+ )
3 2 3ad2ant2 ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → 𝐵 ∈ ℝ+ )
4 eluz2nn ( 𝑋 ∈ ( ℤ ‘ 2 ) → 𝑋 ∈ ℕ )
5 4 nnrpd ( 𝑋 ∈ ( ℤ ‘ 2 ) → 𝑋 ∈ ℝ+ )
6 5 3ad2ant1 ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → 𝑋 ∈ ℝ+ )
7 eluz2b3 ( 𝐵 ∈ ( ℤ ‘ 2 ) ↔ ( 𝐵 ∈ ℕ ∧ 𝐵 ≠ 1 ) )
8 7 simprbi ( 𝐵 ∈ ( ℤ ‘ 2 ) → 𝐵 ≠ 1 )
9 8 3ad2ant2 ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → 𝐵 ≠ 1 )
10 3 6 9 3jca ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → ( 𝐵 ∈ ℝ+𝑋 ∈ ℝ+𝐵 ≠ 1 ) )
11 relogbcl ( ( 𝐵 ∈ ℝ+𝑋 ∈ ℝ+𝐵 ≠ 1 ) → ( 𝐵 logb 𝑋 ) ∈ ℝ )
12 10 11 syl ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → ( 𝐵 logb 𝑋 ) ∈ ℝ )
13 eluz2gt1 ( 𝑋 ∈ ( ℤ ‘ 2 ) → 1 < 𝑋 )
14 13 adantr ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → 1 < 𝑋 )
15 4 adantr ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → 𝑋 ∈ ℕ )
16 15 nnrpd ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → 𝑋 ∈ ℝ+ )
17 1 adantl ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → 𝐵 ∈ ℕ )
18 17 nnrpd ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → 𝐵 ∈ ℝ+ )
19 eluz2gt1 ( 𝐵 ∈ ( ℤ ‘ 2 ) → 1 < 𝐵 )
20 19 adantl ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → 1 < 𝐵 )
21 logbgt0b ( ( 𝑋 ∈ ℝ+ ∧ ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ) → ( 0 < ( 𝐵 logb 𝑋 ) ↔ 1 < 𝑋 ) )
22 16 18 20 21 syl12anc ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → ( 0 < ( 𝐵 logb 𝑋 ) ↔ 1 < 𝑋 ) )
23 14 22 mpbird ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → 0 < ( 𝐵 logb 𝑋 ) )
24 23 anim1ci ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐵 logb 𝑋 ) ∈ ℚ ) → ( ( 𝐵 logb 𝑋 ) ∈ ℚ ∧ 0 < ( 𝐵 logb 𝑋 ) ) )
25 elpq ( ( ( 𝐵 logb 𝑋 ) ∈ ℚ ∧ 0 < ( 𝐵 logb 𝑋 ) ) → ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) )
26 24 25 syl ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝐵 logb 𝑋 ) ∈ ℚ ) → ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) )
27 26 ex ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → ( ( 𝐵 logb 𝑋 ) ∈ ℚ → ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) ) )
28 oveq2 ( ( 𝑚 / 𝑛 ) = ( 𝐵 logb 𝑋 ) → ( 𝐵𝑐 ( 𝑚 / 𝑛 ) ) = ( 𝐵𝑐 ( 𝐵 logb 𝑋 ) ) )
29 28 eqcoms ( ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) → ( 𝐵𝑐 ( 𝑚 / 𝑛 ) ) = ( 𝐵𝑐 ( 𝐵 logb 𝑋 ) ) )
30 eluzelcn ( 𝐵 ∈ ( ℤ ‘ 2 ) → 𝐵 ∈ ℂ )
31 30 adantl ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → 𝐵 ∈ ℂ )
32 nnne0 ( 𝐵 ∈ ℕ → 𝐵 ≠ 0 )
33 1 32 syl ( 𝐵 ∈ ( ℤ ‘ 2 ) → 𝐵 ≠ 0 )
34 33 8 nelprd ( 𝐵 ∈ ( ℤ ‘ 2 ) → ¬ 𝐵 ∈ { 0 , 1 } )
35 34 adantl ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → ¬ 𝐵 ∈ { 0 , 1 } )
36 31 35 eldifd ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
37 eluzelcn ( 𝑋 ∈ ( ℤ ‘ 2 ) → 𝑋 ∈ ℂ )
38 37 adantr ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → 𝑋 ∈ ℂ )
39 nnne0 ( 𝑋 ∈ ℕ → 𝑋 ≠ 0 )
40 nelsn ( 𝑋 ≠ 0 → ¬ 𝑋 ∈ { 0 } )
41 4 39 40 3syl ( 𝑋 ∈ ( ℤ ‘ 2 ) → ¬ 𝑋 ∈ { 0 } )
42 41 adantr ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → ¬ 𝑋 ∈ { 0 } )
43 38 42 eldifd ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → 𝑋 ∈ ( ℂ ∖ { 0 } ) )
44 cxplogb ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵𝑐 ( 𝐵 logb 𝑋 ) ) = 𝑋 )
45 36 43 44 syl2anc ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → ( 𝐵𝑐 ( 𝐵 logb 𝑋 ) ) = 𝑋 )
46 45 adantr ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐵𝑐 ( 𝐵 logb 𝑋 ) ) = 𝑋 )
47 29 46 sylan9eqr ( ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) ) → ( 𝐵𝑐 ( 𝑚 / 𝑛 ) ) = 𝑋 )
48 47 ex ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) → ( 𝐵𝑐 ( 𝑚 / 𝑛 ) ) = 𝑋 ) )
49 oveq1 ( ( 𝐵𝑐 ( 𝑚 / 𝑛 ) ) = 𝑋 → ( ( 𝐵𝑐 ( 𝑚 / 𝑛 ) ) ↑ 𝑛 ) = ( 𝑋𝑛 ) )
50 31 adantr ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → 𝐵 ∈ ℂ )
51 nncn ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
52 51 adantr ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑚 ∈ ℂ )
53 nncn ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
54 53 adantl ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
55 nnne0 ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
56 55 adantl ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑛 ≠ 0 )
57 52 54 56 3jca ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
58 divcl ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) → ( 𝑚 / 𝑛 ) ∈ ℂ )
59 57 58 syl ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝑚 / 𝑛 ) ∈ ℂ )
60 59 adantl ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝑚 / 𝑛 ) ∈ ℂ )
61 nnnn0 ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
62 61 adantl ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
63 62 adantl ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → 𝑛 ∈ ℕ0 )
64 50 60 63 3jca ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐵 ∈ ℂ ∧ ( 𝑚 / 𝑛 ) ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) )
65 cxpmul2 ( ( 𝐵 ∈ ℂ ∧ ( 𝑚 / 𝑛 ) ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( 𝐵𝑐 ( ( 𝑚 / 𝑛 ) · 𝑛 ) ) = ( ( 𝐵𝑐 ( 𝑚 / 𝑛 ) ) ↑ 𝑛 ) )
66 65 eqcomd ( ( 𝐵 ∈ ℂ ∧ ( 𝑚 / 𝑛 ) ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐵𝑐 ( 𝑚 / 𝑛 ) ) ↑ 𝑛 ) = ( 𝐵𝑐 ( ( 𝑚 / 𝑛 ) · 𝑛 ) ) )
67 64 66 syl ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵𝑐 ( 𝑚 / 𝑛 ) ) ↑ 𝑛 ) = ( 𝐵𝑐 ( ( 𝑚 / 𝑛 ) · 𝑛 ) ) )
68 57 adantl ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
69 divcan1 ( ( 𝑚 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) → ( ( 𝑚 / 𝑛 ) · 𝑛 ) = 𝑚 )
70 68 69 syl ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝑚 / 𝑛 ) · 𝑛 ) = 𝑚 )
71 70 oveq2d ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐵𝑐 ( ( 𝑚 / 𝑛 ) · 𝑛 ) ) = ( 𝐵𝑐 𝑚 ) )
72 33 adantl ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → 𝐵 ≠ 0 )
73 72 adantr ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → 𝐵 ≠ 0 )
74 nnz ( 𝑚 ∈ ℕ → 𝑚 ∈ ℤ )
75 74 adantr ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑚 ∈ ℤ )
76 75 adantl ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → 𝑚 ∈ ℤ )
77 50 73 76 cxpexpzd ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐵𝑐 𝑚 ) = ( 𝐵𝑚 ) )
78 71 77 eqtrd ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐵𝑐 ( ( 𝑚 / 𝑛 ) · 𝑛 ) ) = ( 𝐵𝑚 ) )
79 67 78 eqtrd ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵𝑐 ( 𝑚 / 𝑛 ) ) ↑ 𝑛 ) = ( 𝐵𝑚 ) )
80 79 eqeq1d ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 𝐵𝑐 ( 𝑚 / 𝑛 ) ) ↑ 𝑛 ) = ( 𝑋𝑛 ) ↔ ( 𝐵𝑚 ) = ( 𝑋𝑛 ) ) )
81 simpr ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
82 rplpwr ( ( 𝑋 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑋 gcd 𝐵 ) = 1 → ( ( 𝑋𝑛 ) gcd 𝐵 ) = 1 ) )
83 15 17 81 82 syl2an3an ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝑋 gcd 𝐵 ) = 1 → ( ( 𝑋𝑛 ) gcd 𝐵 ) = 1 ) )
84 oveq1 ( ( 𝑋𝑛 ) = ( 𝐵𝑚 ) → ( ( 𝑋𝑛 ) gcd 𝐵 ) = ( ( 𝐵𝑚 ) gcd 𝐵 ) )
85 84 eqeq1d ( ( 𝑋𝑛 ) = ( 𝐵𝑚 ) → ( ( ( 𝑋𝑛 ) gcd 𝐵 ) = 1 ↔ ( ( 𝐵𝑚 ) gcd 𝐵 ) = 1 ) )
86 85 eqcoms ( ( 𝐵𝑚 ) = ( 𝑋𝑛 ) → ( ( ( 𝑋𝑛 ) gcd 𝐵 ) = 1 ↔ ( ( 𝐵𝑚 ) gcd 𝐵 ) = 1 ) )
87 86 adantl ( ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( 𝐵𝑚 ) = ( 𝑋𝑛 ) ) → ( ( ( 𝑋𝑛 ) gcd 𝐵 ) = 1 ↔ ( ( 𝐵𝑚 ) gcd 𝐵 ) = 1 ) )
88 eluzelz ( 𝐵 ∈ ( ℤ ‘ 2 ) → 𝐵 ∈ ℤ )
89 88 adantl ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → 𝐵 ∈ ℤ )
90 simpl ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑚 ∈ ℕ )
91 rpexp ( ( 𝐵 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝐵𝑚 ) gcd 𝐵 ) = 1 ↔ ( 𝐵 gcd 𝐵 ) = 1 ) )
92 89 89 90 91 syl2an3an ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 𝐵𝑚 ) gcd 𝐵 ) = 1 ↔ ( 𝐵 gcd 𝐵 ) = 1 ) )
93 gcdid ( 𝐵 ∈ ℤ → ( 𝐵 gcd 𝐵 ) = ( abs ‘ 𝐵 ) )
94 88 93 syl ( 𝐵 ∈ ( ℤ ‘ 2 ) → ( 𝐵 gcd 𝐵 ) = ( abs ‘ 𝐵 ) )
95 eluzelre ( 𝐵 ∈ ( ℤ ‘ 2 ) → 𝐵 ∈ ℝ )
96 nnnn0 ( 𝐵 ∈ ℕ → 𝐵 ∈ ℕ0 )
97 nn0ge0 ( 𝐵 ∈ ℕ0 → 0 ≤ 𝐵 )
98 1 96 97 3syl ( 𝐵 ∈ ( ℤ ‘ 2 ) → 0 ≤ 𝐵 )
99 95 98 absidd ( 𝐵 ∈ ( ℤ ‘ 2 ) → ( abs ‘ 𝐵 ) = 𝐵 )
100 94 99 eqtrd ( 𝐵 ∈ ( ℤ ‘ 2 ) → ( 𝐵 gcd 𝐵 ) = 𝐵 )
101 100 eqeq1d ( 𝐵 ∈ ( ℤ ‘ 2 ) → ( ( 𝐵 gcd 𝐵 ) = 1 ↔ 𝐵 = 1 ) )
102 101 adantl ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → ( ( 𝐵 gcd 𝐵 ) = 1 ↔ 𝐵 = 1 ) )
103 102 adantr ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵 gcd 𝐵 ) = 1 ↔ 𝐵 = 1 ) )
104 eqneqall ( 𝐵 = 1 → ( 𝐵 ≠ 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
105 8 104 syl5com ( 𝐵 ∈ ( ℤ ‘ 2 ) → ( 𝐵 = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
106 105 adantl ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → ( 𝐵 = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
107 106 adantr ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( 𝐵 = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
108 103 107 sylbid ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵 gcd 𝐵 ) = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
109 92 108 sylbid ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 𝐵𝑚 ) gcd 𝐵 ) = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
110 109 adantr ( ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( 𝐵𝑚 ) = ( 𝑋𝑛 ) ) → ( ( ( 𝐵𝑚 ) gcd 𝐵 ) = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
111 87 110 sylbid ( ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( 𝐵𝑚 ) = ( 𝑋𝑛 ) ) → ( ( ( 𝑋𝑛 ) gcd 𝐵 ) = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
112 111 ex ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵𝑚 ) = ( 𝑋𝑛 ) → ( ( ( 𝑋𝑛 ) gcd 𝐵 ) = 1 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) ) )
113 112 com23 ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 𝑋𝑛 ) gcd 𝐵 ) = 1 → ( ( 𝐵𝑚 ) = ( 𝑋𝑛 ) → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) ) )
114 83 113 syld ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝑋 gcd 𝐵 ) = 1 → ( ( 𝐵𝑚 ) = ( 𝑋𝑛 ) → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) ) )
115 ax-1 ( ¬ ( 𝑋 gcd 𝐵 ) = 1 → ( ( 𝐵𝑚 ) = ( 𝑋𝑛 ) → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
116 114 115 pm2.61d1 ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵𝑚 ) = ( 𝑋𝑛 ) → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
117 80 116 sylbid ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 𝐵𝑐 ( 𝑚 / 𝑛 ) ) ↑ 𝑛 ) = ( 𝑋𝑛 ) → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
118 49 117 syl5 ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵𝑐 ( 𝑚 / 𝑛 ) ) = 𝑋 → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
119 48 118 syld ( ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
120 119 rexlimdvva ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( 𝐵 logb 𝑋 ) = ( 𝑚 / 𝑛 ) → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
121 27 120 syld ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → ( ( 𝐵 logb 𝑋 ) ∈ ℚ → ¬ ( 𝑋 gcd 𝐵 ) = 1 ) )
122 121 con2d ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ) → ( ( 𝑋 gcd 𝐵 ) = 1 → ¬ ( 𝐵 logb 𝑋 ) ∈ ℚ ) )
123 122 3impia ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → ¬ ( 𝐵 logb 𝑋 ) ∈ ℚ )
124 12 123 eldifd ( ( 𝑋 ∈ ( ℤ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → ( 𝐵 logb 𝑋 ) ∈ ( ℝ ∖ ℚ ) )