let n be Nat; :: thesis: for a, b, k being Integer holds ((a + b) |^ n) mod k = (((a mod k) + (b mod k)) |^ n) mod k
let a, b, k be Integer; :: thesis: ((a + b) |^ n) mod k = (((a mod k) + (b mod k)) |^ n) mod k
set ak = a mod k;
set bk = b mod k;
defpred S₁[ Nat] means ((a + b) |^ $1) mod k = (((a mod k) + (b mod k)) |^ $1) mod k;
A1: S₁[ 0 ]

proof

thus ((a + b) |^ 0) mod k = 1 mod k by NEWTON:4
.= (((a mod k) + (b mod k)) |^ 0) mod k by NEWTON:4 ; :: thesis: verum

end;

A2: for x being Nat st S₁[x] holds
S₁[x + 1]

proof

let x be Nat; :: thesis: ( S₁[x] implies S₁[x + 1] )
assume A3: S₁[x] ; :: thesis: S₁[x + 1]
A4: (a + b) |^ (x + 1) = ((a + b) |^ x) * (a + b) by NEWTON:6;
A5: (a + b) mod k = ((a mod k) + (b mod k)) mod k by NAT_D:66;
thus ((a + b) |^ (x + 1)) mod k = ((((a + b) |^ x) mod k) * ((a + b) mod k)) mod k by A4, NAT_D:67
.= ((((a mod k) + (b mod k)) |^ x) * ((a mod k) + (b mod k))) mod k by A3, A5, NAT_D:67
.= (((a mod k) + (b mod k)) |^ (x + 1)) mod k by NEWTON:6 ; :: thesis: verum

end;

for x being Nat holds S₁[x] from NAT_1:sch 2(A1, A2);
hence ((a + b) |^ n) mod k = (((a mod k) + (b mod k)) |^ n) mod k ; :: thesis: verum