let m be Nat; :: thesis: ( m is odd implies (3 |^ m) mod 4 = 3 )
assume m is odd ; :: thesis: (3 |^ m) mod 4 = 3
then consider n being Nat such that
A1: m = (2 * n) + 1 by ABIAN:9;
ex k being Nat st 3 |^ ((2 * n) + 1) = (4 * k) + 3 by Lm8;
then (3 |^ ((2 * n) + 1)) mod 4 = 3 mod 4 by NAT_D:21;
hence (3 |^ m) mod 4 = 3 by A1, NAT_D:24; :: thesis: verum