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_{1}[ 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_{1}[k]
by A3;

consider k being Nat such that

A6: S_{1}[k]
and

A7: for n being Nat st S_{1}[n] holds

k <= n from NAT_1:sch 5(A5);

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

A4: b = (a * (b div a)) + (b mod a) by A1, NAT_D:2;

then A5: ex k being Nat st S

consider k being Nat such that

A6: S

A7: for n being Nat st S

k <= n from NAT_1:sch 5(A5);

now :: thesis: a divides bend;

hence
a divides b
; :: thesis: verumper cases
( k = 0 or k <> 0 )
;

end;

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

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;

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

0 < q |^ (b mod a)
by A2, PREPOWER:6;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;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

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

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;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