let n be Nat; :: thesis: ( 5 divides ((2 |^ ((2 * n) + 1)) - (2 |^ (n + 1))) + 1 iff ( n mod 4 = 1 or n mod 4 = 2 ) )
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;
thus ( not 5 divides H₁(n) or n mod 4 = 1 or n mod 4 = 2 ) :: thesis: ( ( n mod 4 = 1 or n mod 4 = 2 ) implies 5 divides ((2 |^ ((2 * n) + 1)) - (2 |^ (n + 1))) + 1 )

proof

assume 5 divides H₁(n) ; :: thesis: ( n mod 4 = 1 or n mod 4 = 2 )
then H₁(n) mod 5 = 0 by INT_1:62;
hence ( n mod 4 = 1 or n mod 4 = 2 ) by A1, Lm6, Lm7, Lm34, Lm37, NAT_D:21; :: thesis: verum

end;

A2: H₁((4 * k) + 1) mod 5 = 0 by Lm35;
A3: H₁((4 * k) + 2) mod 5 = 0 by Lm36;
(4 * k) + 0 = 4 * k ;
hence ( ( n mod 4 = 1 or n mod 4 = 2 ) implies 5 divides ((2 |^ ((2 * n) + 1)) - (2 |^ (n + 1))) + 1 ) by A1, A2, A3, Lm8, NAT_D:21, INT_1:62; :: thesis: verum