let A be non trivial Nat; :: thesis: for C being Nat
for B, L being positive Nat holds
( C = Py (A,B) iff ex i, j being positive Nat ex D, E, F, G, H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * i) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * (j - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 ) )
let C be Nat; :: thesis: for B, L being positive Nat holds
( C = Py (A,B) iff ex i, j being positive Nat ex D, E, F, G, H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * i) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * (j - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 ) )
let B, L be positive Nat; :: thesis: ( C = Py (A,B) iff ex i, j being positive Nat ex D, E, F, G, H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * i) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * (j - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 ) )
reconsider L1 = L - 1 as Nat ;
thus ( C = Py (A,B) implies ex i, j being positive Nat ex D, E, F, G, H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * i) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * (j - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 ) ) :: thesis: ( ex i, j being positive Nat ex D, E, F, G, H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * i) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * (j - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 ) implies C = Py (A,B) )

proof

assume C = Py (A,B) ; :: thesis: ex i, j being positive Nat ex D, E, F, G, H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * i) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * (j - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
then consider i, j, D, E, F, G, H, I being Nat such that
A1: ( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * D) * (L1 + 1)) * (C ^2) & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * j) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 ) by Th17;
take i + 1 ; :: thesis: ex j being positive Nat ex D, E, F, G, H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * (j - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
take j + 1 ; :: thesis: ex D, E, F, G, H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * ((j + 1) - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
take D ; :: thesis: ex E, F, G, H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * ((j + 1) - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
take E ; :: thesis: ex F, G, H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * ((j + 1) - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
take F ; :: thesis: ex G, H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * ((j + 1) - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
take G ; :: thesis: ex H, I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * ((j + 1) - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
take H ; :: thesis: ex I being Integer st
( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * ((j + 1) - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
take I ; :: thesis: ( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * ((j + 1) - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 )
thus ( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 & E = (((2 * (i + 1)) * (C ^2)) * L) * D & F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) & H = B + ((2 * ((j + 1) - 1)) * C) & I = (((G ^2) - 1) * (H ^2)) + 1 ) by A1; :: thesis: verum

end;

given i, j being positive Nat, D, E, F, G, H, I being Integer such that A2: ( (D * F) * I is square & F divides H - C & B <= C & D = (((A ^2) - 1) * (C ^2)) + 1 ) and
A3: E = (((2 * i) * (C ^2)) * L) * D and
A4: ( F = (((A ^2) - 1) * (E ^2)) + 1 & G = A + (F * (F - A)) ) and
A5: H = B + ((2 * (j - 1)) * C) and
A6: I = (((G ^2) - 1) * (H ^2)) + 1 ; :: thesis: C = Py (A,B)
reconsider ii = i - 1, jj = j - 1 as Nat ;
( E = (((2 * (ii + 1)) * D) * (L1 + 1)) * (C ^2) & H = B + ((2 * jj) * C) ) by A3, A5;
hence C = Py (A,B) by A2, A4, A6, Th18; :: thesis: verum