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

per cases ( ( a <> 0 & b <> 0 ) or a = 0 or b = 0 ) ;

suppose A1: ( a <> 0 & b <> 0 ) ; :: thesis: (Oddity a) gcd (Oddity b) = Oddity (a gcd b)

then reconsider a = a as non zero Integer ;
reconsider b = b as non zero Integer by A1;
A2: Parity ((Oddity a) gcd (Oddity b)) = 1 gcd 1 by NAT_2:def 1;
Oddity (a gcd b) = Oddity (((Parity a) * (Oddity a)) gcd ((Parity b) * (Oddity b)))
.= Oddity (((Parity a) gcd ((Parity b) * (Oddity b))) * ((Oddity a) gcd ((Parity b) * (Oddity b)))) by OPC, NEWTON03:35
.= Oddity ((((Parity a) gcd (Parity b)) * ((Parity a) gcd (Oddity b))) * ((Oddity a) gcd ((Parity b) * (Oddity b)))) by OPC, NEWTON03:35
.= Oddity ((((Parity a) gcd (Parity b)) * 1) * ((Oddity a) gcd ((Parity b) * (Oddity b)))) by OPC
.= Oddity (((Parity a) gcd (Parity b)) * (((Oddity a) gcd (Parity b)) * ((Oddity a) gcd (Oddity b)))) by OPC, NEWTON03:35
.= Oddity (((Parity a) gcd (Parity b)) * (1 * ((Oddity a) gcd (Oddity b)))) by OPC
.= (Oddity ((Parity a) gcd (Parity b))) * (Oddity ((Oddity a) gcd (Oddity b))) by ILO
.= (Oddity (Parity (a gcd b))) * (Oddity ((Oddity a) gcd (Oddity b))) by PGG
.= 1 * (Oddity ((Oddity a) gcd (Oddity b))) by OPA ;
hence (Oddity a) gcd (Oddity b) = Oddity (a gcd b) by A2; :: thesis: verum

end;

suppose a = 0 ; :: thesis: (Oddity a) gcd (Oddity b) = Oddity (a gcd b)

then ( Oddity (a gcd b) = Oddity |.b.| & (Oddity a) gcd (Oddity b) = |.(Oddity b).| ) by INT_2:12, NEWTON02:3;
hence (Oddity a) gcd (Oddity b) = Oddity (a gcd b) by OMO; :: thesis: verum

end;

suppose b = 0 ; :: thesis: (Oddity a) gcd (Oddity b) = Oddity (a gcd b)

then ( Oddity (a gcd b) = Oddity |.a.| & (Oddity a) gcd (Oddity b) = |.(Oddity a).| ) by INT_2:12, NEWTON02:3;
hence (Oddity a) gcd (Oddity b) = Oddity (a gcd b) by OMO; :: thesis: verum

end;

end;