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_{1}[ Nat] means (2 |^ ((2 * $1) + 1)) mod 3 = 2;

L1: S_{1}[ 0 ]
by NAT_D:63;

L2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[c]
from NAT_1:sch 2(L1, L2);

hence (2 |^ n) mod 3 = 2 by L0; :: thesis: verum

consider m being Nat such that

L0: n = (2 * m) + 1 by ABIAN:9;

defpred S

L1: S

L2: for k being Nat st S

S

proof

for c being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A1: S_{1}[k]
; :: thesis: S_{1}[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_{1}[k + 1]
; :: thesis: verum

end;assume A1: S

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

hence (2 |^ n) mod 3 = 2 by L0; :: thesis: verum