let s be positive Nat; :: thesis: ( s <> 2 implies ex f being s -element natural-valued FinSequence st
( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 ) )
set d = H2(2);
set t = H2(3);
assume s <> 2 ; :: thesis: ex f being s -element natural-valued FinSequence st
( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 )
per cases then ( s = 1 or s = 3 or s = 4 or s >= 5 ) by Lm24;
suppose s = 1 ; :: thesis: ex f being s -element natural-valued FinSequence st
( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 )
then reconsider f = <*H2(1)*> as s -element natural-valued FinSequence ;
take f ; :: thesis: ( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 )
thus f is triangular-valued ; :: thesis: f is with_sum_of_reciprocals_equal_1
thus f is with_sum_of_reciprocals_equal_1 by NUMPOLY1:11; :: thesis: verum
end;
suppose s = 3 ; :: thesis: ex f being s -element natural-valued FinSequence st
( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 )
then reconsider f = <*H2(2),H2(2),H2(2)*> as s -element natural-valued FinSequence ;
take f ; :: thesis: ( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 )
thus f is triangular-valued ; :: thesis: f is with_sum_of_reciprocals_equal_1
thus f is with_sum_of_reciprocals_equal_1 by Th127; :: thesis: verum
end;
suppose s = 4 ; :: thesis: ex f being s -element natural-valued FinSequence st
( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 )
then reconsider f = <*H2(2),H2(2),H2(3),H2(3)*> as s -element natural-valued FinSequence ;
take f ; :: thesis: ( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 )
thus f is triangular-valued ; :: thesis: f is with_sum_of_reciprocals_equal_1
thus f is with_sum_of_reciprocals_equal_1 by Th128; :: thesis: verum
end;
suppose A1: s >= 5 ; :: thesis: ex f being s -element natural-valued FinSequence st
( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 )
per cases ( s is odd or s is even ) ;
suppose s is odd ; :: thesis: ex f being s -element natural-valued FinSequence st
( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 )
then consider q being Nat such that
A2: s = (2 * q) + 1 by ABIAN:9;
set k = q + 1;
A3: now :: thesis: not q + 1 < 2 + 1
assume q + 1 < 2 + 1 ; :: thesis: contradiction
then q + 1 <= 2 by NAT_1:13;
then 2 * (q + 1) <= 2 * 2 by XREAL_1:64;
then (2 * (q + 1)) - 1 <= 4 - 1 by XREAL_1:9;
hence contradiction by A1, A2, XXREAL_0:2; :: thesis: verum
end;
set f1 = <*H2(2)*>;
set f2 = TriangleShift2 ((q + 1),2);
set f3 = ((q + 1) + 1) |-> H2(q + 1);
set f = (<*H2(2)*> ^ (TriangleShift2 ((q + 1),2))) ^ (((q + 1) + 1) |-> H2(q + 1));
A4: len <*H2(2)*> = 1 by CARD_1:def 7;
A5: len (TriangleShift2 ((q + 1),2)) = ((q + 1) - 2) - 1 by A3, Def15;
A6: len (<*H2(2)*> ^ (TriangleShift2 ((q + 1),2))) = (len <*H2(2)*>) + (len (TriangleShift2 ((q + 1),2))) by FINSEQ_1:22;
len ((<*H2(2)*> ^ (TriangleShift2 ((q + 1),2))) ^ (((q + 1) + 1) |-> H2(q + 1))) = (len (<*H2(2)*> ^ (TriangleShift2 ((q + 1),2)))) + (len (((q + 1) + 1) |-> H2(q + 1))) by FINSEQ_1:22
.= s by A2, A4, A5, A6 ;
then reconsider f = (<*H2(2)*> ^ (TriangleShift2 ((q + 1),2))) ^ (((q + 1) + 1) |-> H2(q + 1)) as s -element natural-valued FinSequence by CARD_1:def 7;
take f ; :: thesis: ( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 )
TriangleShift2 ((q + 1),2) is triangular-valued by A3, Th132;
hence f is triangular-valued ; :: thesis: f is with_sum_of_reciprocals_equal_1
A7: <*H2(2)*> " = <*(H2(2) ")*> by NUMBER15:63;
A8: Sum ((TriangleShift2 ((q + 1),2)) ") = (2 / 3) - (((q + 1) + 1) / H2(q + 1)) by A3, Th133;
A9: (((q + 1) + 1) |-> H2(q + 1)) " = ((q + 1) + 1) |-> (H2(q + 1) ") by Th43;
A10: (<*H2(2)*> ^ (TriangleShift2 ((q + 1),2))) " = (<*H2(2)*> ") ^ ((TriangleShift2 ((q + 1),2)) ") by NUMBER15:60;
thus Sum (f ") = Sum (((<*H2(2)*> ^ (TriangleShift2 ((q + 1),2))) ") ^ ((((q + 1) + 1) |-> H2(q + 1)) ")) by NUMBER15:60
.= (Sum ((<*H2(2)*> ^ (TriangleShift2 ((q + 1),2))) ")) + (Sum ((((q + 1) + 1) |-> H2(q + 1)) ")) by RVSUM_2:32
.= ((Sum (<*H2(2)*> ")) + (Sum ((TriangleShift2 ((q + 1),2)) "))) + (Sum ((((q + 1) + 1) |-> H2(q + 1)) ")) by A10, RVSUM_2:32
.= (((H2(2) ") + (2 / 3)) - (((q + 1) + 1) / H2(q + 1))) + (((q + 1) + 1) * (H2(q + 1) ")) by A7, A8, A9, RVSUM_2:36
.= 1 by NUMPOLY1:12 ; :: according to NUMBER17:def 6 :: thesis: verum
end;
suppose s is even ; :: thesis: ex f being s -element natural-valued FinSequence st
( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 )
then consider k being Nat such that
A11: s = 2 * k ;
now :: thesis: not k < 2 + 1
assume k < 2 + 1 ; :: thesis: contradiction
then k <= 2 by NAT_1:13;
then 2 * k <= 2 * 2 by XREAL_1:64;
hence contradiction by A1, A11, XXREAL_0:2; :: thesis: verum
end;
per cases then ( k = 3 or k > 3 ) by XXREAL_0:1;
suppose A12: k > 3 ; :: thesis: ex f being s -element natural-valued FinSequence st
( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 )
set f1 = <*H2(3),H2(3)*>;
set f2 = TriangleShift2 (k,2);
set f3 = (k + 1) |-> H2(k);
set f = (<*H2(3),H2(3)*> ^ (TriangleShift2 (k,2))) ^ ((k + 1) |-> H2(k));
A13: len <*H2(3),H2(3)*> = 2 by CARD_1:def 7;
A14: len (TriangleShift2 (k,2)) = (k - 2) - 1 by A12, Lm26, Def15;
A15: len (<*H2(3),H2(3)*> ^ (TriangleShift2 (k,2))) = (len <*H2(3),H2(3)*>) + (len (TriangleShift2 (k,2))) by FINSEQ_1:22;
len ((<*H2(3),H2(3)*> ^ (TriangleShift2 (k,2))) ^ ((k + 1) |-> H2(k))) = (len (<*H2(3),H2(3)*> ^ (TriangleShift2 (k,2)))) + (len ((k + 1) |-> H2(k))) by FINSEQ_1:22
.= s by A11, A13, A14, A15 ;
then reconsider f = (<*H2(3),H2(3)*> ^ (TriangleShift2 (k,2))) ^ ((k + 1) |-> H2(k)) as s -element natural-valued FinSequence by CARD_1:def 7;
take f ; :: thesis: ( f is triangular-valued & f is with_sum_of_reciprocals_equal_1 )
TriangleShift2 (k,2) is triangular-valued by A12, Lm26, Th132;
hence f is triangular-valued ; :: thesis: f is with_sum_of_reciprocals_equal_1
A16: <*H2(3),H2(3)*> " = <*(H2(3) "),(H2(3) ")*> by NUMBER15:64;
A17: Sum <*(H2(3) "),(H2(3) ")*> = (H2(3) ") + (H2(3) ") by RVSUM_2:34;
A18: Sum ((TriangleShift2 (k,2)) ") = (2 / 3) - ((k + 1) / H2(k)) by A12, Th133;
A19: ((k + 1) |-> H2(k)) " = (k + 1) |-> (H2(k) ") by Th43;
A20: (<*H2(3),H2(3)*> ^ (TriangleShift2 (k,2))) " = (<*H2(3),H2(3)*> ") ^ ((TriangleShift2 (k,2)) ") by NUMBER15:60;
thus Sum (f ") = Sum (((<*H2(3),H2(3)*> ^ (TriangleShift2 (k,2))) ") ^ (((k + 1) |-> H2(k)) ")) by NUMBER15:60
.= (Sum ((<*H2(3),H2(3)*> ^ (TriangleShift2 (k,2))) ")) + (Sum (((k + 1) |-> H2(k)) ")) by RVSUM_2:32
.= ((Sum (<*H2(3),H2(3)*> ")) + (Sum ((TriangleShift2 (k,2)) "))) + (Sum (((k + 1) |-> H2(k)) ")) by A20, RVSUM_2:32
.= ((((H2(3) ") + (H2(3) ")) + (2 / 3)) - ((k + 1) / H2(k))) + ((k + 1) * (H2(k) ")) by A16, A17, A18, A19, RVSUM_2:36
.= 1 by NUMPOLY1:13 ; :: according to NUMBER17:def 6 :: thesis: verum
end;
end;
end;
end;
end;
end;