let n be odd Nat; :: thesis: (2 |^ n) mod 3 = 2
consider m being Nat such that
L0: n = (2 * m) + 1 by ABIAN:9;
defpred S₁[ Nat] means (2 |^ ((2 * $1) + 1)) mod 3 = 2;
L1: S₁[ 0 ] by NAT_D:63;
L2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A1: S₁[k] ; :: thesis: S₁[k + 1]
A2: 1 = 1 mod 3 by NAT_D:63
.= ((1 * 3) + 1) mod 3 by NAT_D:21
.= (2 * 2) mod 3
.= (2 |^ 2) mod 3 by NEWTON:81 ;
2 = (2 * 1) mod 3 by NAT_D:63
.= ((2 |^ ((2 * k) + 1)) * (2 |^ 2)) mod 3 by A1, A2, NAT_D:67
.= (2 |^ (((2 * k) + 1) + 2)) mod 3 by NEWTON:8
.= (2 |^ ((2 * (k + 1)) + 1)) mod 3 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for c being Nat holds S₁[c] from NAT_1:sch 2(L1, L2);
hence (2 |^ n) mod 3 = 2 by L0; :: thesis: verum