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 S₁[ 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 S₁[k] by A3;
consider k being Nat such that
A6: S₁[k] and
A7: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A5);

now :: thesis: a divides b

per cases ( k = 0 or k <> 0 ) ;

suppose A8: k = 0 ; :: thesis: a divides b

A9: now :: thesis: not 0 <> (q |^ (b mod a)) -' 1

assume A10: 0 <> (q |^ (b mod a)) -' 1 ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

suppose A20: k <> 0 ; :: thesis: a divides b

then 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; :: thesis: verum

end;

end;

end;

hence a divides b ; :: thesis: verum