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