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
|- ( ( X e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) /\ ( X gcd B ) = 1 ) -> ( B logb X ) e. ( RR \ QQ ) )

Proof

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