let f be natural-valued increasing Arithmetic_Progression; :: thesis: ( ( for i being Nat st i < 10 holds
f . i is odd Prime ) implies 210 divides difference f )
assume A1: for i being Nat st i < 10 holds
f . i is odd Prime ; :: thesis: 210 divides difference f
reconsider m = f . 0 as Nat ;
difference f = (f . 1) - (f . 0) by NUMBER06:def 5;
then reconsider r = difference f as Nat ;
A2: f = ArProg (m,r) by NUMBER06:6;
set n = 10;
a3: for i being Nat st i < 10 holds
( (ArProg (m,r)) . i is odd & (ArProg (m,r)) . i is prime ) by A1, A2;
then T1: 2 divides r by XPRIMES1:2, SierpinskiTh5;
3 divides r by a3, XPRIMES1:3, SierpinskiTh5;
then T5: 2 * 3 divides r by T1, PEPIN:4, INT_2:30, XPRIMES1:2, XPRIMES1:3;
T3: 5 divides r by a3, XPRIMES1:5, SierpinskiTh5;
7 divides r by a3, XPRIMES1:7, SierpinskiTh5;
then T6: 5 * 7 divides r by PEPIN:4, T3, INT_2:30, XPRIMES1:5, XPRIMES1:7;
( 2,5 are_coprime & 2,7 are_coprime ) by INT_2:30, XPRIMES1:2, XPRIMES1:5, XPRIMES1:7;
then T8: 2,5 * 7 are_coprime by EULER_1:14;
( 3,5 are_coprime & 3,7 are_coprime ) by INT_2:30, XPRIMES1:3, XPRIMES1:5, XPRIMES1:7;
then 3,5 * 7 are_coprime by EULER_1:14;
then 35 * 6 divides r by T5, T6, PEPIN:4, T8, EULER_1:14;
hence 210 divides difference f ; :: thesis: verum