let fp be FinSequence of NAT ; 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; 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 ; ( 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
; 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:27;
A7:
a >= 1
by A1, FINSEQ_3:27;
A8:
b >= 1
by A2, FINSEQ_3:27;
A9:
(len (Del fp,a)) + 1 = n + 1
by A1, A5, WSIERP_1:def 1;
A10:
b <= n + 1
by A2, A5, FINSEQ_3:27;
per cases
( a <= n or a = n + 1 )
by A6, NAT_1:8;
suppose A11:
a <= n
;
fp . b divides Product (Del fp,a)per cases
( b < a or a < b )
by A3, XXREAL_0:1;
suppose A14:
a < b
;
fp . b divides Product (Del fp,a)then
b >= a + 1
by NAT_1:13;
then
b - 1
>= a
by XREAL_1:21;
then
b -' 1
>= a
by A8, XREAL_1:235;
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:52;
then
b -' 1
> 0
by A8, XREAL_1:235;
then A16:
b -' 1
>= 1
by Lm7;
b - 1
<= (n + 1) - 1
by A10, XREAL_1:11;
then
b -' 1
<= n
by A8, XREAL_1:235;
then
b -' 1
in dom (Del fp,a)
by A9, A16, FINSEQ_3:27;
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:237;
verum end; suppose A17:
a = n + 1
;
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:27;
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;
verum end;