let i be Nat; :: thesis: Fermat 1 divides (3 |^ ((4 * i) + 2)) + 1
defpred S₁[ Nat] means Fermat 1 divides (3 |^ ((4 * $1) + 2)) + 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 1 divides (3 |^ ((4 * n) + 2)) + 1 ; :: thesis: S₁[n + 1]
then consider m being Nat such that
A2: (3 |^ ((4 * n) + 2)) + 1 = (Fermat 1) * m by NAT_D:def 3;
3 |^ (4 * n) >= 3 |^ 0 by PREPOWER:93;
then 3 |^ (4 * n) >= 1 by NEWTON:4;
then (3 |^ (4 * n)) * (3 |^ 2) > 0 * (3 |^ 2) by Lm17, XREAL_1:68;
then 3 |^ ((4 * n) + 2) > 0 by NEWTON:8;
then (3 |^ ((4 * n) + 2)) + 1 > 0 + 1 by XREAL_1:6;
then ((Fermat 1) * m) * 81 > 1 * 81 by A2, XREAL_1:68;
then (((Fermat 1) * m) * 81) / (Fermat 1) > (1 * 81) / (Fermat 1) by XREAL_1:74;
then ((m * (Fermat 1)) * 81) * ((Fermat 1) ") > (1 * 81) / (Fermat 1) ;
then ((m * 81) * ((Fermat 1) ")) * (Fermat 1) > (1 * 81) / (Fermat 1) ;
then ((m * 81) / (Fermat 1)) * (Fermat 1) > (1 * 81) / (Fermat 1) ;
then m * 81 > 81 / 5 by Th51;
then m * 81 > 16 by XXREAL_0:2;
then A3: (m * 81) + (- 16) > 16 + (- 16) by XREAL_1:6;
(3 |^ ((4 * (n + 1)) + 2)) + 1 = (3 |^ (((4 * n) + 2) + 4)) + 1
.= ((((Fermat 1) * m) - 1) * (3 |^ 4)) + 1 by A2, NEWTON:8
.= (Fermat 1) * ((m * 81) - 16) by Lm18, Th51
.= (Fermat 1) * ((m * 81) -' 16) by A3, XREAL_0:def 2 ;
hence S₁[n + 1] by NAT_D:def 3; :: thesis: verum

end;

(3 |^ ((4 * 0) + 2)) + 1 = 5 * 2 by Lm17;
then A4: S₁[ 0 ] by Th51, NAT_D:def 3;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A1);
hence Fermat 1 divides (3 |^ ((4 * i) + 2)) + 1 ; :: thesis: verum