let a, b be non zero Integer; :: thesis: Parity (a lcm b) = max ((Parity a),(Parity b))
(min ((Parity a),(Parity b))) * (max ((Parity a),(Parity b))) = (Parity a) * (Parity b) by NEWTON04:18
.= ((Parity a) gcd (Parity b)) * ((Parity a) lcm (Parity b)) by NAT_D:29
.= (Parity (a gcd b)) * ((Parity a) lcm (Parity b)) by PGG
.= (min ((Parity a),(Parity b))) * ((Parity a) lcm (Parity b)) by PGC
.= (min ((Parity a),(Parity b))) * (Parity (a lcm b)) by PLG ;
hence Parity (a lcm b) = max ((Parity a),(Parity b)) by XCMPLX_1:5; :: thesis: verum