let n be Nat; for a, b being non trivial Nat holds
( Px (a,n), Px (b,n) are_congruent_mod a - b & Py (a,n), Py (b,n) are_congruent_mod a - b )
let a, b be non trivial Nat; ( Px (a,n), Px (b,n) are_congruent_mod a - b & Py (a,n), Py (b,n) are_congruent_mod a - b )
defpred S1[ Nat] means ( Px (a,$1), Px (b,$1) are_congruent_mod a - b & Py (a,$1), Py (b,$1) are_congruent_mod a - b );
( Px (a,0) = 1 & 1 = Px (b,0) & Py (a,0) = 0 & 0 = Py (b,0) )
by Th6;
then A1:
S1[ 0 ]
by INT_1:11;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
set A =
(a ^2) -' 1;
set B =
(b ^2) -' 1;
(
(a ^2) -' 1
= (a ^2) - 1 &
(b ^2) -' 1
= (b ^2) - 1 )
by NAT_1:14, XREAL_1:233;
then
((a ^2) -' 1) - ((b ^2) -' 1) = (a - b) * (a + b)
;
then A3:
(a ^2) -' 1,
(b ^2) -' 1
are_congruent_mod a - b
by INT_1:def 5;
a - b = 1
* (a - b)
;
then A4:
a,
b are_congruent_mod a - b
by INT_1:def 5;
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A5:
S1[
n]
;
S1[n + 1]
A6:
(
Px (
a,
(n + 1))
= ((Px (a,n)) * a) + ((Py (a,n)) * ((a ^2) -' 1)) &
Px (
b,
(n + 1))
= ((Px (b,n)) * b) + ((Py (b,n)) * ((b ^2) -' 1)) )
by Th9;
A7:
(Py (a,n)) * ((a ^2) -' 1),
(Py (b,n)) * ((b ^2) -' 1) are_congruent_mod a - b
by A5, A3, INT_1:18;
(Px (a,n)) * a,
(Px (b,n)) * b are_congruent_mod a - b
by A5, A4, INT_1:18;
hence
Px (
a,
(n + 1)),
Px (
b,
(n + 1))
are_congruent_mod a - b
by A6, A7, INT_1:16;
Py (a,(n + 1)), Py (b,(n + 1)) are_congruent_mod a - b
A8:
(
Py (
a,
(n + 1))
= (Px (a,n)) + ((Py (a,n)) * a) &
Py (
b,
(n + 1))
= (Px (b,n)) + ((Py (b,n)) * b) )
by Th9;
(Py (a,n)) * a,
(Py (b,n)) * b are_congruent_mod a - b
by A4, A5, INT_1:18;
hence
Py (
a,
(n + 1)),
Py (
b,
(n + 1))
are_congruent_mod a - b
by A8, A5, INT_1:16;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
hence
( Px (a,n), Px (b,n) are_congruent_mod a - b & Py (a,n), Py (b,n) are_congruent_mod a - b )
; verum