let a, b, c be Nat; :: thesis: ( (a |^ 2) + (b |^ 2) = c |^ 2 implies ( (b |^ 2) mod a = (c |^ 2) mod a & (a |^ 2) mod b = (c |^ 2) mod b ) )
assume A1: (a |^ 2) + (b |^ 2) = c |^ 2 ; :: thesis: ( (b |^ 2) mod a = (c |^ 2) mod a & (a |^ 2) mod b = (c |^ 2) mod b )
A2: ((a |^ 2) + (b |^ 2)) mod a = (((a |^ 2) mod a) + ((b |^ 2) mod a)) mod a by NAT_D:66
.= (b |^ 2) mod a ;
((a |^ 2) + (b |^ 2)) mod b = (((a |^ 2) mod b) + ((b |^ 2) mod b)) mod b by NAT_D:66
.= (a |^ 2) mod b ;
hence ( (b |^ 2) mod a = (c |^ 2) mod a & (a |^ 2) mod b = (c |^ 2) mod b ) by A1, A2; :: thesis: verum