let f be natural-valued increasing Arithmetic_Progression; :: thesis: ( ( for i being Nat st i < 10 holds
f . i is odd Prime ) & difference f = 210 implies for f0 being Nat st f0 = f . 0 holds
f0 mod 11 = 1 )
assume A1: for i being Nat st i < 10 holds
f . i is odd Prime ; :: thesis: ( not difference f = 210 or for f0 being Nat st f0 = f . 0 holds
f0 mod 11 = 1 )
assume B1: 210 = difference f ; :: thesis: for f0 being Nat st f0 = f . 0 holds
f0 mod 11 = 1
let f0 be Nat; :: thesis: ( f0 = f . 0 implies f0 mod 11 = 1 )
AA: f = ArProg ((f . 0),(difference f)) by NUMBER06:6;
assume A2: f0 = f . 0 ; :: thesis: f0 mod 11 = 1
then A3: f0 is Prime by A1;
then f0 > 1 by INT_2:def 4;
then R1: f0 >= 1 + 1 by NAT_1:13;
J1: f0 mod 11 <> 0

proof

assume f0 mod 11 = 0 ; :: thesis: contradiction
then 11 divides f0 by PEPIN:6;
then ( f0 = 1 or f0 = 11 ) by A3, INT_2:def 4;
then a3: f . 1 = 11 + (1 * 210) by A3, INT_2:def 4, A2, AA, NUMBER06:7, B1
.= 221 ;
13 divides 13 * 17 ;
then 221 is not Prime by INT_2:def 4;
hence contradiction by A1, a3; :: thesis: verum

end;

JA: f0 mod 11 <> 10

proof

assume K1: f0 mod 11 = 10 ; :: thesis: contradiction
f0 + 210 >= 210 + 2 by R1, XREAL_1:6;
then K0: f0 + 210 <> 11 ;
K2: 210 mod 11 = (100 + (11 * 10)) mod 11
.= (1 + (9 * 11)) mod 11 by NAT_D:21
.= 1 mod 11 by NAT_D:21
.= 1 by NAT_D:24 ;
(f0 + 210) mod 11 = ((f0 mod 11) + (210 mod 11)) mod 11 by NAT_D:66
.= 0 by K2, K1, NAT_D:25 ;
then 11 divides f0 + 210 by PEPIN:6;
then K3: f0 + 210 is not Prime by K0, INT_2:def 4;
difference f = (f . 1) - (f . 0) by NUMBER06:def 5;
hence contradiction by K3, A1, A2, B1; :: thesis: verum

end;

JC: f0 mod 11 <> 9

proof

assume K1: f0 mod 11 = 9 ; :: thesis: contradiction
f0 + (2 * 210) >= (2 * 210) + 2 by R1, XREAL_1:6;
then K0: f0 + (2 * 210) <> 11 ;
k2: (2 * 210) mod 11 = ((210 + 100) + (11 * 10)) mod 11
.= ((210 + 1) + (9 * 11)) mod 11 by NAT_D:21
.= ((19 * 11) + 2) mod 11 by NAT_D:21
.= 2 mod 11 by NAT_D:21
.= 2 by NAT_D:24 ;
(f0 + (2 * 210)) mod 11 = ((f0 mod 11) + ((2 * 210) mod 11)) mod 11 by NAT_D:66
.= 0 by K1, k2, NAT_D:25 ;
then 11 divides f0 + (2 * 210) by PEPIN:6;
then K3: f0 + (2 * 210) is not Prime by K0, INT_2:def 4;
f . 2 = (f . 0) + (2 * (difference f)) by AA, NUMBER06:7;
hence contradiction by A1, K3, A2, B1; :: thesis: verum

end;

JD: f0 mod 11 <> 8

proof

assume K1: f0 mod 11 = 8 ; :: thesis: contradiction
f0 + (3 * 210) >= (3 * 210) + 2 by R1, XREAL_1:6;
then K0: f0 + (3 * 210) <> 11 ;
k2: (3 * 210) mod 11 = (((210 + 210) + 100) + (11 * 10)) mod 11
.= (((210 + 210) + 1) + (9 * 11)) mod 11 by NAT_D:21
.= (212 + (19 * 11)) mod 11 by NAT_D:21
.= ((100 + 2) + (11 * 10)) mod 11 by NAT_D:21
.= ((1 + 2) + (9 * 11)) mod 11 by NAT_D:21
.= (1 + 2) mod 11 by NAT_D:21
.= 3 by NAT_D:24 ;
(f0 + (3 * 210)) mod 11 = ((f0 mod 11) + ((3 * 210) mod 11)) mod 11 by NAT_D:66
.= 0 by K1, k2, NAT_D:25 ;
then 11 divides f0 + (3 * 210) by PEPIN:6;
then K3: f0 + (3 * 210) is not Prime by K0, INT_2:def 4;
f . 3 = (f . 0) + (3 * (difference f)) by AA, NUMBER06:7;
hence contradiction by K3, A1, A2, B1; :: thesis: verum

end;

JB: f0 mod 11 <> 7

proof

assume K1: f0 mod 11 = 7 ; :: thesis: contradiction
f0 + (4 * 210) >= (4 * 210) + 2 by R1, XREAL_1:6;
then K0: f0 + (4 * 210) <> 11 ;
k2: (4 * 210) mod 11 = (4 + (76 * 11)) mod 11
.= 4 mod 11 by NAT_D:21
.= 4 by NAT_D:24 ;
(f0 + (4 * 210)) mod 11 = ((f0 mod 11) + ((4 * 210) mod 11)) mod 11 by NAT_D:66
.= 0 by K1, k2, NAT_D:25 ;
then 11 divides f0 + (4 * 210) by PEPIN:6;
then K3: f0 + (4 * 210) is not Prime by K0, INT_2:def 4;
f . 4 = (f . 0) + (4 * (difference f)) by AA, NUMBER06:7;
hence contradiction by K3, A1, A2, B1; :: thesis: verum

end;

JE: f0 mod 11 <> 6

proof

assume K1: f0 mod 11 = 6 ; :: thesis: contradiction
f0 + (5 * 210) >= (5 * 210) + 2 by R1, XREAL_1:6;
then K0: f0 + (5 * 210) <> 11 ;
k2: (5 * 210) mod 11 = (5 + (95 * 11)) mod 11
.= 5 mod 11 by NAT_D:21
.= 5 by NAT_D:24 ;
(f0 + (5 * 210)) mod 11 = ((f0 mod 11) + ((5 * 210) mod 11)) mod 11 by NAT_D:66
.= 0 by K1, k2, NAT_D:25 ;
then 11 divides f0 + (5 * 210) by PEPIN:6;
then K3: f0 + (5 * 210) is not Prime by K0, INT_2:def 4;
f . 5 = (f . 0) + (5 * 210) by AA, B1, NUMBER06:7;
hence contradiction by K3, A1, A2; :: thesis: verum

end;

JF: f0 mod 11 <> 5

proof

assume K1: f0 mod 11 = 5 ; :: thesis: contradiction
f0 + (6 * 210) >= (6 * 210) + 2 by R1, XREAL_1:6;
then K0: f0 + (6 * 210) <> 11 ;
k2: (6 * 210) mod 11 = (6 + (114 * 11)) mod 11
.= 6 mod 11 by NAT_D:21
.= 6 by NAT_D:24 ;
(f0 + (6 * 210)) mod 11 = ((f0 mod 11) + ((6 * 210) mod 11)) mod 11 by NAT_D:66
.= 0 by K1, k2, NAT_D:25 ;
then 11 divides f0 + (6 * 210) by PEPIN:6;
then K3: f0 + (6 * 210) is not Prime by K0, INT_2:def 4;
f . 6 = (f . 0) + (6 * (difference f)) by AA, NUMBER06:7;
hence contradiction by K3, A1, A2, B1; :: thesis: verum

end;

JG: f0 mod 11 <> 4

proof

assume K1: f0 mod 11 = 4 ; :: thesis: contradiction
f0 + (7 * 210) >= (7 * 210) + 2 by R1, XREAL_1:6;
then K0: f0 + (7 * 210) <> 11 ;
k2: (7 * 210) mod 11 = (7 + (133 * 11)) mod 11
.= 7 mod 11 by NAT_D:21
.= 7 by NAT_D:24 ;
(f0 + (7 * 210)) mod 11 = ((f0 mod 11) + ((7 * 210) mod 11)) mod 11 by NAT_D:66
.= 0 by K1, k2, NAT_D:25 ;
then 11 divides f0 + (7 * 210) by PEPIN:6;
then K3: f0 + (7 * 210) is not Prime by K0, INT_2:def 4;
f . 7 = (f . 0) + (7 * (difference f)) by AA, NUMBER06:7;
hence contradiction by K3, A1, A2, B1; :: thesis: verum

end;

JH: f0 mod 11 <> 3

proof

assume K1: f0 mod 11 = 3 ; :: thesis: contradiction
f0 + (8 * 210) >= (8 * 210) + 2 by R1, XREAL_1:6;
then K0: f0 + (8 * 210) <> 11 ;
k2: (8 * 210) mod 11 = (8 + (152 * 11)) mod 11
.= 8 mod 11 by NAT_D:21
.= 8 by NAT_D:24 ;
(f0 + (8 * 210)) mod 11 = ((f0 mod 11) + ((8 * 210) mod 11)) mod 11 by NAT_D:66
.= 0 by K1, k2, NAT_D:25 ;
then 11 divides f0 + (8 * 210) by PEPIN:6;
then K3: f0 + (8 * 210) is not Prime by K0, INT_2:def 4;
f . 8 = (f . 0) + (8 * (difference f)) by AA, NUMBER06:7;
hence contradiction by K3, A1, A2, B1; :: thesis: verum

end;

JI: f0 mod 11 <> 2

proof

assume K1: f0 mod 11 = 2 ; :: thesis: contradiction
f0 + (9 * 210) >= (9 * 210) + 2 by R1, XREAL_1:6;
then K0: f0 + (9 * 210) <> 11 ;
k2: (9 * 210) mod 11 = (9 + (171 * 11)) mod 11
.= 9 mod 11 by NAT_D:21
.= 9 by NAT_D:24 ;
(f0 + (9 * 210)) mod 11 = ((f0 mod 11) + ((9 * 210) mod 11)) mod 11 by NAT_D:66
.= 0 by NAT_D:25, K1, k2 ;
then 11 divides f0 + (9 * 210) by PEPIN:6;
then K3: f0 + (9 * 210) is not Prime by K0, INT_2:def 4;
f . 9 = (f . 0) + (9 * (difference f)) by AA, NUMBER06:7;
hence contradiction by K3, A1, A2, B1; :: thesis: verum

end;

not not f0 mod (10 + 1) = 0 & ... & not f0 mod (10 + 1) = 10 by NUMBER03:11;
hence f0 mod 11 = 1 by JD, JE, JF, JG, JH, JI, J1, JA, JB, JC; :: thesis: verum