let n be Nat; :: thesis: ( 5 divides ((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1 iff ( n mod 4 = 0 or n mod 4 = 3 ) )
consider k being Nat such that
A1: ( n = 4 * k or n = (4 * k) + 1 or n = (4 * k) + 2 or n = (4 * k) + 3 ) by NUMBER02:24;
A2: (4 * k) + 0 = 4 * k ;
thus ( not 5 divides H₂(n) or n mod 4 = 0 or n mod 4 = 3 ) :: thesis: ( ( n mod 4 = 0 or n mod 4 = 3 ) implies 5 divides ((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1 )

proof

assume 5 divides H₂(n) ; :: thesis: ( n mod 4 = 0 or n mod 4 = 3 )
then H₂(n) mod 5 = 0 by INT_1:62;
hence ( n mod 4 = 0 or n mod 4 = 3 ) by A1, A2, Lm8, Lm35, Lm36, NAT_D:21; :: thesis: verum

end;

A3: H₂(4 * k) mod 5 = 0 by Lm34;
H₂((4 * k) + 3) mod 5 = 0 by Lm37;
hence ( ( n mod 4 = 0 or n mod 4 = 3 ) implies 5 divides ((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1 ) by A1, A3, Lm6, Lm7, NAT_D:21, INT_1:62; :: thesis: verum