let n, k be Nat; :: thesis: for a being non trivial Nat holds Py (a,(n * k)),(k * ((Px (a,n)) |^ (k -' 1))) * (Py (a,n)) are_congruent_mod (Py (a,n)) ^2
let a be non trivial Nat; :: thesis: Py (a,(n * k)),(k * ((Px (a,n)) |^ (k -' 1))) * (Py (a,n)) are_congruent_mod (Py (a,n)) ^2
set m = min_Pell's_solution_of ((a ^2) -' 1);
set x = Px (a,n);
set y = Py (a,n);
set s = sqrt ((a ^2) -' 1);
set ys = (Py (a,n)) * (sqrt ((a ^2) -' 1));

per cases ( n = 0 or k = 0 or ( n > 0 & k > 0 ) ) ;

suppose ( n = 0 or k = 0 ) ; :: thesis: Py (a,(n * k)),(k * ((Px (a,n)) |^ (k -' 1))) * (Py (a,n)) are_congruent_mod (Py (a,n)) ^2

then ( ( Py (a,n) = 0 or k = 0 ) & Py (a,(n * k)) = 0 ) by Th6;
hence Py (a,(n * k)),(k * ((Px (a,n)) |^ (k -' 1))) * (Py (a,n)) are_congruent_mod (Py (a,n)) ^2 by INT_1:11; :: thesis: verum

end;

suppose A1: ( n > 0 & k > 0 ) ; :: thesis: Py (a,(n * k)),(k * ((Px (a,n)) |^ (k -' 1))) * (Py (a,n)) are_congruent_mod (Py (a,n)) ^2

set I = ((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k;
A2: (Px (a,n)) + ((Py (a,n)) * (sqrt ((a ^2) -' 1))) = (((min_Pell's_solution_of ((a ^2) -' 1)) `1) + (((min_Pell's_solution_of ((a ^2) -' 1)) `2) * (sqrt ((a ^2) -' 1)))) |^ n by Def2;
A3: (Px (a,(n * k))) + ((Py (a,(n * k))) * (sqrt ((a ^2) -' 1))) = (((min_Pell's_solution_of ((a ^2) -' 1)) `1) + (((min_Pell's_solution_of ((a ^2) -' 1)) `2) * (sqrt ((a ^2) -' 1)))) |^ (n * k) by Def2
.= ((Px (a,n)) + ((Py (a,n)) * (sqrt ((a ^2) -' 1)))) |^ k by A2, NEWTON:9
.= Sum (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k) by NEWTON:30 ;
consider e, o being complex-valued FinSequence such that
A4: ( len e = [\((len (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k)) / 2)/] & len o = [/((len (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k)) / 2)\] ) and
A5: Sum (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k) = (Sum e) + (Sum o) and
A6: for n being Nat holds
( e . n = (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k) . (2 * n) & o . n = (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k) . ((2 * n) - 1) ) by Th2;
A7: len (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k) = k + 1 by NEWTON:def 4;
(sqrt ((a ^2) -' 1)) |^ (1 + 1) = (sqrt ((a ^2) -' 1)) * ((sqrt ((a ^2) -' 1)) |^ 1) by NEWTON:6
.= (sqrt ((a ^2) -' 1)) ^2
.= (a ^2) -' 1 by SQUARE_1:def 2 ;
then A8: ((Py (a,n)) * (sqrt ((a ^2) -' 1))) |^ 2 = ((Py (a,n)) |^ 2) * ((a ^2) -' 1) by NEWTON:7;
rng o c= NAT

proof

let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in rng o or w in NAT )
assume w in rng o ; :: thesis: w in NAT
then consider z being object such that
A9: ( z in dom o & o . z = w ) by FUNCT_1:def 3;
reconsider z = z as Nat by A9;
set Z = (2 * z) - 1;
A10: w = (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k) . ((2 * z) - 1) by A6, A9;
A11: ( 1 <= z & z <= len o ) by A9, FINSEQ_3:25;
A12: 2 * z >= 2 * 1 by XREAL_1:64, A9, FINSEQ_3:25;
then A13: (2 * z) - 1 >= 2 - 1 by XREAL_1:9;
reconsider zz = (2 * z) - 1, m = ((2 * z) - 1) - 1 as Nat by A12;
A14: ((len (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k)) / 2) + 1 = ((len (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k)) + 2) / 2 ;
len o < ((len (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k)) / 2) + 1 by A4, INT_1:def 7;
then z < ((len (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k)) / 2) + 1 by A11, XXREAL_0:2;
then ( 2 * z < (k + 1) + 2 & (k + 1) + 2 = (k + 2) + 1 ) by A7, A14, XREAL_1:79;
then A15: 2 * z <= (k + 1) + 1 by NAT_1:13;
then A16: (2 * z) - 1 <= k + 1 by XREAL_1:20;
reconsider l = (k + 1) - zz as Nat by NAT_1:21, XREAL_1:20, A15;
A17: (2 * z) - 1 in dom (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k) by A16, A7, A13, FINSEQ_3:25;
l = k - m ;
then A18: (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k) . ((2 * z) - 1) = ((k choose m) * ((Px (a,n)) |^ l)) * (((Py (a,n)) * (sqrt ((a ^2) -' 1))) |^ m) by A17, NEWTON:def 4;
reconsider z1 = z - 1 as Nat by A11;
m = 2 * z1 ;
then ((Py (a,n)) * (sqrt ((a ^2) -' 1))) |^ m = (((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ z1 by A8, NEWTON:9;
hence w in NAT by A10, A18, ORDINAL1:def 12; :: thesis: verum

end;

then reconsider o = o as FinSequence of NAT by FINSEQ_1:def 4;
defpred S₁[ object , object ] means ( $2 in NAT & ( for n being Nat st n = $2 holds
( e . $1 = (sqrt ((a ^2) -' 1)) * n & ( for N being Nat st N = $1 holds
( N - 1 is Nat & (2 * N) - 1 is Nat & (k + 1) - (2 * N) is Nat & ( for n1, m, l being Nat st n1 = N - 1 & m = (2 * N) - 1 & l = (k + 1) - (2 * N) holds
$2 = ((k choose m) * ((Px (a,n)) |^ l)) * (((((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ n1) * (Py (a,n))) ) ) ) ) ) );
A19: for n being Nat st n in Seg (len e) holds
ex x being object st S₁[n,x]

proof

let n be Nat; :: thesis: ( n in Seg (len e) implies ex x being object st S₁[n,x] )
assume A20: n in Seg (len e) ; :: thesis: ex x being object st S₁[n,x]
set N = 2 * n;
A21: ( 1 <= n & n <= len e ) by A20, FINSEQ_1:1;
then 2 * n >= 2 * 1 by XREAL_1:64;
then A22: 2 * n >= 1 by XXREAL_0:2;
reconsider m = (2 * n) - 1, n1 = n - 1 as Nat by A21;
len e <= (len (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k)) / 2 by A4, INT_1:def 6;
then n <= (len (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k)) / 2 by A21, XXREAL_0:2;
then A23: 2 * n <= k + 1 by A7, XREAL_1:83;
then reconsider l = (k + 1) - (2 * n) as Nat by NAT_1:21;
take U = ((k choose m) * ((Px (a,n)) |^ l)) * (((((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ n1) * (Py (a,n))); :: thesis: S₁[n,U]
thus U in NAT by ORDINAL1:def 12; :: thesis: for n being Nat st n = U holds
( e . n = (sqrt ((a ^2) -' 1)) * n & ( for N being Nat st N = n holds
( N - 1 is Nat & (2 * N) - 1 is Nat & (k + 1) - (2 * N) is Nat & ( for n1, m, l being Nat st n1 = N - 1 & m = (2 * N) - 1 & l = (k + 1) - (2 * N) holds
U = ((k choose m) * ((Px (a,n)) |^ l)) * (((((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ n1) * (Py (a,n))) ) ) ) )
let u be Nat; :: thesis: ( u = U implies ( e . n = (sqrt ((a ^2) -' 1)) * u & ( for N being Nat st N = n holds
( N - 1 is Nat & (2 * N) - 1 is Nat & (k + 1) - (2 * N) is Nat & ( for n1, m, l being Nat st n1 = N - 1 & m = (2 * N) - 1 & l = (k + 1) - (2 * N) holds
U = ((k choose m) * ((Px (a,n)) |^ l)) * (((((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ n1) * (Py (a,n))) ) ) ) ) )
assume A24: u = U ; :: thesis: ( e . n = (sqrt ((a ^2) -' 1)) * u & ( for N being Nat st N = n holds
( N - 1 is Nat & (2 * N) - 1 is Nat & (k + 1) - (2 * N) is Nat & ( for n1, m, l being Nat st n1 = N - 1 & m = (2 * N) - 1 & l = (k + 1) - (2 * N) holds
U = ((k choose m) * ((Px (a,n)) |^ l)) * (((((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ n1) * (Py (a,n))) ) ) ) )
A25: 2 * n in dom (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k) by A23, A7, A22, FINSEQ_3:25;
l = k - m ;
then A26: (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k) . (2 * n) = ((k choose m) * ((Px (a,n)) |^ l)) * (((Py (a,n)) * (sqrt ((a ^2) -' 1))) |^ m) by A25, NEWTON:def 4;
m = (2 * n1) + 1 ;
then ((Py (a,n)) * (sqrt ((a ^2) -' 1))) |^ m = (((Py (a,n)) * (sqrt ((a ^2) -' 1))) |^ (2 * n1)) * ((Py (a,n)) * (sqrt ((a ^2) -' 1))) by NEWTON:6
.= ((((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ n1) * ((Py (a,n)) * (sqrt ((a ^2) -' 1))) by A8, NEWTON:9 ;
hence e . n = (sqrt ((a ^2) -' 1)) * u by A6, A26, A24; :: thesis: for N being Nat st N = n holds
( N - 1 is Nat & (2 * N) - 1 is Nat & (k + 1) - (2 * N) is Nat & ( for n1, m, l being Nat st n1 = N - 1 & m = (2 * N) - 1 & l = (k + 1) - (2 * N) holds
U = ((k choose m) * ((Px (a,n)) |^ l)) * (((((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ n1) * (Py (a,n))) ) )
let nn be Nat; :: thesis: ( nn = n implies ( nn - 1 is Nat & (2 * nn) - 1 is Nat & (k + 1) - (2 * nn) is Nat & ( for n1, m, l being Nat st n1 = nn - 1 & m = (2 * nn) - 1 & l = (k + 1) - (2 * nn) holds
U = ((k choose m) * ((Px (a,n)) |^ l)) * (((((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ n1) * (Py (a,n))) ) ) )
assume A27: n = nn ; :: thesis: ( nn - 1 is Nat & (2 * nn) - 1 is Nat & (k + 1) - (2 * nn) is Nat & ( for n1, m, l being Nat st n1 = nn - 1 & m = (2 * nn) - 1 & l = (k + 1) - (2 * nn) holds
U = ((k choose m) * ((Px (a,n)) |^ l)) * (((((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ n1) * (Py (a,n))) ) )
( nn - 1 = n1 & (2 * nn) - 1 = m & (k + 1) - (2 * nn) = l ) by A27;
hence ( nn - 1 is Nat & (2 * nn) - 1 is Nat & (k + 1) - (2 * nn) is Nat & ( for n1, m, l being Nat st n1 = nn - 1 & m = (2 * nn) - 1 & l = (k + 1) - (2 * nn) holds
U = ((k choose m) * ((Px (a,n)) |^ l)) * (((((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ n1) * (Py (a,n))) ) ) ; :: thesis: verum

end;

consider p being FinSequence such that
A28: ( dom p = Seg (len e) & ( for n being Nat st n in Seg (len e) holds
S₁[n,p . n] ) ) from FINSEQ_1:sch 1(A19);
rng p c= NAT

proof

let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in rng p or w in NAT )
assume w in rng p ; :: thesis: w in NAT
then ex n being object st
( n in dom p & p . n = w ) by FUNCT_1:def 3;
hence w in NAT by A28; :: thesis: verum

end;

then reconsider p = p as FinSequence of NAT by FINSEQ_1:def 4;
A29: ( dom ((sqrt ((a ^2) -' 1)) * p) = dom p & dom p = dom e ) by A28, VALUED_1:def 5, FINSEQ_1:def 3;
A30: len p = len e by A28, FINSEQ_1:def 3;
for n being Nat st n in dom p holds
e . n = ((sqrt ((a ^2) -' 1)) * p) . n

proof

let n be Nat; :: thesis: ( n in dom p implies e . n = ((sqrt ((a ^2) -' 1)) * p) . n )
assume n in dom p ; :: thesis: e . n = ((sqrt ((a ^2) -' 1)) * p) . n
hence e . n = (sqrt ((a ^2) -' 1)) * (p . n) by A28
.= ((sqrt ((a ^2) -' 1)) * p) . n by VALUED_1:6 ;
:: thesis: verum

end;

then e = (sqrt ((a ^2) -' 1)) * p by A29, FINSEQ_1:13;
then Sum (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k) = (Sum o) + ((sqrt ((a ^2) -' 1)) * (Sum p)) by A5, RVSUM_1:87;
then A31: Py (a,(n * k)) = Sum p by A3, PELLS_EQ:3;
A32: Sum p is Nat by TARSKI:1;
A33: (Py (a,n)) |^ (1 + 1) = (Py (a,n)) * ((Py (a,n)) |^ 1) by NEWTON:6
.= (Py (a,n)) * (Py (a,n)) ;
for n being Nat st 1 < n & n <= len p holds
(p . n) mod ((Py (a,n)) ^2) = 0

proof

let n be Nat; :: thesis: ( 1 < n & n <= len p implies (p . n) mod ((Py (a,n)) ^2) = 0 )
assume A34: ( 1 < n & n <= len p ) ; :: thesis: (p . n) mod ((Py (a,n)) ^2) = 0
then A35: n in Seg (len e) by A28, FINSEQ_3:25;
then S₁[n,p . n] by A28;
then reconsider n1 = n - 1, m = (2 * n) - 1, l = (k + 1) - (2 * n) as Nat ;
A36: p . n = ((k choose m) * ((Px (a,n)) |^ l)) * (((((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ n1) * (Py (a,n))) by A35, A28;
A37: n - 1 > 1 - 1 by A34, XREAL_1:9;
(Py (a,n)) ^2 divides (((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ n1 by A37, NEWTON02:14, A33, INT_1:def 3;
then (Py (a,n)) ^2 divides ((((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ n1) * (Py (a,n)) by NAT_D:9;
then (Py (a,n)) ^2 divides p . n by A36, NAT_D:9;
hence (p . n) mod ((Py (a,n)) ^2) = 0 by INT_1:62, A1; :: thesis: verum

end;

then (Sum p) mod ((Py (a,n)) ^2) = (p . 1) mod ((Py (a,n)) ^2) by Th1;
then ((Sum p) - (p . 1)) mod ((Py (a,n)) ^2) = 0 by A32, INT_4:22, A1;
then (Py (a,n)) ^2 divides (Sum p) - (p . 1) by INT_1:62, A1;
then A38: Sum p,p . 1 are_congruent_mod (Py (a,n)) ^2 by INT_1:def 4;
( len (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k) >= 1 + 1 & 1 + 1 = 2 * 1 ) by XREAL_1:6, A7, A1, NAT_1:14;
then (len (((Px (a,n)),((Py (a,n)) * (sqrt ((a ^2) -' 1)))) In_Power k)) / 2 >= 1 by XREAL_1:77;
then len p >= 1 by INT_1:54, A30, A4;
then A39: 1 in Seg (len e) by A28, FINSEQ_3:25;
then S₁[1,p . 1] by A28;
then reconsider l = (k + 1) - (2 * 1) as Nat ;
A40: k choose 1 = k by NEWTON:23, A1, NAT_1:14;
A41: (((Py (a,n)) |^ 2) * ((a ^2) -' 1)) |^ 0 = 1 by NEWTON:4;
A42: l = k - 1 ;
( 1 - 1 = 0 & (2 * 1) - 1 = 1 ) ;
then p . 1 = (k * ((Px (a,n)) |^ l)) * (1 * (Py (a,n))) by A39, A28, A40, A41;
hence Py (a,(n * k)),(k * ((Px (a,n)) |^ (k -' 1))) * (Py (a,n)) are_congruent_mod (Py (a,n)) ^2 by A42, A31, A38, XREAL_0:def 2; :: thesis: verum

end;

end;