let n, k, d be Nat; :: thesis: for p, q, r, s, t being Integer st p divides d & q divides d & r divides d & s divides d & t divides d holds
card ((seq (n,d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq ((n + k),d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))
let p, q, r, s, t be Integer; :: thesis: ( p divides d & q divides d & r divides d & s divides d & t divides d implies card ((seq (n,d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq ((n + k),d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) )
assume A1: ( p divides d & q divides d & r divides d & s divides d & t divides d ) ; :: thesis: card ((seq (n,d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq ((n + k),d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))

per cases ( d = 0 or d > 0 ) ;

suppose d = 0 ; :: thesis: card ((seq (n,d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq ((n + k),d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))

then ( seq (n,d) = {} & {} = seq ((n + k),d) ) by CALCUL_2:2;
hence card ((seq (n,d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq ((n + k),d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) ; :: thesis: verum

end;

suppose A2: d > 0 ; :: thesis: card ((seq (n,d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq ((n + k),d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))

set km = k mod d;
set kd = k div d;
set M = ((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t);
k mod d < d by A2, INT_1:58;
then reconsider dkm = d - (k mod d) as Element of NAT by NAT_1:21;
A3: (seq (n,(k mod d))) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) misses (seq ((n + (k mod d)),dkm)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) by Th75, XBOOLE_1:76;
seq (n,((k mod d) + dkm)) = (seq (n,(k mod d))) \/ (seq ((n + (k mod d)),dkm)) by Th77;
then (seq (n,d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) = ((seq (n,(k mod d))) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) \/ ((seq ((n + (k mod d)),dkm)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) by XBOOLE_1:23;
then A4: card ((seq (n,d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = (card ((seq (n,(k mod d))) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))) + (card ((seq ((n + (k mod d)),dkm)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))) by A3, CARD_2:40;
A5: (seq ((n + k),dkm)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) misses (seq (((n + k) + dkm),(k mod d))) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) by Th75, XBOOLE_1:76;
seq ((n + k),(dkm + (k mod d))) = (seq ((n + k),dkm)) \/ (seq (((n + k) + dkm),(k mod d))) by Th77;
then (seq ((n + k),d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)) = ((seq ((n + k),dkm)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) \/ ((seq (((n + k) + dkm),(k mod d))) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) by XBOOLE_1:23;
then A6: card ((seq ((n + k),d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = (card ((seq ((n + k),dkm)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))) + (card ((seq (((n + k) + dkm),(k mod d))) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t)))) by A5, CARD_2:40;
A7: k = ((k div d) * d) + (k mod d) by A2, INT_1:59;
then A8: (n + (k mod d)) + ((k div d) * d) = n + k ;
( p divides (k div d) * d & q divides (k div d) * d & r divides (k div d) * d & s divides (k div d) * d & t divides (k div d) * d ) by A1, INT_2:2;
then A9: card ((seq ((n + (k mod d)),dkm)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq ((n + k),dkm)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) by A8, Th88;
A10: (n + k) + dkm = n + (((k div d) + 1) * d) by A7;
( p divides ((k div d) + 1) * d & q divides ((k div d) + 1) * d & r divides ((k div d) + 1) * d & s divides ((k div d) + 1) * d & t divides ((k div d) + 1) * d ) by A1, INT_2:2;
hence card ((seq (n,d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) = card ((seq ((n + k),d)) /\ (((((multiples p) \/ (multiples q)) \/ (multiples r)) \/ (multiples s)) \/ (multiples t))) by A4, A6, A9, A10, Th88; :: thesis: verum

end;

end;