This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑋 ) ∈ ( ℝ ∖ ℚ ) )