let n be Nat; :: thesis: Fermat 2 divides (3 |^ ((16 * n) + 8)) + 1
defpred S₁[ Nat] means Fermat 2 divides (3 |^ ((16 * $1) + 8)) + 1;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume Fermat 2 divides (3 |^ ((16 * n) + 8)) + 1 ; :: thesis: S₁[n + 1]
then consider m being Nat such that
A2: (3 |^ ((16 * n) + 8)) + 1 = (Fermat 2) * m by NAT_D:def 3;
3 |^ (16 * n) >= 3 |^ 0 by PREPOWER:93;
then 3 |^ (16 * n) >= 1 by NEWTON:4;
then (3 |^ (16 * n)) * (3 |^ 8) > 0 * (3 |^ 8) by Lm19, XREAL_1:68;
then 3 |^ ((16 * n) + 8) > 0 by NEWTON:8;
then (3 |^ ((16 * n) + 8)) + 1 > 0 + 1 by XREAL_1:6;
then ((Fermat 2) * m) * 6561 > 1 * 6561 by A2, XREAL_1:68;
then (((Fermat 2) * m) * 6561) * 6561 > 6561 * 6561 by XREAL_1:68;
then (((Fermat 2) * m) * 6561) * 6561 > 6562 * 6560 by XXREAL_0:2;
then ((((Fermat 2) * m) * 6561) * 6561) / (Fermat 2) > (6560 * 6562) / (Fermat 2) by XREAL_1:74;
then (((m * 6561) * (Fermat 2)) * 6561) * ((Fermat 2) ") > (6560 * 6562) / (Fermat 2) ;
then (((m * 6561) * 6561) * ((Fermat 2) ")) * (Fermat 2) > (6560 * 6562) / (Fermat 2) ;
then (((m * 6561) * 6561) / (Fermat 2)) * (Fermat 2) > (6560 * 6562) / (Fermat 2) ;
then (m * 6561) * 6561 > (6560 * 6562) / 17 by Th52;
then A3: ((m * 6561) * 6561) - (386 * 6560) > (386 * 6560) - (386 * 6560) by XREAL_1:9;
(3 |^ ((16 * (n + 1)) + 8)) + 1 = (3 |^ (((16 * n) + 8) + 16)) + 1
.= ((((Fermat 2) * m) - 1) * (3 |^ 16)) + 1 by A2, NEWTON:8
.= (Fermat 2) * (((m * 6561) * 6561) - (386 * 6560)) by Lm20, Th52
.= (Fermat 2) * (((m * 6561) * 6561) -' (386 * 6560)) by A3, XREAL_0:def 2 ;
hence S₁[n + 1] by NAT_D:def 3; :: thesis: verum

end;

(3 |^ ((16 * 0) + 8)) + 1 = 17 * 386 by Lm19;
then A4: S₁[ 0 ] by Th52, NAT_D:def 3;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A1);
hence Fermat 2 divides (3 |^ ((16 * n) + 8)) + 1 ; :: thesis: verum