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 ;
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
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 ;
then consider m being Nat such that
A11: a = (b mod a) + m by NAT_1:10;
A12: m <> 0 by ;
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 ;
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 ;
m in NAT by ORDINAL1:def 12;
then q |^ m <> 1 by A2, A12, Th1;
then q |^ m > 1 by ;
then A18: q |^ (b mod a) < q |^ a by ;
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 ;
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 ;
hence contradiction by A6, A8, A10, NAT_D:7; :: thesis: verum
end;
0 < q |^ (b mod a) by ;
then 0 + 1 <= q |^ (b mod a) by NAT_1:13;
then ((q |^ (b mod a)) - 1) + 1 = 1 by ;
then b mod a = 0 by ;
hence a divides b by ; :: 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 ;
then A23: k -' 1 = j by ;
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 ;
(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 ;
A26: 0 < q |^ ((a * k) + (b mod a)) by ;
A27: 0 < q |^ a by ;
0 + 1 <= q |^ ((a * k) + (b mod a)) by ;
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 ;
((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 ;
0 < q |^ ((a * (k -' 1)) + (b mod a)) by ;
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 ;
0 < q |^ a by ;
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 ; :: thesis: verum
end;
end;
end;
hence a divides b ; :: thesis: verum