let a be even Integer; :: thesis: for b being Integer st a,b are_coprime holds
a + b,a - b are_coprime
let b be Integer; :: thesis: ( a,b are_coprime implies a + b,a - b are_coprime )
assume A1: a,b are_coprime ; :: thesis: a + b,a - b are_coprime
a gcd b is odd by A1;
then reconsider b = b as odd Integer ;
A2: a + b,2 are_coprime by NEWTON03:def 5;
((1 * b) + a) gcd b = a gcd b by NEWTON02:5;
then a + b,b are_coprime by A1;
then A3: a + b,2 * b are_coprime by A2, INT_2:26;
(a + b) gcd (a - b) = (a + b) gcd ((a - b) - (1 * (a + b))) by NEWTON02:5
.= (a + b) gcd (- (2 * b))
.= (a + b) gcd (2 * b) by NEWTON02:1 ;
hence a + b,a - b are_coprime by A3; :: thesis: verum