let p, k, m be Nat; :: thesis: (p |^ k) mod m = ((p mod m) |^ k) mod m
defpred S₁[ Nat] means (p |^ $1) mod m = ((p mod m) |^ $1) mod m;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
(p |^ (n + 1)) mod m = ((p |^ n) * (p |^ 1)) mod m by NEWTON:13
.= ((p |^ n) * p) mod m by NEWTON:10
.= (((p |^ n) mod m) * (p mod m)) mod m by EULER_2:11
.= (((p mod m) |^ n) * (p mod m)) mod m by A2, EULER_2:10
.= ((p mod m) |^ (n + 1)) mod m by NEWTON:11 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(p |^ 0 ) mod m = 1 mod m by NEWTON:9;
then A3: S₁[ 0 ] by NEWTON:9;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence (p |^ k) mod m = ((p mod m) |^ k) mod m ; :: thesis: verum