let a, b be non zero Integer; :: thesis: Parity (a gcd b) = min ((Parity a),(Parity b))
reconsider c = a gcd b as non zero Nat ;
A1: ( Parity c = 2 |^ (2 |-count (a gcd b)) & Parity b = 2 |^ (2 |-count b) & Parity a = 2 |^ (2 |-count a) ) by Def1;
not 2 is trivial ;
then 2 |^ (2 |-count (a gcd b)) = 2 |^ (min ((2 |-count a),(2 |-count b))) by CCM
.= min ((2 |^ (2 |-count a)),(2 |^ (2 |-count b))) by MIN1 ;
hence Parity (a gcd b) = min ((Parity a),(Parity b)) by A1; :: thesis: verum