let F, F1 be FinSequence of INT ; for k, ma being Nat st k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F is_non_decreasing_on 1,k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds
F1 is_non_decreasing_on 1,k + 1
let k, ma be Nat; ( k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F is_non_decreasing_on 1,k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) implies F1 is_non_decreasing_on 1,k + 1 )
assume that
A1:
k + 1 <= len F
and
A2:
ma = min_at (F,(k + 1),(len F))
and
A3:
F is_split_at k
and
A4:
F is_non_decreasing_on 1,k
and
A5:
F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1)))
; F1 is_non_decreasing_on 1,k + 1
A6:
1 <= k + 1
by NAT_1:12;
set Fk = F +* ((k + 1),(F . ma));
A7:
dom F1 = dom (F +* ((k + 1),(F . ma)))
by A5, FUNCT_7:30;
A8:
dom (F +* ((k + 1),(F . ma))) = dom F
by FUNCT_7:30;
then A9:
k + 1 in dom F1
by A1, A7, A6, FINSEQ_3:25;
let i, j be Nat; FINSEQ_6:def 9 ( 1 <= i & i <= j & j <= k + 1 implies F1 . i <= F1 . j )
assume that
A10:
1 <= i
and
A11:
i <= j
and
A12:
j <= k + 1
; F1 . i <= F1 . j
A13:
j <= len F
by A1, A12, XXREAL_0:2;
1 <= j
by A10, A11, XXREAL_0:2;
then A14:
j in dom F1
by A7, A8, A13, FINSEQ_3:25;
per cases
( j < k + 1 or j = k + 1 )
by A12, XXREAL_0:1;
suppose A15:
j < k + 1
;
F1 . i <= F1 . jthen
i < k + 1
by A11, XXREAL_0:2;
then
i <> ma
by A1, A2, A6, Th59;
then A16:
F1 . i =
(F +* ((k + 1),(F . ma))) . i
by A5, FUNCT_7:32
.=
F . i
by A11, A15, FUNCT_7:32
;
j <> ma
by A1, A2, A6, A15, Th59;
then A17:
F1 . j =
(F +* ((k + 1),(F . ma))) . j
by A5, FUNCT_7:32
.=
F . j
by A15, FUNCT_7:32
;
j <= k
by A15, NAT_1:13;
hence
F1 . i <= F1 . j
by A4, A10, A11, A16, A17;
verum end; suppose A18:
j = k + 1
;
F1 . i <= F1 . jthus
F1 . i <= F1 . j
verumproof
per cases
( i < j or i = j )
by A11, XXREAL_0:1;
suppose A19:
i < j
;
F1 . i <= F1 . jthen
i <> ma
by A1, A2, A6, A18, Th59;
then A20:
F1 . i =
(F +* ((k + 1),(F . ma))) . i
by A5, FUNCT_7:32
.=
F . i
by A18, A19, FUNCT_7:32
;
A21:
i <= k
by A18, A19, NAT_1:13;
A22:
k < j
by A18, NAT_1:13;
thus
F1 . i <= F1 . j
verumproof
per cases
( k + 1 = ma or k + 1 <> ma )
;
suppose
k + 1
= ma
;
F1 . i <= F1 . jthen
F1 . j = F . (k + 1)
by A5, A7, A9, A18, FUNCT_7:31;
hence
F1 . i <= F1 . j
by A1, A3, A10, A18, A20, A21, A22;
verum end; suppose A23:
k + 1
<> ma
;
F1 . i <= F1 . jA24:
ma <= len F
by A1, A2, A6, Th59;
k + 1
<= ma
by A1, A2, A6, Th59;
then A25:
k < ma
by NAT_1:13;
F1 . j =
(F +* ((k + 1),(F . ma))) . j
by A5, A18, A23, FUNCT_7:32
.=
F . ma
by A7, A8, A14, A18, FUNCT_7:31
;
hence
F1 . i <= F1 . j
by A3, A10, A20, A21, A25, A24;
verum end;
end; end;
end; end;