let a, b be Integer; :: thesis: (Parity a) gcd (Parity b) = Parity (a gcd b)
|.a.| in NAT by INT_1:3;
then reconsider k = |.a.| as Nat ;
|.b.| in NAT by INT_1:3;
then reconsider l = |.b.| as Nat ;

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

suppose A1: a = 0 ; :: thesis: (Parity a) gcd (Parity b) = Parity (a gcd b)

then Parity a = 0 by Def1;
then (Parity a) gcd (Parity b) = Parity (k gcd l) by A1, PMP;
hence (Parity a) gcd (Parity b) = Parity (a gcd b) by INT_2:34; :: thesis: verum

end;

suppose A1: b = 0 ; :: thesis: (Parity a) gcd (Parity b) = Parity (a gcd b)

then Parity b = 0 by Def1;
then (Parity a) gcd (Parity b) = Parity (k gcd l) by A1, PMP;
hence (Parity a) gcd (Parity b) = Parity (a gcd b) by INT_2:34; :: thesis: verum

end;

suppose A0: ( a <> 0 & b <> 0 ) ; :: thesis: (Parity a) gcd (Parity b) = Parity (a gcd b)

reconsider a = a as non zero Integer by A0;
reconsider b = b as non zero Integer by A0;

per cases ( Parity a divides Parity b or Parity b divides Parity a ) by Th4;

suppose B1: Parity a divides Parity b ; :: thesis: (Parity a) gcd (Parity b) = Parity (a gcd b)

then B2: Parity a <= Parity b by NAT_D:7;
(Parity a) gcd (Parity b) = |.(Parity a).| by B1
.= min ((Parity a),(Parity b)) by B2, XXREAL_0:def 9
.= Parity (a gcd b) by PGC ;
hence (Parity a) gcd (Parity b) = Parity (a gcd b) ; :: thesis: verum

end;

suppose B1: Parity b divides Parity a ; :: thesis: (Parity a) gcd (Parity b) = Parity (a gcd b)

then B2: Parity a >= Parity b by NAT_D:7;
(Parity a) gcd (Parity b) = |.(Parity b).| by B1
.= min ((Parity a),(Parity b)) by B2, XXREAL_0:def 9
.= Parity (a gcd b) by PGC ;
hence (Parity a) gcd (Parity b) = Parity (a gcd b) ; :: thesis: verum

end;

end;

end;

end;