let k be Nat; 7 divides (10 |^ ((6 * k) + 4)) + 3
10000 = (1428 * 7) + 4
;
then A1:
10 |^ 4,4 are_congruent_mod 7
by Lm2062;
A2:
7, 0 are_congruent_mod 7
;
per cases
( k = 0 or k <> 0 )
;
suppose A4:
k <> 0
;
7 divides (10 |^ ((6 * k) + 4)) + 3
(1 * 7) + 3,7
are_coprime
by Th64, XPRIMES1:3, XPRIMES1:7, INT_2:30;
then A5:
(10 |^ (Euler 7)) mod 7
= 1
by EULER_2:18;
Euler 7
= 7
- 1
by EULER_1:20, XPRIMES1:7;
then A6:
((10 |^ 6) |^ k) mod 7
= 1
by A5, A4, NEWTON05:15;
A7:
1
mod 7
= 1
by NAT_D:24;
(10 |^ 6) |^ k = 10
|^ (6 * k)
by NEWTON:9;
then
10
|^ (6 * k),1
are_congruent_mod 7
by A6, A7, NAT_D:64;
then A8:
(10 |^ (6 * k)) * (10 |^ 4),1
* 4
are_congruent_mod 7
by A1, INT_1:18;
(10 |^ (6 * k)) * (10 |^ 4) = 10
|^ ((6 * k) + 4)
by NEWTON:8;
then
(10 |^ ((6 * k) + 4)) + 3,4
+ 3
are_congruent_mod 7
by A8;
then
(10 |^ ((6 * k) + 4)) + 3,
0 are_congruent_mod 7
by A2, INT_1:15;
hence
7
divides (10 |^ ((6 * k) + 4)) + 3
;
verum end;