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 
|- ( ( 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 ) )