let f be Arithmetic_Progression; :: thesis: for p1, p2, p3 being Prime st difference f = 10 & ex i being Nat st
( p1 = f . i & p2 = f . (i + 1) & p3 = f . (i + 2) ) holds
p1 = 3
let p1, p2, p3 be Prime; :: thesis: ( difference f = 10 & ex i being Nat st
( p1 = f . i & p2 = f . (i + 1) & p3 = f . (i + 2) ) implies p1 = 3 )
assume A1: ( difference f = 10 & ex i being Nat st
( p1 = f . i & p2 = f . (i + 1) & p3 = f . (i + 2) ) ) ; :: thesis: p1 = 3
consider i being Nat such that
A2: ( p1 = f . i & p2 = f . (i + 1) & p3 = f . (i + 2) ) by A1;
B1: ( 3 divides p1 + 1 iff 3 divides (p1 + 1) + (3 * 3) ) by LemmaCong;
B2: ( 3 divides p1 + 2 iff 3 divides (p1 + 2) + (3 * 6) ) by LemmaCong;
cc: (f . ((i + 1) + 1)) - (f . (i + 1)) = 10 by A1, LemmaDiffConst;
then C2: p2 + 10 = p3 by A2;
c1: (f . (i + 1)) - (f . i) = 10 by A1, LemmaDiffConst;
then CC: ( 3 divides p1 or 3 divides p2 or 3 divides p3 ) by A2, cc, B1, B2, ThreeConsecutive;
C3: not 3 divides p2

proof

assume 3 divides p2 ; :: thesis: contradiction
then p2 = 3 by INT_2:def 4;
then p1 = 3 - 10 by c1, A2;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

not 3 divides p3

proof

assume 3 divides p3 ; :: thesis: contradiction
then ( p3 = 3 or p3 = 1 ) by INT_2:def 4;
then p2 = 3 - 10 by C2, INT_2:def 4;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

hence p1 = 3 by INT_2:def 4, CC, C3; :: thesis: verum