let n be Nat; ex k being Nat st
( 17 divides k & k = ((10 |^ ((16 * n) + 9)) - 7) / 3 )
A1:
10 |^ (1 + 1) = 10 * (10 |^ 1)
by NEWTON:6;
100 = (17 * 5) + 15
;
then
( (10 |^ 2) mod 17 = 15 & 15 * 15 = (13 * 17) + 4 )
by A1, NUMBER02:16;
then
( ((10 |^ 2) * (10 |^ 2)) mod 17 = (15 * 15) mod 17 & (15 * 15) mod 17 = 4 & (10 |^ 2) * (10 |^ 2) = 10 |^ (2 + 2) & 16 = (17 * 0) + 16 )
by NUMBER02:16, NAT_D:67, NEWTON:8;
then A2:
( ((10 |^ 4) * (10 |^ 4)) mod 17 = (4 * 4) mod 17 & (4 * 4) mod 17 = 16 & 16 * 16 = (15 * 17) + 1 & (10 |^ 4) * (10 |^ 4) = 10 |^ (4 + 4) )
by NEWTON:8, NUMBER02:16, NAT_D:67;
then
( ((10 |^ 8) * (10 |^ 8)) mod 17 = (16 * 16) mod 17 & (16 * 16) mod 17 = 1 & (10 |^ 8) * (10 |^ 8) = 10 |^ (8 + 8) )
by NEWTON:8, NUMBER02:16, NAT_D:67;
then A3:
( ((10 |^ 16) |^ n) mod 17 = (1 |^ n) mod 17 & (1 |^ n) mod 17 = 1 )
by GR_CY_3:30;
( 10 mod 17 = 10 & 16 * 10 = (17 * 9) + 7 )
by NAT_D:24;
then A4:
( ((10 |^ 8) * 10) mod 17 = (16 * 10) mod 17 & (16 * 10) mod 17 = 7 & (10 |^ 8) * 10 = 10 |^ (8 + 1) )
by A2, NEWTON:6, NUMBER02:16, NAT_D:67;
10 |^ ((16 * n) + 9) =
(10 |^ (16 * n)) * (10 |^ 9)
by NEWTON:8
.=
((10 |^ 16) |^ n) * (10 |^ 9)
by NEWTON:9
;
then
( (10 |^ ((16 * n) + 9)) mod 17 = (1 * 7) mod 17 & 7 mod 17 = 7 )
by A3, A4, NAT_D:67;
then A5:
( ((10 |^ ((16 * n) + 9)) - 7) mod 17 = (7 - 7) mod 17 & (7 - 7) mod 17 = 0 )
by INT_6:7;
value ((<%1%> ^ (((16 * n) + 8) --> 3)),10) = ((10 |^ (((16 * n) + 8) + 1)) - 7) / 3
by Th16;
then reconsider k = ((10 |^ ((16 * n) + 9)) - 7) / 3 as Nat ;
take
k
; ( 17 divides k & k = ((10 |^ ((16 * n) + 9)) - 7) / 3 )
( ((3 * k) * 6) mod 17 = ((6 mod 17) * 0) mod 17 & ((6 mod 17) * 0) mod 17 = 0 & (3 * 6) * k = (3 * k) * 6 )
by A5, NAT_D:67;
then
( 0 = ((18 mod 17) * (k mod 17)) mod 17 & ((17 * 1) + 1) mod 17 = 1 )
by NUMBER02:16, NAT_D:67;
then
k mod 17 = 0
;
hence
( 17 divides k & k = ((10 |^ ((16 * n) + 9)) - 7) / 3 )
by PEPIN:6; verum