given f being Arithmetic_Progression such that A1: ( difference f = 100 & ex p1, p2, p3 being Prime ex i being Nat st
( p1,p2,p3 are_mutually_distinct & p1 = f . i & p2 = f . (i + 1) & p3 = f . (i + 2) ) ) ; :: thesis: contradiction
reconsider f = f as integer-valued Arithmetic_Progression by A1, LemmaIntProg;
consider p1, p2, p3 being Prime, i being Nat such that
A2: ( p1,p2,p3 are_mutually_distinct & p1 = f . i & p2 = f . (i + 1) & p3 = f . (i + 2) ) by A1;
b1: p2 - p1 = difference f by A2, LemmaDiffConst;
f . ((i + 1) + 1) = p3 by A2;
then b2: p3 - p2 = difference f by A2, LemmaDiffConst;
K1: ( 3 divides p1 + 1 iff 3 divides (p1 + 1) + (3 * 33) ) by LemmaCong;
( 3 divides p1 + 2 iff 3 divides (p1 + 2) + (3 * 66) ) by LemmaCong;

per cases then ( p1 = 3 or p2 = 3 or p3 = 3 ) by LemmaDivides, b1, b2, A1, K1, ThreeConsecutive;

suppose AA: p1 = 3 ; :: thesis: contradiction

203 = 7 * 29 ;
then 7 divides 203 ;
then not 203 is prime ;
hence contradiction by AA, b1, b2, A1; :: thesis: verum

end;

suppose p2 = 3 ; :: thesis: contradiction

then p1 = 3 - 100 by b1, A1;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

suppose p3 = 3 ; :: thesis: contradiction

then p2 = 3 - 100 by b2, A1;
then p2 < 0 ;
hence contradiction ; :: thesis: verum

end;

end;