let a, b be non zero Integer; :: thesis: for n being Nat holds min ((Parity (a |^ n)),(Parity (b |^ n))) = (min ((Parity a),(Parity b))) |^ n
let n be Nat; :: thesis: min ((Parity (a |^ n)),(Parity (b |^ n))) = (min ((Parity a),(Parity b))) |^ n
min ((Parity (a |^ n)),(Parity (b |^ n))) = Parity ((a |^ n) gcd (b |^ n)) by PGC
.= Parity ((a gcd b) |^ n) by NEWTON03:4
.= (Parity (a gcd b)) |^ n by PAN ;
hence min ((Parity (a |^ n)),(Parity (b |^ n))) = (min ((Parity a),(Parity b))) |^ n by PGC; :: thesis: verum