let fp be FinSequence of NAT ; :: thesis: for a being Nat

for b being Element of NAT st a in dom fp & b in dom fp & a <> b & len fp >= 1 holds

fp . b divides Product (Del (fp,a))

let a be Nat; :: thesis: for b being Element of NAT st a in dom fp & b in dom fp & a <> b & len fp >= 1 holds

fp . b divides Product (Del (fp,a))

let b be Element of NAT ; :: thesis: ( a in dom fp & b in dom fp & a <> b & len fp >= 1 implies fp . b divides Product (Del (fp,a)) )

assume that

A1: a in dom fp and

A2: b in dom fp and

A3: a <> b and

A4: len fp >= 1 ; :: thesis: fp . b divides Product (Del (fp,a))

consider n being Nat such that

A5: len fp = n + 1 by A4, NAT_1:6;

A6: a <= n + 1 by A1, A5, FINSEQ_3:25;

A7: a >= 1 by A1, FINSEQ_3:25;

A8: b >= 1 by A2, FINSEQ_3:25;

A9: (len (Del (fp,a))) + 1 = n + 1 by A1, A5, WSIERP_1:def 1;

A10: b <= n + 1 by A2, A5, FINSEQ_3:25;

for b being Element of NAT st a in dom fp & b in dom fp & a <> b & len fp >= 1 holds

fp . b divides Product (Del (fp,a))

let a be Nat; :: thesis: for b being Element of NAT st a in dom fp & b in dom fp & a <> b & len fp >= 1 holds

fp . b divides Product (Del (fp,a))

let b be Element of NAT ; :: thesis: ( a in dom fp & b in dom fp & a <> b & len fp >= 1 implies fp . b divides Product (Del (fp,a)) )

assume that

A1: a in dom fp and

A2: b in dom fp and

A3: a <> b and

A4: len fp >= 1 ; :: thesis: fp . b divides Product (Del (fp,a))

consider n being Nat such that

A5: len fp = n + 1 by A4, NAT_1:6;

A6: a <= n + 1 by A1, A5, FINSEQ_3:25;

A7: a >= 1 by A1, FINSEQ_3:25;

A8: b >= 1 by A2, FINSEQ_3:25;

A9: (len (Del (fp,a))) + 1 = n + 1 by A1, A5, WSIERP_1:def 1;

A10: b <= n + 1 by A2, A5, FINSEQ_3:25;

per cases
( a <= n or a = n + 1 )
by A6, NAT_1:8;

end;

suppose A11:
a <= n
; :: thesis: fp . b divides Product (Del (fp,a))

end;

per cases
( b < a or a < b )
by A3, XXREAL_0:1;

end;

suppose A12:
b < a
; :: thesis: fp . b divides Product (Del (fp,a))

then
b <= n
by A11, XXREAL_0:2;

then A13: b in dom (Del (fp,a)) by A8, A9, FINSEQ_3:25;

(Del (fp,a)) . b = fp . b by A1, A12, WSIERP_1:def 1;

hence fp . b divides Product (Del (fp,a)) by A13, Th32; :: thesis: verum

end;then A13: b in dom (Del (fp,a)) by A8, A9, FINSEQ_3:25;

(Del (fp,a)) . b = fp . b by A1, A12, WSIERP_1:def 1;

hence fp . b divides Product (Del (fp,a)) by A13, Th32; :: thesis: verum

suppose A14:
a < b
; :: thesis: fp . b divides Product (Del (fp,a))

then
b >= a + 1
by NAT_1:13;

then b - 1 >= a by XREAL_1:19;

then b -' 1 >= a by A8, XREAL_1:233;

then A15: (Del (fp,a)) . (b -' 1) = fp . ((b -' 1) + 1) by A1, WSIERP_1:def 1;

b > 1 by A7, A14, XXREAL_0:2;

then b - 1 > 0 by XREAL_1:50;

then b -' 1 > 0 by A8, XREAL_1:233;

then A16: b -' 1 >= 1 by Lm7;

b - 1 <= (n + 1) - 1 by A10, XREAL_1:9;

then b -' 1 <= n by A8, XREAL_1:233;

then b -' 1 in dom (Del (fp,a)) by A9, A16, FINSEQ_3:25;

then (Del (fp,a)) . (b -' 1) divides Product (Del (fp,a)) by Th32;

hence fp . b divides Product (Del (fp,a)) by A8, A15, XREAL_1:235; :: thesis: verum

end;then b - 1 >= a by XREAL_1:19;

then b -' 1 >= a by A8, XREAL_1:233;

then A15: (Del (fp,a)) . (b -' 1) = fp . ((b -' 1) + 1) by A1, WSIERP_1:def 1;

b > 1 by A7, A14, XXREAL_0:2;

then b - 1 > 0 by XREAL_1:50;

then b -' 1 > 0 by A8, XREAL_1:233;

then A16: b -' 1 >= 1 by Lm7;

b - 1 <= (n + 1) - 1 by A10, XREAL_1:9;

then b -' 1 <= n by A8, XREAL_1:233;

then b -' 1 in dom (Del (fp,a)) by A9, A16, FINSEQ_3:25;

then (Del (fp,a)) . (b -' 1) divides Product (Del (fp,a)) by Th32;

hence fp . b divides Product (Del (fp,a)) by A8, A15, XREAL_1:235; :: thesis: verum

suppose A17:
a = n + 1
; :: thesis: fp . b divides Product (Del (fp,a))

then
b < n + 1
by A3, A10, XXREAL_0:1;

then b <= n by NAT_1:13;

then A18: b in dom (Del (fp,a)) by A8, A9, FINSEQ_3:25;

b < a by A3, A10, A17, XXREAL_0:1;

then (Del (fp,a)) . b = fp . b by A1, WSIERP_1:def 1;

hence fp . b divides Product (Del (fp,a)) by A18, Th32; :: thesis: verum

end;then b <= n by NAT_1:13;

then A18: b in dom (Del (fp,a)) by A8, A9, FINSEQ_3:25;

b < a by A3, A10, A17, XXREAL_0:1;

then (Del (fp,a)) . b = fp . b by A1, WSIERP_1:def 1;

hence fp . b divides Product (Del (fp,a)) by A18, Th32; :: thesis: verum