let n be Nat; :: thesis: 2 |^ (12 * n),1 are_congruent_mod 13
defpred S₁[ Nat] means 2 |^ (12 * $1),1 are_congruent_mod 13;
A1: S₁[ 0 ]

proof

2 |^ (12 * 0) = 1 by NEWTON:4;
hence 2 |^ (12 * 0),1 are_congruent_mod 13 by INT_1:11; :: thesis: verum

end;

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 A3: S₁[k] ; :: thesis: S₁[k + 1]
A4: 12 * (k + 1) = (12 * k) + (12 * 1) ;
13 * 315 = (2 |^ 12) - 1 by Lm6, Lm1107;
then 2 |^ (12 * 1),1 are_congruent_mod 13 ;
then (2 |^ (12 * k)) * (2 |^ (12 * 1)),1 * 1 are_congruent_mod 13 by A3, INT_1:18;
hence 2 |^ (12 * (k + 1)),1 are_congruent_mod 13 by A4, NEWTON:8; :: thesis: verum

end;

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