# 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 ${⊢}\left({X}\in {ℤ}_{\ge 2}\wedge {B}\in {ℤ}_{\ge 2}\wedge {X}\mathrm{gcd}{B}=1\right)\to {\mathrm{log}}_{{B}}{X}\in \left(ℝ\setminus ℚ\right)$

### Proof

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