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 f . 0 >= 199 )
assume A1: for i being Nat st i < 10 holds
f . i is odd Prime ; :: thesis: ( not difference f = 210 or f . 0 >= 199 )
then L1: f . 0 is odd Prime ;
assume KK: difference f = 210 ; :: thesis: f . 0 >= 199
AA: f = ArProg ((f . 0),(difference f)) by NUMBER06:6;
f . 0 is odd by A1;
then T1: (f . 0) mod 2 = 1 by NAT_2:22;
wv: (f . 0) mod 11 = 1 by A1, KK, Diff210Mod11;
then WV: (f . 0) mod 22 = 1 by T1, Mod22;
h3: ( (f . 0) div 22 = 0 implies f . 0 = 1 )

proof

assume H1: (f . 0) div 22 = 0 ; :: thesis: f . 0 = 1
f . 0 = (22 * ((f . 0) div 22)) + ((f . 0) mod 22) by NAT_D:2
.= 1 by wv, H1, T1, Mod22 ;
hence f . 0 = 1 ; :: thesis: verum

end;

h2: ( (f . 0) div 22 = 1 implies f . 0 = 23 )

proof

assume H1: (f . 0) div 22 = 1 ; :: thesis: f . 0 = 23
f . 0 = (22 * ((f . 0) div 22)) + ((f . 0) mod 22) by NAT_D:2
.= 23 by WV, H1 ;
hence f . 0 = 23 ; :: thesis: verum

end;

vw: 5 divides 5 * 9 ;
h1: ( (f . 0) div 22 = 2 implies f . 0 = 45 )

proof

assume H1: (f . 0) div 22 = 2 ; :: thesis: f . 0 = 45
f . 0 = (22 * ((f . 0) div 22)) + ((f . 0) mod 22) by NAT_D:2
.= 45 by WV, H1 ;
hence f . 0 = 45 ; :: thesis: verum

end;

h4: ( (f . 0) div 22 = 3 implies f . 0 = 67 )

proof

assume H1: (f . 0) div 22 = 3 ; :: thesis: f . 0 = 67
f . 0 = (22 * ((f . 0) div 22)) + ((f . 0) mod 22) by NAT_D:2
.= 67 by WV, H1 ;
hence f . 0 = 67 ; :: thesis: verum

end;

h5: ( (f . 0) div 22 = 4 implies f . 0 = 89 )

proof

assume H1: (f . 0) div 22 = 4 ; :: thesis: f . 0 = 89
f . 0 = (22 * ((f . 0) div 22)) + ((f . 0) mod 22) by NAT_D:2
.= 89 by WV, H1 ;
hence f . 0 = 89 ; :: thesis: verum

end;

kc: 3 divides 3 * 37 ;
h6: ( (f . 0) div 22 = 5 implies f . 0 = 111 )

proof

assume H1: (f . 0) div 22 = 5 ; :: thesis: f . 0 = 111
f . 0 = (22 * ((f . 0) div 22)) + ((f . 0) mod 22) by NAT_D:2
.= 111 by WV, H1 ;
hence f . 0 = 111 ; :: thesis: verum

end;

kd: 7 divides 7 * 19 ;
h7: ( (f . 0) div 22 = 6 implies f . 0 = 133 )

proof

assume H1: (f . 0) div 22 = 6 ; :: thesis: f . 0 = 133
f . 0 = (22 * ((f . 0) div 22)) + ((f . 0) mod 22) by NAT_D:2
.= 133 by WV, H1 ;
hence f . 0 = 133 ; :: thesis: verum

end;

kb: 5 divides 5 * 31 ;
h8: ( (f . 0) div 22 = 7 implies f . 0 = 155 )

proof

assume H1: (f . 0) div 22 = 7 ; :: thesis: f . 0 = 155
f . 0 = (22 * ((f . 0) div 22)) + ((f . 0) mod 22) by NAT_D:2
.= 155 by WV, H1 ;
hence f . 0 = 155 ; :: thesis: verum

end;

ka: 3 divides 3 * 59 ;
h9: ( (f . 0) div 22 = 8 implies f . 0 = 177 )

proof

assume H1: (f . 0) div 22 = 8 ; :: thesis: f . 0 = 177
f . 0 = (22 * ((f . 0) div 22)) + ((f . 0) mod 22) by NAT_D:2
.= 177 by WV, H1 ;
hence f . 0 = 177 ; :: thesis: verum

end;

hh: ( (f . 0) div 22 > 4 implies f . 0 >= 199 )

proof

assume (f . 0) div 22 > 4 ; :: thesis: f . 0 >= 199
then (f . 0) div 22 >= 4 + 1 by NAT_1:13;
then ( not not (f . 0) div 22 = 5 + 0 & ... & not (f . 0) div 22 = 5 + 3 or (f . 0) div 22 > 8 ) by NAT_1:62;
then (f . 0) div 22 >= 8 + 1 by NAT_1:13, h7, kd, h6, kc, h8, kb, ka, h9, L1, INT_2:def 4;
then 22 * ((f . 0) div 22) >= 22 * 9 by XREAL_1:64;
then (22 * ((f . 0) div 22)) + 1 >= 198 + 1 by XREAL_1:6;
hence f . 0 >= 199 by WV, NAT_D:2; :: thesis: verum

end;

W1: f . 0 <> 23

proof

assume L1: f . 0 = 23 ; :: thesis: contradiction
O2: f . 5 = (f . 0) + (5 * (difference f)) by AA, NUMBER06:7
.= 29 * 37 by L1, KK ;
then O1: 29 divides f . 5 ;
f . 5 is Prime by A1;
hence contradiction by O2, O1, INT_2:def 4; :: thesis: verum

end;

xx: ( (f . 0) div 22 <= 4 implies not not (f . 0) div 22 = 0 & ... & not (f . 0) div 22 = 4 ) ;
W2: f . 0 <> 67

proof

assume L1: f . 0 = 67 ; :: thesis: contradiction
O2: f . 3 = (f . 0) + (3 * (difference f)) by AA, NUMBER06:7
.= 17 * 41 by L1, KK ;
then O1: 17 divides f . 3 ;
f . 3 is Prime by A1;
hence contradiction by O2, O1, INT_2:def 4; :: thesis: verum

end;

f . 0 <> 89

proof

assume L1: f . 0 = 89 ; :: thesis: contradiction
O2: f . 1 = (f . 0) + (1 * (difference f)) by AA, NUMBER06:7
.= 13 * 23 by L1, KK ;
then O1: 13 divides f . 1 ;
f . 1 is Prime by A1;
hence contradiction by O1, O2, INT_2:def 4; :: thesis: verum

end;

hence f . 0 >= 199 by W2, xx, h1, h2, h3, h4, h5, hh, W1, vw, L1, INT_2:def 4; :: thesis: verum