let a, b be Integer; :: thesis: (Parity a) lcm (Parity b) = Parity (a lcm 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 or b = 0 ) ; :: thesis: (Parity a) lcm (Parity b) = Parity (a lcm b)

then ( Parity a = 0 or Parity b = 0 ) by Def1;
hence (Parity a) lcm (Parity b) = Parity (a lcm b) by A1; :: thesis: verum

end;

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

reconsider a = a as non zero Integer by A0;
reconsider b = b as non zero Integer by A0;
((Parity a) lcm (Parity b)) * ((Parity a) gcd (Parity b)) = (Parity a) * (Parity b) by NAT_D:29
.= Parity (a * b) by ILP
.= Parity |.(a * b).| by PMP
.= Parity (k * l) by COMPLEX1:65
.= Parity ((k gcd l) * (k lcm l)) by NAT_D:29
.= (Parity (k gcd l)) * (Parity (k lcm l)) by ILP
.= (Parity (a gcd b)) * (Parity (k lcm l)) by INT_2:34
.= (Parity (a gcd b)) * (Parity (a lcm b)) by INT_2:33
.= ((Parity a) gcd (Parity b)) * (Parity (a lcm b)) by PGG ;
hence (Parity a) lcm (Parity b) = Parity (a lcm b) by XCMPLX_1:5; :: thesis: verum

end;

end;