let s be positive Nat; :: thesis: ( ( s = 1 or s = 4 or s >= 6 ) iff ex f being s -element natural-valued positive FinSequence st f is with_sum_of_squares_of_reciprocals_equal_1 )
defpred S1[ Nat] means ex f being $1 -element natural-valued positive FinSequence st f is with_sum_of_squares_of_reciprocals_equal_1 ;
thus ( not S1[s] or s = 1 or s = 4 or s >= 6 ) :: thesis: ( ( s = 1 or s = 4 or s >= 6 ) implies ex f being s -element natural-valued positive FinSequence st f is with_sum_of_squares_of_reciprocals_equal_1 )
proof
given f being s -element natural-valued positive FinSequence such that A1: f is with_sum_of_squares_of_reciprocals_equal_1 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
A2: f is FinSequence of NAT by FINSEQ_1:103;
per cases ( s = 1 or s = 4 or s >= 6 or s = 2 or s = 3 or s = 5 ) by Lm27;
suppose ( s = 1 or s = 4 or s >= 6 ) ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
hence ( s = 1 or s = 4 or s >= 6 ) ; :: thesis: verum
end;
suppose s = 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then consider a, b being Element of NAT such that
A3: f = <*a,b*> by A2, FINSEQ_2:100;
reconsider a = a, b = b as positive Nat by A3;
<*a,b*> " = <*(a "),(b ")*> by NUMBER15:64;
then (<*a,b*> ") ^2 = <*((a ") ^2),((b ") ^2)*> by Th8;
then A4: Sum ((<*a,b*> ") ^2) = ((a ") ^2) + ((b ") ^2) by RVSUM_2:34;
( a >= 1 & b >= 1 ) by NAT_1:14;
per cases then ( a = 1 or b = 1 or ( a > 1 & b > 1 ) ) by XXREAL_0:1;
suppose ( a = 1 or b = 1 ) ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A3, A4, XREAL_1:6; :: thesis: verum
end;
suppose ( a > 1 & b > 1 ) ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then ( (a ") ^2 <= 1 / 4 & (b ") ^2 <= 1 / 4 ) by Lm29;
then ((a ") ^2) + ((b ") ^2) <= (1 / 4) + (1 / 4) by XREAL_1:7;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A3, A4; :: thesis: verum
end;
end;
end;
suppose s = 3 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then consider a, b, c being Element of NAT such that
A5: f = <*a,b,c*> by A2, FINSEQ_2:103;
reconsider a = a, b = b, c = c as positive Nat by A5;
<*a,b,c*> " = <*(a "),(b "),(c ")*> by NUMBER15:65;
then (<*a,b,c*> ") ^2 = <*((a ") ^2),((b ") ^2),((c ") ^2)*> by Th9;
then A6: Sum ((<*a,b,c*> ") ^2) = (((a ") ^2) + ((b ") ^2)) + ((c ") ^2) by RVSUM_2:35;
( a >= 1 & b >= 1 & c >= 1 ) by NAT_1:14;
per cases then ( a = 1 or b = 1 or c = 1 or ( a > 1 & b > 1 & c > 1 ) ) by XXREAL_0:1;
suppose ( a = 1 or b = 1 or c = 1 ) ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then ( (((a ") ^2) + ((b ") ^2)) + ((c ") ^2) > 1 + 0 or (((a ") ^2) + ((c ") ^2)) + ((b ") ^2) > 1 + 0 or (((b ") ^2) + ((c ") ^2)) + ((a ") ^2) > 1 + 0 ) by XREAL_1:8;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A5, A6; :: thesis: verum
end;
suppose ( a > 1 & b > 1 & c > 1 ) ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then A7: ( (a ") ^2 <= 1 / 4 & (b ") ^2 <= 1 / 4 & (c ") ^2 <= 1 / 4 ) by Lm29;
then ((a ") ^2) + ((b ") ^2) <= ((1 / 2) ^2) + ((1 / 2) ^2) by XREAL_1:7;
then (((a ") ^2) + ((b ") ^2)) + ((c ") ^2) <= (((1 / 2) ^2) + ((1 / 2) ^2)) + ((1 / 2) ^2) by A7, XREAL_1:7;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A5, A6; :: thesis: verum
end;
end;
end;
suppose s = 5 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then consider a, b, c, d, e being Element of NAT such that
A8: f = <*a,b,c,d,e*> by A2, Th6;
reconsider a = a, b = b, c = c, d = d, e = e as positive Nat by A8;
<*a,b,c,d,e*> " = <*(a "),(b "),(c "),(d "),(e ")*> by Th16;
then (<*a,b,c,d,e*> ") ^2 = <*((a ") ^2),((b ") ^2),((c ") ^2),((d ") ^2),((e ") ^2)*> by Th11;
then A9: Sum ((<*a,b,c,d,e*> ") ^2) = (((((a ") ^2) + ((b ") ^2)) + ((c ") ^2)) + ((d ") ^2)) + ((e ") ^2) by Th21;
A10: (((((a ") ^2) + ((b ") ^2)) + ((c ") ^2)) + ((d ") ^2)) + ((e ") ^2) = (((((a ") ^2) + ((b ") ^2)) + ((c ") ^2)) + ((e ") ^2)) + ((d ") ^2) ;
A11: (((((a ") ^2) + ((b ") ^2)) + ((c ") ^2)) + ((d ") ^2)) + ((e ") ^2) = (((((b ") ^2) + ((c ") ^2)) + ((d ") ^2)) + ((e ") ^2)) + ((a ") ^2) ;
A12: (((((a ") ^2) + ((b ") ^2)) + ((c ") ^2)) + ((d ") ^2)) + ((e ") ^2) = (((((a ") ^2) + ((b ") ^2)) + ((d ") ^2)) + ((e ") ^2)) + ((c ") ^2) ;
( a >= 1 & b >= 1 & c >= 1 & d >= 1 & e >= 1 ) by NAT_1:14;
per cases then ( a = 1 or b = 1 or c = 1 or d = 1 or e = 1 or ( a > 1 & b > 1 & c > 1 & d > 1 & e > 1 ) ) by XXREAL_0:1;
suppose a = 1 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then (((((b ") ^2) + ((c ") ^2)) + ((d ") ^2)) + ((e ") ^2)) + ((a ") ^2) > 1 + 0 by XREAL_1:8;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
suppose b = 1 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then (((((a ") ^2) + ((c ") ^2)) + ((d ") ^2)) + ((e ") ^2)) + ((b ") ^2) > 1 + 0 by XREAL_1:8;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
suppose c = 1 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then (((((a ") ^2) + ((b ") ^2)) + ((d ") ^2)) + ((e ") ^2)) + ((c ") ^2) > 1 + 0 by XREAL_1:8;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
suppose d = 1 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then (((((a ") ^2) + ((b ") ^2)) + ((c ") ^2)) + ((e ") ^2)) + ((d ") ^2) > 1 + 0 by XREAL_1:8;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
suppose e = 1 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9, XREAL_1:8; :: thesis: verum
end;
suppose that A13: a > 1 and
A14: b > 1 and
A15: c > 1 and
A16: d > 1 and
A17: e > 1 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
A18: b >= 1 + 1 by A14, NAT_1:13;
A19: c >= 1 + 1 by A15, NAT_1:13;
A20: d >= 1 + 1 by A16, NAT_1:13;
A21: e >= 1 + 1 by A17, NAT_1:13;
A22: (a ") ^2 <= 1 / 4 by A13, Lm29;
A23: (b ") ^2 <= 1 / 4 by A14, Lm29;
A24: (c ") ^2 <= 1 / 4 by A15, Lm29;
A25: (d ") ^2 <= 1 / 4 by A16, Lm29;
A26: (e ") ^2 <= 1 / 4 by A17, Lm29;
a >= 1 + 1 by A13, NAT_1:13;
per cases then ( ( a = 2 & b = 2 & c = 2 & d = 2 & e = 2 ) or a > 2 or ( a = 2 & b > 2 ) or ( a = 2 & b = 2 & c > 2 ) or ( a = 2 & b = 2 & c = 2 & d > 2 & e = 2 ) or ( a = 2 & b = 2 & c = 2 & d > 2 & e > 2 ) or ( a = 2 & b = 2 & c = 2 & d = 2 & e > 2 ) ) by A18, A19, A20, A21, XXREAL_0:1;
suppose ( a = 2 & b = 2 & c = 2 & d = 2 & e = 2 ) ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
suppose a > 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then A27: (a ") ^2 <= 1 / 9 by Lm30;
per cases ( b = 2 or b > 2 ) by A18, XXREAL_0:1;
suppose A28: b = 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
per cases ( c = 2 or c > 2 ) by A19, XXREAL_0:1;
suppose A29: c = 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
per cases ( d = 2 or d > 2 ) by A20, XXREAL_0:1;
suppose A30: d = 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
per cases ( e = 2 or e > 2 ) by A21, XXREAL_0:1;
suppose e = 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9, A11, A28, A29, A30, XREAL_1:6; :: thesis: verum
end;
suppose e > 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then (e ") ^2 <= 1 / 9 by Lm30;
then A31: ((a ") ^2) + ((e ") ^2) <= (1 / 9) + (1 / 9) by A27, XREAL_1:7;
((b ") ^2) + ((c ") ^2) <= (1 / 4) + (1 / 4) by A23, A24, XREAL_1:7;
then (((b ") ^2) + ((c ") ^2)) + ((d ") ^2) <= (2 / 4) + (1 / 4) by A25, XREAL_1:7;
then (((a ") ^2) + ((e ") ^2)) + ((((b ") ^2) + ((c ") ^2)) + ((d ") ^2)) <= (2 / 9) + (3 / 4) by A31, XREAL_1:7;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
end;
end;
suppose d > 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then (d ") ^2 <= 1 / 9 by Lm30;
then A32: ((a ") ^2) + ((d ") ^2) <= (1 / 9) + (1 / 9) by A27, XREAL_1:7;
((b ") ^2) + ((c ") ^2) <= (1 / 4) + (1 / 4) by A23, A24, XREAL_1:7;
then (((b ") ^2) + ((c ") ^2)) + ((e ") ^2) <= (2 / 4) + (1 / 4) by A26, XREAL_1:7;
then (((a ") ^2) + ((d ") ^2)) + ((((b ") ^2) + ((c ") ^2)) + ((e ") ^2)) <= (2 / 9) + (3 / 4) by A32, XREAL_1:7;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
end;
end;
suppose c > 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then (c ") ^2 <= 1 / 9 by Lm30;
then A33: ((a ") ^2) + ((c ") ^2) <= (1 / 9) + (1 / 9) by A27, XREAL_1:7;
((b ") ^2) + ((d ") ^2) <= (1 / 4) + (1 / 4) by A23, A25, XREAL_1:7;
then (((b ") ^2) + ((d ") ^2)) + ((e ") ^2) <= (2 / 4) + (1 / 4) by A26, XREAL_1:7;
then (((a ") ^2) + ((c ") ^2)) + ((((b ") ^2) + ((d ") ^2)) + ((e ") ^2)) <= (2 / 9) + (3 / 4) by A33, XREAL_1:7;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
end;
end;
suppose b > 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then (b ") ^2 <= 1 / 9 by Lm30;
then A34: ((a ") ^2) + ((b ") ^2) <= (1 / 9) + (1 / 9) by A27, XREAL_1:7;
((c ") ^2) + ((d ") ^2) <= (1 / 4) + (1 / 4) by A24, A25, XREAL_1:7;
then (((c ") ^2) + ((d ") ^2)) + ((e ") ^2) <= ((1 / 4) + (1 / 4)) + (1 / 4) by A26, XREAL_1:7;
then (((a ") ^2) + ((b ") ^2)) + ((((c ") ^2) + ((d ") ^2)) + ((e ") ^2)) <= (2 / 9) + (3 / 4) by A34, XREAL_1:7;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
end;
end;
suppose that A35: a = 2 and
A36: b > 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
A37: (b ") ^2 <= 1 / 9 by A36, Lm30;
per cases ( c = 2 or c > 2 ) by A19, XXREAL_0:1;
suppose A38: c = 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
per cases ( d = 2 or d > 2 ) by A20, XXREAL_0:1;
suppose A39: d = 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
per cases ( e = 2 or e > 2 ) by A21, XXREAL_0:1;
suppose e = 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then (((((a ") ^2) + ((c ") ^2)) + ((d ") ^2)) + ((e ") ^2)) + ((b ") ^2) > 1 + 0 by A35, A38, A39, XREAL_1:6;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
suppose e > 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then (e ") ^2 <= 1 / 9 by Lm30;
then A40: ((b ") ^2) + ((e ") ^2) <= (1 / 9) + (1 / 9) by A37, XREAL_1:7;
((a ") ^2) + ((c ") ^2) <= (1 / 4) + (1 / 4) by A22, A24, XREAL_1:7;
then (((a ") ^2) + ((c ") ^2)) + ((d ") ^2) <= (2 / 4) + (1 / 4) by A25, XREAL_1:7;
then (((b ") ^2) + ((e ") ^2)) + ((((a ") ^2) + ((c ") ^2)) + ((d ") ^2)) <= (2 / 9) + (3 / 4) by A40, XREAL_1:7;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
end;
end;
suppose d > 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then (d ") ^2 <= 1 / 9 by Lm30;
then A41: ((b ") ^2) + ((d ") ^2) <= (1 / 9) + (1 / 9) by A37, XREAL_1:7;
((a ") ^2) + ((c ") ^2) <= (1 / 4) + (1 / 4) by A22, A24, XREAL_1:7;
then (((a ") ^2) + ((c ") ^2)) + ((e ") ^2) <= (2 / 4) + (1 / 4) by A26, XREAL_1:7;
then (((b ") ^2) + ((d ") ^2)) + ((((a ") ^2) + ((c ") ^2)) + ((e ") ^2)) <= (2 / 9) + (3 / 4) by A41, XREAL_1:7;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
end;
end;
suppose c > 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then (c ") ^2 <= 1 / 9 by Lm30;
then A42: ((b ") ^2) + ((c ") ^2) <= (1 / 9) + (1 / 9) by A37, XREAL_1:7;
((a ") ^2) + ((d ") ^2) <= (1 / 4) + (1 / 4) by A22, A25, XREAL_1:7;
then (((a ") ^2) + ((d ") ^2)) + ((e ") ^2) <= (2 / 4) + (1 / 4) by A26, XREAL_1:7;
then (((b ") ^2) + ((c ") ^2)) + ((((a ") ^2) + ((d ") ^2)) + ((e ") ^2)) <= (2 / 9) + (3 / 4) by A42, XREAL_1:7;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
end;
end;
suppose that A43: ( a = 2 & b = 2 ) and
A44: c > 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
A45: (c ") ^2 <= 1 / 9 by A44, Lm30;
per cases ( ( d = 2 & e = 2 ) or ( d = 2 & e > 2 ) or d > 2 ) by A20, A21, XXREAL_0:1;
suppose ( d = 2 & e = 2 ) ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9, A12, A43, XREAL_1:6; :: thesis: verum
end;
suppose that A46: d = 2 and
A47: e > 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
(e ") ^2 <= 1 / 9 by A47, Lm30;
then ((c ") ^2) + ((e ") ^2) <= (1 / 9) + (1 / 9) by A45, XREAL_1:7;
then ((((a ") ^2) + ((b ") ^2)) + ((d ") ^2)) + (((c ") ^2) + ((e ") ^2)) <= (3 / 4) + (2 / 9) by A43, A46, XREAL_1:6;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
suppose d > 2 ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
then (d ") ^2 <= 1 / 9 by Lm30;
then ((d ") ^2) + ((e ") ^2) <= (1 / 9) + (1 / 4) by A26, XREAL_1:7;
then ((c ") ^2) + (((d ") ^2) + ((e ") ^2)) <= (1 / 9) + (13 / 36) by A45, XREAL_1:7;
then (((a ") ^2) + ((b ") ^2)) + (((c ") ^2) + (((d ") ^2) + ((e ") ^2))) <= (2 / 4) + (17 / 36) by A43, XREAL_1:6;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
end;
end;
suppose ( a = 2 & b = 2 & c = 2 & d > 2 & e = 2 ) ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9, A10, XREAL_1:6; :: thesis: verum
end;
suppose that A48: ( a = 2 & b = 2 & c = 2 ) and
A49: ( d > 2 & e > 2 ) ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
( (d ") ^2 <= 1 / 9 & (e ") ^2 <= 1 / 9 ) by A49, Lm30;
then ((d ") ^2) + ((e ") ^2) <= (1 / 9) + (1 / 9) by XREAL_1:7;
then ((((a ") ^2) + ((b ") ^2)) + ((c ") ^2)) + (((d ") ^2) + ((e ") ^2)) <= (3 / 4) + (2 / 9) by A48, XREAL_1:6;
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9; :: thesis: verum
end;
suppose ( a = 2 & b = 2 & c = 2 & d = 2 & e > 2 ) ; :: thesis: ( s = 1 or s = 4 or s >= 6 )
hence ( s = 1 or s = 4 or s >= 6 ) by A1, A8, A9, XREAL_1:6; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
assume ( s = 1 or s = 4 or s >= 6 ) ; :: thesis: ex f being s -element natural-valued positive FinSequence st f is with_sum_of_squares_of_reciprocals_equal_1
per cases then ( s = 1 or s = 4 or s >= 6 ) ;
suppose s = 1 ; :: thesis: ex f being s -element natural-valued positive FinSequence st f is with_sum_of_squares_of_reciprocals_equal_1
then reconsider f = <*1*> as s -element natural-valued positive FinSequence ;
take f ; :: thesis: f is with_sum_of_squares_of_reciprocals_equal_1
thus f is with_sum_of_squares_of_reciprocals_equal_1 by Th135; :: thesis: verum
end;
suppose s = 4 ; :: thesis: ex f being s -element natural-valued positive FinSequence st f is with_sum_of_squares_of_reciprocals_equal_1
then reconsider f = <*2,2,2,2*> as s -element natural-valued positive FinSequence ;
take f ; :: thesis: f is with_sum_of_squares_of_reciprocals_equal_1
thus f is with_sum_of_squares_of_reciprocals_equal_1 by Th136; :: thesis: verum
end;
suppose A50: s >= 6 ; :: thesis: ex f being s -element natural-valued positive FinSequence st f is with_sum_of_squares_of_reciprocals_equal_1
defpred S2[ Nat] means ( $1 >= 6 implies S1[$1] );
A51: for k being Nat holds
( S2[3 * k] & S2[(3 * k) + 1] & S2[(3 * k) + 2] )
proof
let k be Nat; :: thesis: ( S2[3 * k] & S2[(3 * k) + 1] & S2[(3 * k) + 2] )
thus S2[3 * k] :: thesis: ( S2[(3 * k) + 1] & S2[(3 * k) + 2] )
proof
assume A52: 3 * k >= 6 ; :: thesis: S1[3 * k]
then 3 * k >= 3 * 2 ;
then A53: k >= 2 by XREAL_1:68;
defpred S3[ Nat] means ( $1 >= 2 implies S2[3 * $1] );
A54: S3[ 0 ] ;
A55: for m being Nat st S3[m] holds
S3[m + 1]
proof
let m be Nat; :: thesis: ( S3[m] implies S3[m + 1] )
assume that
A56: S3[m] and
A57: m + 1 >= 2 ; :: thesis: S2[3 * (m + 1)]
m >= 2 - 1 by A57, XREAL_1:20;
per cases then ( m = 1 or m >= 2 ) by NAT_1:23;
suppose m = 1 ; :: thesis: S2[3 * (m + 1)]
hence S2[3 * (m + 1)] by Th137; :: thesis: verum
end;
suppose A58: m >= 2 ; :: thesis: S2[3 * (m + 1)]
then 3 * m >= 3 * 2 by XREAL_1:64;
then S1[(3 * m) + 3] by A56, A58, Lm28;
hence S2[3 * (m + 1)] ; :: thesis: verum
end;
end;
end;
for m being Nat holds S3[m] from NAT_1:sch 2(A54, A55);
 hence S1[3 * k] by A52, A53; :: thesis: verum
end;
thus S2[(3 * k) + 1] :: thesis: S2[(3 * k) + 2]
proof
assume A59: (3 * k) + 1 >= 6 ; :: thesis: S1[(3 * k) + 1]
A60: now :: thesis: not k < 1 + 1
assume k < 1 + 1 ; :: thesis: contradiction
then k <= 1 by NAT_1:13;
then 3 * k <= 3 * 1 by XREAL_1:64;
then (3 * k) + 1 <= 3 + 1 by XREAL_1:6;
hence contradiction by A59, XXREAL_0:2; :: thesis: verum
end;
defpred S3[ Nat] means ( $1 >= 2 implies S2[(3 * $1) + 1] );
A61: S3[ 0 ] ;
A62: for m being Nat st S3[m] holds
S3[m + 1]
proof
let m be Nat; :: thesis: ( S3[m] implies S3[m + 1] )
assume that
A63: S3[m] and
A64: m + 1 >= 2 ; :: thesis: S2[(3 * (m + 1)) + 1]
m >= 2 - 1 by A64, XREAL_1:20;
per cases then ( m = 1 or m >= 2 ) by NAT_1:23;
suppose m = 1 ; :: thesis: S2[(3 * (m + 1)) + 1]
hence S2[(3 * (m + 1)) + 1] by Th138; :: thesis: verum
end;
suppose A65: m >= 2 ; :: thesis: S2[(3 * (m + 1)) + 1]
then (3 * m) + 1 >= 3 * 2 by XREAL_1:64, XREAL_1:145;
then S1[((3 * m) + 1) + 3] by A63, A65, Lm28;
hence S2[(3 * (m + 1)) + 1] ; :: thesis: verum
end;
end;
end;
for m being Nat holds S3[m] from NAT_1:sch 2(A61, A62);
 hence S1[(3 * k) + 1] by A59, A60; :: thesis: verum
end;
thus S2[(3 * k) + 2] :: thesis: verum
proof
assume A66: (3 * k) + 2 >= 6 ; :: thesis: S1[(3 * k) + 2]
A67: now :: thesis: not k < 1 + 1
assume k < 1 + 1 ; :: thesis: contradiction
then k <= 1 by NAT_1:13;
then 3 * k <= 3 * 1 by XREAL_1:64;
then (3 * k) + 2 <= 3 + 2 by XREAL_1:6;
hence contradiction by A66, XXREAL_0:2; :: thesis: verum
end;
defpred S3[ Nat] means ( $1 >= 2 implies S2[(3 * $1) + 2] );
A68: S3[ 0 ] ;
A69: for m being Nat st S3[m] holds
S3[m + 1]
proof
let m be Nat; :: thesis: ( S3[m] implies S3[m + 1] )
assume that
A70: S3[m] and
A71: m + 1 >= 2 ; :: thesis: S2[(3 * (m + 1)) + 2]
m >= 2 - 1 by A71, XREAL_1:20;
per cases then ( m = 1 or m >= 2 ) by NAT_1:23;
suppose m = 1 ; :: thesis: S2[(3 * (m + 1)) + 2]
hence S2[(3 * (m + 1)) + 2] by Th139; :: thesis: verum
end;
suppose A72: m >= 2 ; :: thesis: S2[(3 * (m + 1)) + 2]
then A73: 3 * m >= 3 * 2 by XREAL_1:64;
(3 * m) + 2 > (3 * m) + 0 by XREAL_1:6;
then (3 * m) + 2 >= 3 * 2 by A73, XXREAL_0:2;
then S1[((3 * m) + 2) + 3] by A70, A72, Lm28;
hence S2[(3 * (m + 1)) + 2] ; :: thesis: verum
end;
end;
end;
for m being Nat holds S3[m] from NAT_1:sch 2(A68, A69);
 hence S1[(3 * k) + 2] by A66, A67; :: thesis: verum
end;
end;
for k being Nat holds S2[k] from NUMBER17:sch 3(A51);
hence ex f being s -element natural-valued positive FinSequence st f is with_sum_of_squares_of_reciprocals_equal_1 by A50; :: thesis: verum
end;
end;