let n be Nat; :: thesis: 2 |^ n,2 |^ (n mod 12) are_congruent_mod 65
defpred S₁[ Nat] means 2 |^ $1,2 |^ ($1 mod 12) are_congruent_mod 65;
A1: S₁[ 0 ] by INT_1:11;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then A3: 2 * (2 |^ k),2 * (2 |^ (k mod 12)) are_congruent_mod 65 by INT_4:11;
A4: 2 |^ ((k mod 12) + 1) = 2 * (2 |^ (k mod 12)) by NEWTON:6;

per cases ( (k + 1) mod 12 = 0 or (k + 1) mod 12 = (k mod 12) + 1 ) by RADIX_1:4;

suppose A5: (k + 1) mod 12 = 0 ; :: thesis: S₁[k + 1]

set d = (k + 1) div 12;
A6: k + 1 = (12 * ((k + 1) div 12)) + ((k + 1) mod 12) by INT_1:59;
(2 |^ 12) |^ ((k + 1) div 12),1 |^ ((k + 1) div 12) are_congruent_mod 65 by Lm1107, Lm1118, GR_CY_3:34;
then 2 |^ (12 * ((k + 1) div 12)),1 are_congruent_mod 65 by NEWTON:9;
hence S₁[k + 1] by A5, A6, NEWTON:4; :: thesis: verum

end;

suppose (k + 1) mod 12 = (k mod 12) + 1 ; :: thesis: S₁[k + 1]

hence S₁[k + 1] by A3, A4, NEWTON:6; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence 2 |^ n,2 |^ (n mod 12) are_congruent_mod 65 ; :: thesis: verum