let q, a, b be Element of NAT ; :: thesis: ( 0 < a & 1 < q & (q |^ a) -' 1 divides (q |^ b) -' 1 implies a divides b )
assume that
A1:
0 < a
and
A2:
1 < q
and
A3:
(q |^ a) -' 1 divides (q |^ b) -' 1
; :: thesis: a divides b
set r = b mod a;
set qNa = q |^ a;
set qNr = q |^ (b mod a);
defpred S1[ Nat] means (q |^ a) -' 1 divides (q |^ ((a * $1) + (b mod a))) -' 1;
A4:
b = (a * (b div a)) + (b mod a)
by A1, NAT_D:2;
then A5:
ex k being Nat st S1[k]
by A3;
consider k being Nat such that
A6:
S1[k]
and
A7:
for n being Nat st S1[n] holds
k <= n
from NAT_1:sch 5(A5);
now per cases
( k = 0 or k <> 0 )
;
suppose A8:
k = 0
;
:: thesis: a divides bA9:
now assume A10:
0 <> (q |^ (b mod a)) -' 1
;
:: thesis: contradictionthen A11:
0 < (q |^ (b mod a)) -' 1
;
b mod a < a
by A1, NAT_D:1;
then consider m being
Nat such that A12:
a = (b mod a) + m
by NAT_1:10;
A13:
m <> 0
by A1, A12, NAT_D:1;
A14:
q |^ ((b mod a) + m) = q #Z ((b mod a) + m)
by PREPOWER:46;
A15:
q #Z ((b mod a) + m) = (q #Z (b mod a)) * (q #Z m)
by A2, PREPOWER:54;
A16:
q #Z (b mod a) = q |^ (b mod a)
by PREPOWER:46;
A17:
q #Z m = q |^ m
by PREPOWER:46;
A18:
q #Z (b mod a) > 0
by A2, PREPOWER:49;
A19:
q |^ m >= 1
by A2, PREPOWER:19;
m in NAT
by ORDINAL1:def 13;
then
q |^ m <> 1
by A2, A13, Th1;
then
q |^ m > 1
by A19, XXREAL_0:1;
then A20:
q |^ (b mod a) < q |^ a
by A12, A14, A15, A16, A17, A18, XREAL_1:157;
then
0 + 1
<= q |^ a
by NAT_1:13;
then
(q |^ a) -' 1
= (q |^ a) - 1
by XREAL_1:235;
then A21:
(q |^ a) -' 1
= (q |^ a) + (- 1)
;
0 + 1
<= q |^ (b mod a)
by A10, NAT_2:10;
then
(q |^ (b mod a)) -' 1
= (q |^ (b mod a)) - 1
by XREAL_1:235;
then
(q |^ (b mod a)) -' 1
= (q |^ (b mod a)) + (- 1)
;
then
(q |^ (b mod a)) -' 1
< (q |^ a) -' 1
by A20, A21, XREAL_1:10;
hence
contradiction
by A6, A8, A11, NAT_D:7;
:: thesis: verum end;
0 < q |^ (b mod a)
by A2, PREPOWER:13;
then
0 + 1
<= q |^ (b mod a)
by NAT_1:13;
then
((q |^ (b mod a)) - 1) + 1
= 1
by A9, XREAL_1:235;
then
b mod a = 0
by A2, Th1;
hence
a divides b
by A4, NAT_D:3;
:: thesis: verum suppose A22:
k <> 0
;
:: thesis: a divides bthen A23:
0 < k
;
consider j being
Nat such that A24:
k = j + 1
by A22, NAT_1:6;
A25:
k - 1
= j
by A24;
0 + 1
<= k
by A23, NAT_1:13;
then A26:
k -' 1
= j
by A25, XREAL_1:235;
set qNaj =
q |^ ((a * j) + (b mod a));
set qNak =
q |^ ((a * k) + (b mod a));
set qNak1 =
q |^ ((a * (k -' 1)) + (b mod a));
A27:
not
(q |^ a) -' 1
divides (q |^ ((a * j) + (b mod a))) -' 1
by A7, A24, XREAL_1:31;
(q |^ a) -' 1
divides - ((q |^ a) -' 1)
by INT_2:14;
then A28:
(q |^ a) -' 1
divides ((q |^ ((a * k) + (b mod a))) -' 1) + (- ((q |^ a) -' 1))
by A6, WSIERP_1:9;
A29:
0 < q |^ ((a * k) + (b mod a))
by A2, PREPOWER:13;
A30:
0 < q |^ a
by A2, PREPOWER:13;
0 + 1
<= q |^ ((a * k) + (b mod a))
by A29, NAT_1:13;
then A31:
(q |^ ((a * k) + (b mod a))) -' 1
= (q |^ ((a * k) + (b mod a))) - 1
by XREAL_1:235;
A32:
0 + 1
<= q |^ a
by A30, NAT_1:13;
((q |^ ((a * k) + (b mod a))) - 1) - ((q |^ a) - 1) = (q |^ ((a * k) + (b mod a))) - (q |^ a)
;
then
((q |^ ((a * k) + (b mod a))) - 1) - ((q |^ a) - 1) = ((q |^ a) * (q |^ ((a * (k -' 1)) + (b mod a)))) - ((q |^ a) * 1)
by A2, A23, Th2;
then A33:
((q |^ ((a * k) + (b mod a))) -' 1) - ((q |^ a) -' 1) = (q |^ a) * ((q |^ ((a * (k -' 1)) + (b mod a))) - 1)
by A31, A32, XREAL_1:235;
0 < q |^ ((a * (k -' 1)) + (b mod a))
by A2, PREPOWER:13;
then
0 + 1
<= q |^ ((a * (k -' 1)) + (b mod a))
by NAT_1:13;
then A34:
((q |^ ((a * k) + (b mod a))) -' 1) - ((q |^ a) -' 1) = (q |^ a) * ((q |^ ((a * (k -' 1)) + (b mod a))) -' 1)
by A33, XREAL_1:235;
0 < q |^ a
by A2, PREPOWER:13;
then
0 + 1
<= q |^ a
by NAT_1:13;
then
((q |^ a) -' 1) + 1
= q |^ a
by XREAL_1:237;
then
(q |^ a) -' 1,
q |^ a are_relative_prime
by PEPIN:1;
hence
a divides b
by A26, A27, A28, A34, INT_2:40;
:: thesis: verum end;
hence
a divides b
; :: thesis: verum