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: S₁[ 0 ]

proof

(3 |^ ((16 * 0 ) + 8)) + 1 = 17 * 386 by Lm23;
hence S₁[ 0 ] by Th57, NAT_D:def 3; :: thesis: verum

end;

A2: 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
A3: (3 |^ ((16 * n) + 8)) + 1 = (Fermat 2) * m by NAT_D:def 3;
A4: ((m * 6561) * 6561) - (386 * 6560) > 0

proof

3 |^ (16 * n) >= 3 |^ 0 by PREPOWER:107;
then 3 |^ (16 * n) >= 1 by NEWTON:9;
then (3 |^ (16 * n)) * (3 |^ 8) > 0 * (3 |^ 8) by Lm23, XREAL_1:70;
then 3 |^ ((16 * n) + 8) > 0 by NEWTON:13;
then (3 |^ ((16 * n) + 8)) + 1 > 0 + 1 by XREAL_1:8;
then ((Fermat 2) * m) * 6561 > 1 * 6561 by A3, XREAL_1:70;
then (((Fermat 2) * m) * 6561) * 6561 > 6561 * 6561 by XREAL_1:70;
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:76;
then (((m * 6561) * (Fermat 2)) * 6561) * ((Fermat 2) " ) > (6560 * 6562) / (Fermat 2) by XCMPLX_0:def 9;
then (((m * 6561) * 6561) * ((Fermat 2) " )) * (Fermat 2) > (6560 * 6562) / (Fermat 2) ;
then (((m * 6561) * 6561) / (Fermat 2)) * (Fermat 2) > (6560 * 6562) / (Fermat 2) by XCMPLX_0:def 9;
then (m * 6561) * 6561 > (6560 * 6562) / 17 by Th57, XCMPLX_1:88;
then ((m * 6561) * 6561) - (386 * 6560) > (386 * 6560) - (386 * 6560) by XREAL_1:11;
hence ((m * 6561) * 6561) - (386 * 6560) > 0 ; :: thesis: verum

end;

(3 |^ ((16 * (n + 1)) + 8)) + 1 = (3 |^ (((16 * n) + 8) + 16)) + 1
.= ((((Fermat 2) * m) - 1) * (3 |^ 16)) + 1 by A3, NEWTON:13
.= (Fermat 2) * (((m * 6561) * 6561) - (386 * 6560)) by Lm24, Th57
.= (Fermat 2) * (((m * 6561) * 6561) -' (386 * 6560)) by A4, XREAL_0:def 2 ;
hence S₁[n + 1] by NAT_D:def 3; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence Fermat 2 divides (3 |^ ((16 * n) + 8)) + 1 ; :: thesis: verum