let A, B be Interval; :: thesis: ( A is open_interval & B is open_interval & A \/ B is Interval implies diameter (A \/ B) <= (diameter A) + (diameter B) )
assume that
A1: A is open_interval and
A2: B is open_interval and
A3: A \/ B is Interval ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
per cases ( A = {} or B = {} or ( A <> {} & B <> {} ) ) ;
suppose ( A = {} or B = {} ) ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
hence diameter (A \/ B) <= (diameter A) + (diameter B) by XXREAL_3:4, MEASURE5:10; :: thesis: verum
end;
suppose A4: ( A <> {} & B <> {} ) ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
then A5: diameter (A \/ B) = (sup (A \/ B)) - (inf (A \/ B)) by MEASURE5:def 6;
ex a1, a2 being R_eal st A = ].a1,a2.[ by A1, MEASURE5:def 2;
then A6: A = ].(inf A),(sup A).[ by A4, XXREAL_2:78;
ex b1, b2 being R_eal st B = ].b1,b2.[ by A2, MEASURE5:def 2;
then A7: B = ].(inf B),(sup B).[ by A4, XXREAL_2:78;
A8: ( diameter A = (sup A) - (inf A) & diameter B = (sup B) - (inf B) ) by A4, MEASURE5:def 6;
A9: ( inf (A \/ B) = min ((inf A),(inf B)) & sup (A \/ B) = max ((sup A),(sup B)) ) by XXREAL_2:9, XXREAL_2:10;
A10: ( sup A <> -infty & sup B <> -infty & inf A <> +infty & inf B <> +infty ) by A4, A6, A7, XXREAL_1:28, XXREAL_0:3, XXREAL_0:5;
A11: ( diameter A >= 0 & diameter B >= 0 & diameter (A \/ B) >= 0 ) by A3, MEASURE5:13;
A12: ( sup A > inf B & sup B > inf A ) by A1, A2, A3, A4, A6, A7, Th1, XXREAL_1:275;
per cases ( inf A < sup B or inf B < sup A ) by A1, A2, A3, A4, Th1;
suppose A13: inf A < sup B ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
per cases ( inf A <= inf B or inf A > inf B ) ;
suppose A14: inf A <= inf B ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
then A15: diameter (A \/ B) = (sup (A \/ B)) - (inf A) by A5, A9, XXREAL_0:def 9;
per cases ( sup A >= sup B or sup A < sup B ) ;
suppose A16: sup A < sup B ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
then A17: diameter (A \/ B) = (sup B) - (inf A) by A9, A15, XXREAL_0:def 10;
per cases ( sup B = +infty or inf A = -infty or ( sup B <> +infty & inf A <> -infty ) ) ;
suppose A18: ( sup B <> +infty & inf A <> -infty ) ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
then A19: inf B <> -infty by A14, XXREAL_0:6;
A20: sup A <> +infty by A16, XXREAL_0:3;
(sup A) - (inf B) >= 0 by A12, XXREAL_3:40;
then (sup B) - (inf A) <= ((sup B) - (inf A)) + ((sup A) - (inf B)) by XXREAL_3:39;
then (sup B) - (inf A) <= (((sup B) - (inf A)) + (sup A)) - (inf B) by A10, A19, A20, XXREAL_3:30;
then (sup B) - (inf A) <= ((sup B) - ((inf A) - (sup A))) - (inf B) by A18, A20, XXREAL_3:32;
then (sup B) - (inf A) <= ((sup B) + (- ((inf A) - (sup A)))) - (inf B) by XXREAL_3:def 4;
then (sup B) - (inf A) <= ((sup B) + (diameter A)) - (inf B) by A8, XXREAL_3:26;
then (sup B) - (inf A) <= (sup B) + ((diameter A) - (inf B)) by A10, A11, XXREAL_3:30;
then (sup B) - (inf A) <= (sup B) + (- ((inf B) - (diameter A))) by XXREAL_3:26;
then (sup B) - (inf A) <= (sup B) - ((inf B) - (diameter A)) by XXREAL_3:def 4;
hence diameter (A \/ B) <= (diameter A) + (diameter B) by A8, A10, A11, A17, XXREAL_3:32; :: thesis: verum
end;
end;
end;
end;
end;
suppose A21: inf A > inf B ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
then A22: diameter (A \/ B) = (sup (A \/ B)) - (inf B) by A5, A9, XXREAL_0:def 9;
per cases ( sup A > sup B or sup A <= sup B ) ;
suppose A23: sup A > sup B ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
then A24: sup B <> +infty by XXREAL_0:3;
A25: sup (A \/ B) = sup A by A9, A23, XXREAL_0:def 10;
per cases ( sup A = +infty or inf B = -infty or ( sup A <> +infty & inf B <> -infty ) ) ;
suppose A26: ( sup A <> +infty & inf B <> -infty ) ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
A27: inf A <> -infty by A21, XXREAL_0:5;
(sup B) - (inf A) >= 0 by A13, XXREAL_3:40;
then (sup A) - (inf B) <= ((sup A) - (inf B)) + ((sup B) - (inf A)) by XXREAL_3:39;
then (sup A) - (inf B) <= (((sup A) - (inf B)) + (sup B)) - (inf A) by A10, A24, A27, XXREAL_3:30;
then (sup A) - (inf B) <= ((sup A) - ((inf B) - (sup B))) - (inf A) by A24, A26, XXREAL_3:32;
then (sup A) - (inf B) <= ((sup A) + (- ((inf B) - (sup B)))) - (inf A) by XXREAL_3:def 4;
then (sup A) - (inf B) <= ((sup A) + (diameter B)) - (inf A) by A8, XXREAL_3:26;
then (sup A) - (inf B) <= (sup A) + ((diameter B) - (inf A)) by A10, A11, XXREAL_3:30;
then (sup A) - (inf B) <= (sup A) + (- ((inf A) - (diameter B))) by XXREAL_3:26;
then (sup A) - (inf B) <= (sup A) - ((inf A) - (diameter B)) by XXREAL_3:def 4;
hence diameter (A \/ B) <= (diameter A) + (diameter B) by A8, A10, A11, A22, A25, XXREAL_3:32; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
suppose A28: inf B < sup A ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
per cases ( inf B <= inf A or inf B > inf A ) ;
suppose A29: inf B <= inf A ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
then A30: diameter (A \/ B) = (sup (A \/ B)) - (inf B) by A5, A9, XXREAL_0:def 9;
per cases ( sup B >= sup A or sup B < sup A ) ;
suppose A31: sup B < sup A ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
then A32: diameter (A \/ B) = (sup A) - (inf B) by A9, A30, XXREAL_0:def 10;
per cases ( sup A = +infty or inf B = -infty or ( sup A <> +infty & inf B <> -infty ) ) ;
suppose A33: ( sup A <> +infty & inf B <> -infty ) ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
then A34: inf A <> -infty by A29, XXREAL_0:6;
A35: sup B <> +infty by A31, XXREAL_0:3;
(sup B) - (inf A) >= 0 by A12, XXREAL_3:40;
then (sup A) - (inf B) <= ((sup A) - (inf B)) + ((sup B) - (inf A)) by XXREAL_3:39;
then (sup A) - (inf B) <= (((sup A) - (inf B)) + (sup B)) - (inf A) by A10, A34, A35, XXREAL_3:30;
then (sup A) - (inf B) <= ((sup A) - ((inf B) - (sup B))) - (inf A) by A33, A35, XXREAL_3:32;
then (sup A) - (inf B) <= ((sup A) + (- ((inf B) - (sup B)))) - (inf A) by XXREAL_3:def 4;
then (sup A) - (inf B) <= ((sup A) + (diameter B)) - (inf A) by A8, XXREAL_3:26;
then (sup A) - (inf B) <= (sup A) + ((diameter B) - (inf A)) by A10, A11, XXREAL_3:30;
then (sup A) - (inf B) <= (sup A) + (- ((inf A) - (diameter B))) by XXREAL_3:26;
then (sup A) - (inf B) <= (sup A) - ((inf A) - (diameter B)) by XXREAL_3:def 4;
hence diameter (A \/ B) <= (diameter A) + (diameter B) by A8, A10, A11, A32, XXREAL_3:32; :: thesis: verum
end;
end;
end;
end;
end;
suppose A36: inf B > inf A ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
then A37: diameter (A \/ B) = (sup (A \/ B)) - (inf A) by A5, A9, XXREAL_0:def 9;
per cases ( sup B > sup A or sup B <= sup A ) ;
suppose A38: sup B > sup A ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
then A39: sup A <> +infty by XXREAL_0:3;
A40: sup (A \/ B) = sup B by A9, A38, XXREAL_0:def 10;
per cases ( sup B = +infty or inf A = -infty or ( sup B <> +infty & inf A <> -infty ) ) ;
suppose A41: ( sup B <> +infty & inf A <> -infty ) ; :: thesis: diameter (A \/ B) <= (diameter A) + (diameter B)
A42: inf B <> -infty by A36, XXREAL_0:5;
(sup A) - (inf B) >= 0 by A28, XXREAL_3:40;
then (sup B) - (inf A) <= ((sup B) - (inf A)) + ((sup A) - (inf B)) by XXREAL_3:39;
then (sup B) - (inf A) <= (((sup B) - (inf A)) + (sup A)) - (inf B) by A10, A39, A42, XXREAL_3:30;
then (sup B) - (inf A) <= ((sup B) - ((inf A) - (sup A))) - (inf B) by A39, A41, XXREAL_3:32;
then (sup B) - (inf A) <= ((sup B) + (- ((inf A) - (sup A)))) - (inf B) by XXREAL_3:def 4;
then (sup B) - (inf A) <= ((sup B) + (diameter A)) - (inf B) by A8, XXREAL_3:26;
then (sup B) - (inf A) <= (sup B) + ((diameter A) - (inf B)) by A10, A11, XXREAL_3:30;
then (sup B) - (inf A) <= (sup B) + (- ((inf B) - (diameter A))) by XXREAL_3:26;
then (sup B) - (inf A) <= (sup B) - ((inf B) - (diameter A)) by XXREAL_3:def 4;
hence diameter (A \/ B) <= (diameter A) + (diameter B) by A8, A10, A11, A37, A40, XXREAL_3:32; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
end;