let a, b be Integer; :: thesis: parity (a gcd b) = max ((parity a),(parity b))

per cases ( a is odd or a is even ) ;

suppose A1: a is odd ; :: thesis: parity (a gcd b) = max ((parity a),(parity b))

then a gcd b is odd ;
hence parity (a gcd b) = max ((parity a),(parity b)) by A1, XXREAL_0:def 10, NEWTON03:def 1; :: thesis: verum

end;

suppose A1: a is even ; :: thesis: parity (a gcd b) = max ((parity a),(parity b))

per cases ( b is odd or b is even ) ;

suppose B1: b is odd ; :: thesis: parity (a gcd b) = max ((parity a),(parity b))

then a gcd b is odd ;
hence parity (a gcd b) = max ((parity a),(parity b)) by B1, A1, XXREAL_0:def 10; :: thesis: verum

end;

suppose B1: b is even ; :: thesis: parity (a gcd b) = max ((parity a),(parity b))

then a gcd b is even by A1;
hence parity (a gcd b) = max ((parity a),(parity b)) by B1, A1; :: thesis: verum

end;

end;

end;

end;