let q, a, b be Element of NAT ; ( 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
; 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 a divides bper cases
( k = 0 or k <> 0 )
;
suppose A8:
k = 0
;
a divides bA9:
now not 0 <> (q |^ (b mod a)) -' 1assume A10:
0 <> (q |^ (b mod a)) -' 1
;
contradiction
b mod a < a
by A1, NAT_D:1;
then consider m being
Nat such that A11:
a = (b mod a) + m
by NAT_1:10;
A12:
m <> 0
by A1, A11, NAT_D:1;
A13:
q |^ ((b mod a) + m) = q #Z ((b mod a) + m)
by PREPOWER:36;
A14:
q #Z ((b mod a) + m) = (q #Z (b mod a)) * (q #Z m)
by A2, PREPOWER:44;
A15:
q #Z (b mod a) = q |^ (b mod a)
by PREPOWER:36;
A16:
q #Z m = q |^ m
by PREPOWER:36;
A17:
q |^ m >= 1
by A2, PREPOWER:11;
m in NAT
by ORDINAL1:def 12;
then
q |^ m <> 1
by A2, A12, Th1;
then
q |^ m > 1
by A17, XXREAL_0:1;
then A18:
q |^ (b mod a) < q |^ a
by A2, A11, A13, A14, A15, A16, PREPOWER:39, XREAL_1:155;
then
0 + 1
<= q |^ a
by NAT_1:13;
then
(q |^ a) -' 1
= (q |^ a) - 1
by XREAL_1:233;
then A19:
(q |^ a) -' 1
= (q |^ a) + (- 1)
;
0 + 1
<= q |^ (b mod a)
by A10, NAT_2:8;
then
(q |^ (b mod a)) -' 1
= (q |^ (b mod a)) - 1
by XREAL_1:233;
then
(q |^ (b mod a)) -' 1
= (q |^ (b mod a)) + (- 1)
;
then
(q |^ (b mod a)) -' 1
< (q |^ a) -' 1
by A18, A19, XREAL_1:8;
hence
contradiction
by A6, A8, A10, NAT_D:7;
verum end;
0 < q |^ (b mod a)
by A2, PREPOWER:6;
then
0 + 1
<= q |^ (b mod a)
by NAT_1:13;
then
((q |^ (b mod a)) - 1) + 1
= 1
by A9, XREAL_1:233;
then
b mod a = 0
by A2, Th1;
hence
a divides b
by A4, NAT_D:3;
verum suppose A20:
k <> 0
;
a divides bthen consider j being
Nat such that A21:
k = j + 1
by NAT_1:6;
A22:
k - 1
= j
by A21;
0 + 1
<= k
by A20, NAT_1:13;
then A23:
k -' 1
= j
by A22, XREAL_1:233;
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));
A24:
not
(q |^ a) -' 1
divides (q |^ ((a * j) + (b mod a))) -' 1
by A7, A21, XREAL_1:29;
(q |^ a) -' 1
divides - ((q |^ a) -' 1)
by INT_2:10;
then A25:
(q |^ a) -' 1
divides ((q |^ ((a * k) + (b mod a))) -' 1) + (- ((q |^ a) -' 1))
by A6, WSIERP_1:4;
A26:
0 < q |^ ((a * k) + (b mod a))
by A2, PREPOWER:6;
A27:
0 < q |^ a
by A2, PREPOWER:6;
0 + 1
<= q |^ ((a * k) + (b mod a))
by A26, NAT_1:13;
then A28:
(q |^ ((a * k) + (b mod a))) -' 1
= (q |^ ((a * k) + (b mod a))) - 1
by XREAL_1:233;
A29:
0 + 1
<= q |^ a
by A27, 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, A20, Th2;
then A30:
((q |^ ((a * k) + (b mod a))) -' 1) - ((q |^ a) -' 1) = (q |^ a) * ((q |^ ((a * (k -' 1)) + (b mod a))) - 1)
by A28, A29, XREAL_1:233;
0 < q |^ ((a * (k -' 1)) + (b mod a))
by A2, PREPOWER:6;
then
0 + 1
<= q |^ ((a * (k -' 1)) + (b mod a))
by NAT_1:13;
then A31:
((q |^ ((a * k) + (b mod a))) -' 1) - ((q |^ a) -' 1) = (q |^ a) * ((q |^ ((a * (k -' 1)) + (b mod a))) -' 1)
by A30, XREAL_1:233;
0 < q |^ a
by A2, PREPOWER:6;
then
0 + 1
<= q |^ a
by NAT_1:13;
then
((q |^ a) -' 1) + 1
= q |^ a
by XREAL_1:235;
then
(q |^ a) -' 1,
q |^ a are_coprime
by PEPIN:1;
hence
a divides b
by A23, A24, A25, A31, INT_2:25;
verum end;
hence
a divides b
; verum