let n, n1, n2 be Nat; :: thesis: for a being non trivial Nat st Py (a,n1), Py (a,n2) are_congruent_mod Px (a,n) & n > 0 & not n1,n2 are_congruent_mod 2 * n holds
n1, - n2 are_congruent_mod 2 * n
let a be non trivial Nat; :: thesis: ( Py (a,n1), Py (a,n2) are_congruent_mod Px (a,n) & n > 0 & not n1,n2 are_congruent_mod 2 * n implies n1, - n2 are_congruent_mod 2 * n )
assume that
A1: Py (a,n1), Py (a,n2) are_congruent_mod Px (a,n) and
A2: n > 0 ; :: thesis: ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n )
reconsider m1 = n1 mod (4 * n), d1 = n1 div (4 * n) as Element of NAT ;
A3: n1 - (d1 * (4 * n)) = m1 by A2, INT_1:def 10;
then (sgn (((4 * d1) * n) + m1)) * (Py (a,|.(((4 * d1) * n) + m1).|)),(sgn m1) * (Py (a,|.m1.|)) are_congruent_mod Px (a,|.n.|) by Th31;
then Py (a,n1),(sgn m1) * (Py (a,|.m1.|)) are_congruent_mod Px (a,|.n.|) by A3, Th23;
then Py (a,n1), Py (a,m1) are_congruent_mod Px (a,n) by Th23;
then A4: Py (a,m1), Py (a,n1) are_congruent_mod Px (a,n) by INT_1:14;
reconsider m2 = n2 mod (4 * n), d2 = n2 div (4 * n) as Element of NAT ;
A5: ( m1 <= 4 * n & m2 <= 4 * n ) by A2, INT_1:58;
A6: ( |.(Py (a,m1)).| = Py (a,m1) & |.(Py (a,m2)).| = Py (a,m2) ) ;
A7: n2 - (d2 * (4 * n)) = m2 by A2, INT_1:def 10;
then (sgn (((4 * d2) * n) + m2)) * (Py (a,|.(((4 * d2) * n) + m2).|)),(sgn m2) * (Py (a,|.m2.|)) are_congruent_mod Px (a,|.n.|) by Th31;
then Py (a,n2),(sgn m2) * (Py (a,|.m2.|)) are_congruent_mod Px (a,|.n.|) by A7, Th23;
then Py (a,n2), Py (a,m2) are_congruent_mod Px (a,n) by Th23;
then Py (a,n1), Py (a,m2) are_congruent_mod Px (a,n) by A1, INT_1:15;
then Py (a,m1), Py (a,m2) are_congruent_mod Px (a,n) by A4, INT_1:15;
then A8: ( m1,m2 are_congruent_mod 2 * n or m1, - m2 are_congruent_mod 2 * n ) by A6, A5, Th35;
n1 - m1 = (2 * d1) * (2 * n) by A3;
then n1,m1 are_congruent_mod 2 * n by INT_1:def 5;
then A9: ( n1,m2 are_congruent_mod 2 * n or n1, - m2 are_congruent_mod 2 * n ) by A8, INT_1:15;
( m2 - n2 = (- (2 * d2)) * (2 * n) & (- m2) - (- n2) = (2 * d2) * (2 * n) ) by A7;
then ( m2,n2 are_congruent_mod 2 * n & - m2, - n2 are_congruent_mod 2 * n ) by INT_1:def 5;
hence ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n ) by A9, INT_1:15; :: thesis: verum