let n be Nat; :: thesis: ( n + 1 is Prime implies ReciProducts (n + 1) = { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X } )
assume A0: n + 1 is Prime ; :: thesis: ReciProducts (n + 1) = { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X }
T1: ReciProducts (n + 1) c= { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ReciProducts (n + 1) or x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X } )
assume x in ReciProducts (n + 1) ; :: thesis: x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X }
then consider X being Subset of (SetPrimes (n + 1)) such that
A1: x = 1 / (Product (Sgm X)) ;
X c= SetPrimes (n + 1) ;
then A2: X c= (SetPrimes n) \/ {(n + 1)} by A0, PrimesSet2;

per cases ( n + 1 in X or not n + 1 in X ) ;

suppose n + 1 in X ; :: thesis: x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X }

then x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X } by A1;
hence x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X } by XBOOLE_0:def 3; :: thesis: verum

end;

suppose SS: not n + 1 in X ; :: thesis: x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X }

then X c= SetPrimes n by A2, ZFMISC_1:135;
then x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } by SS, A1;
hence x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X } by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

{ (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X } c= ReciProducts (n + 1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X } or x in ReciProducts (n + 1) )
assume x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X } ; :: thesis: x in ReciProducts (n + 1)

per cases then ( x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } or x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X } ) by XBOOLE_0:def 3;

suppose x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } ; :: thesis: x in ReciProducts (n + 1)

then consider X being Subset of (SetPrimes n) such that
I1: ( x = 1 / (Product (Sgm X)) & not n + 1 in X ) ;
n <= n + 1 by NAT_1:13;
then SetPrimes n c= SetPrimes (n + 1) by XBOOLE_1:26, FINSEQ_1:5;
then X c= SetPrimes (n + 1) ;
hence x in ReciProducts (n + 1) by I1; :: thesis: verum

end;

suppose x in { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X } ; :: thesis: x in ReciProducts (n + 1)

then consider X being Subset of (SetPrimes (n + 1)) such that
B1: ( x = 1 / (Product (Sgm X)) & n + 1 in X ) ;
thus x in ReciProducts (n + 1) by B1; :: thesis: verum

end;

end;

end;

hence ReciProducts (n + 1) = { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes n) : not n + 1 in X } \/ { (1 / (Product (Sgm X))) where X is Subset of (SetPrimes (n + 1)) : n + 1 in X } by T1, TARSKI:2; :: thesis: verum