let n, p be Nat; for a being non trivial Nat holds Px (a,n),(p |^ n) + ((Py (a,n)) * (a - p)) are_congruent_mod (((2 * a) * p) - (p ^2)) - 1
let a be non trivial Nat; Px (a,n),(p |^ n) + ((Py (a,n)) * (a - p)) are_congruent_mod (((2 * a) * p) - (p ^2)) - 1
set D = (a ^2) -' 1;
set P = (((2 * a) * p) - (p ^2)) - 1;
defpred S1[ Nat] means (Px (a,$1)) - ((Py (a,$1)) * (a - p)),p |^ $1 are_congruent_mod (((2 * a) * p) - (p ^2)) - 1;
defpred S2[ Nat] means ( S1[$1] & S1[$1 + 1] );
A1:
S2[ 0 ]
proof
A2:
(
Px (
a,
0)
= 1 &
Py (
a,
0)
= 0 &
p |^ 0 = 1 )
by HILB10_1:3, NEWTON:4;
(
Px (
a,
(0 + 1))
= ((Px (a,0)) * a) + ((Py (a,0)) * ((a ^2) -' 1)) &
Py (
a,
(0 + 1))
= (Px (a,0)) + ((Py (a,0)) * a) )
by HILB10_1:6;
hence
S2[
0 ]
by A2, INT_1:11;
verum
end;
A3:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
set k1 =
k + 1;
set k2 =
(k + 1) + 1;
set X =
Px (
a,
k);
set X1 =
Px (
a,
(k + 1));
set X2 =
Px (
a,
((k + 1) + 1));
set Y =
Py (
a,
k);
set Y1 =
Py (
a,
(k + 1));
set Y2 =
Py (
a,
((k + 1) + 1));
assume A4:
S2[
k]
;
S2[k + 1]
(k + 1) + 1
= k + 2
;
then A5:
(
Px (
a,
((k + 1) + 1))
= ((2 * a) * (Px (a,(k + 1)))) - (Px (a,k)) &
Py (
a,
((k + 1) + 1))
= ((2 * a) * (Py (a,(k + 1)))) - (Py (a,k)) )
by Th12;
A6:
2
* a,2
* a are_congruent_mod (((2 * a) * p) - (p ^2)) - 1
by INT_1:11;
A7:
(2 * a) * ((Px (a,(k + 1))) - ((Py (a,(k + 1))) * (a - p))),
(2 * a) * (p |^ (k + 1)) are_congruent_mod (((2 * a) * p) - (p ^2)) - 1
by A4, A6, INT_1:18;
(Px (a,((k + 1) + 1))) - ((Py (a,((k + 1) + 1))) * (a - p)) = ((2 * a) * ((Px (a,(k + 1))) - ((Py (a,(k + 1))) * (a - p)))) - ((Px (a,k)) - ((Py (a,k)) * (a - p)))
by A5;
then A8:
(Px (a,((k + 1) + 1))) - ((Py (a,((k + 1) + 1))) * (a - p)),
((2 * a) * (p |^ (k + 1))) - (p |^ k) are_congruent_mod (((2 * a) * p) - (p ^2)) - 1
by A7, A4, INT_1:17;
A9:
p |^ (k + 1) = p * (p |^ k)
by NEWTON:6;
A10:
(p ^2) * (p |^ k) =
(p |^ k) * (p |^ 2)
by NEWTON:81
.=
p |^ (k + 2)
by NEWTON:8
;
A11:
(((2 * a) * p) - (p ^2)) - 1
= (((2 * a) * p) - 1) - (p ^2)
;
(
((2 * a) * p) - 1,
p ^2 are_congruent_mod (((2 * a) * p) - (p ^2)) - 1 &
p |^ k,
p |^ k are_congruent_mod (((2 * a) * p) - (p ^2)) - 1 )
by A11, INT_1:def 4, INT_1:11;
then
(((2 * a) * p) - 1) * (p |^ k),
p |^ ((k + 1) + 1) are_congruent_mod (((2 * a) * p) - (p ^2)) - 1
by A10, INT_1:18;
hence
S2[
k + 1]
by A4, A9, A8, INT_1:15;
verum
end;
for k being Nat holds S2[k]
from NAT_1:sch 2(A1, A3);
then
(((2 * a) * p) - (p ^2)) - 1 divides ((Px (a,n)) - ((Py (a,n)) * (a - p))) - (p |^ n)
by INT_1:def 4;
then
(((2 * a) * p) - (p ^2)) - 1 divides (Px (a,n)) - ((p |^ n) + ((Py (a,n)) * (a - p)))
;
hence
Px (a,n),(p |^ n) + ((Py (a,n)) * (a - p)) are_congruent_mod (((2 * a) * p) - (p ^2)) - 1
by INT_1:def 4; verum