let i be Nat; :: thesis: ( not i in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) iff ( not 2 divides i & not 3 divides i & not 5 divides i & not 7 divides i ) )

hereby :: thesis: ( not 2 divides i & not 3 divides i & not 5 divides i & not 7 divides i implies not i in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) )

assume not i in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) ; :: thesis: ( not 2 divides i & not 3 divides i & not 5 divides i & not 7 divides i )
then ( not i in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not i in multiples 7 ) by XBOOLE_0:def 3;
then ( not i in (multiples 2) \/ (multiples 3) & not i in multiples 5 & not i in multiples 7 ) by XBOOLE_0:def 3;
then ( not i in multiples 2 & not i in multiples 3 & not i in multiples 5 & not i in multiples 7 ) by XBOOLE_0:def 3;
hence ( not 2 divides i & not 3 divides i & not 5 divides i & not 7 divides i ) by NUMBER14:62; :: thesis: verum

end;

assume ( not 2 divides i & not 3 divides i & not 5 divides i & not 7 divides i ) ; :: thesis: not i in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)
then A1: ( not i in multiples 2 & not i in multiples 3 & not i in multiples 5 & not i in multiples 7 ) by NUMBER14:62;
then not i in (multiples 2) \/ (multiples 3) by XBOOLE_0:def 3;
then not i in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) by A1, XBOOLE_0:def 3;
hence not i in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) by A1, XBOOLE_0:def 3; :: thesis: verum