let n be Nat; :: thesis: for i being Element of n holds { p where p is n -element XFinSequence of NAT : ( ((((p . i) -' 1) !) + 1) mod (p . i) = 0 & p . i > 1 ) } is diophantine Subset of ()
defpred S1[ Nat, Nat, natural object , Nat, Nat, Nat] means 1 * \$3,0 * \$4 are_congruent_mod 1 * \$4;
deffunc H1( Nat, Nat, Nat) -> set = ((\$2 -' 1) !) + 1;
A1: for n being Nat
for i1, i2, i3, i4, i5, i6 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of () by HILB10_3:21;
A2: for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b1 -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of () by Th2;
A3: for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,H1(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of () from let i be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : ( ((((p . i) -' 1) !) + 1) mod (p . i) = 0 & p . i > 1 ) } is diophantine Subset of ()
defpred S2[ XFinSequence of NAT ] means 1 * ((((\$1 . i) -' 1) !) + 1),0 * (\$1 . i) are_congruent_mod 1 * (\$1 . i);
defpred S3[ XFinSequence of NAT ] means \$1 . i > 1;
defpred S4[ XFinSequence of NAT ] means ( S2[\$1] & S3[\$1] );
A4: { q where q is n -element XFinSequence of NAT : S2[q] } is diophantine Subset of () by A3;
A5: { q where q is n -element XFinSequence of NAT : S3[q] } is diophantine Subset of () by Th1;
A6: { q where q is n -element XFinSequence of NAT : ( S2[q] & S3[q] ) } is diophantine Subset of () from defpred S5[ XFinSequence of NAT ] means ( ((((\$1 . i) -' 1) !) + 1) mod (\$1 . i) = 0 & \$1 . i > 1 );
A7: for q being n -element XFinSequence of NAT holds
( S4[q] iff S5[q] )
proof
let q be n -element XFinSequence of NAT ; :: thesis: ( S4[q] iff S5[q] )
hereby :: thesis: ( S5[q] implies S4[q] )
assume A8: S4[q] ; :: thesis: S5[q]
then ((((q . i) -' 1) !) + 1) mod (q . i) = 0 mod (q . i) by NAT_6:11;
hence S5[q] by A8; :: thesis: verum
end;
assume A9: S5[q] ; :: thesis: S4[q]
then ((((q . i) -' 1) !) + 1) mod (q . i) = 0 mod (q . i) ;
hence S4[q] by A9, NAT_6:11; :: thesis: verum
end;
{ q where q is n -element XFinSequence of NAT : S4[q] } = { r where r is n -element XFinSequence of NAT : S5[r] } from hence { p where p is n -element XFinSequence of NAT : ( ((((p . i) -' 1) !) + 1) mod (p . i) = 0 & p . i > 1 ) } is diophantine Subset of () by A6; :: thesis: verum