let A, B be Element of Family_of_Intervals ; :: thesis: ( A misses B & A \/ B is Interval implies pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) )
assume that
A1: A misses B and
A2: A \/ B is Interval ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
A in { I where I is Interval : verum } by MEASUR10:def 1;
then A3: ex I being Interval st A = I ;
B in { I where I is Interval : verum } by MEASUR10:def 1;
then A4: ex I being Interval st B = I ;
per cases ( A = {} or B = {} or ( A <> {} & B <> {} ) ) ;
suppose A5: A = {} ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then pre-Meas . A = 0 by Th58, MEASURE5:10;
hence pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) by A5, XXREAL_3:4; :: thesis: verum
end;
suppose A6: B = {} ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then pre-Meas . B = 0 by Th58, MEASURE5:10;
hence pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) by A6, XXREAL_3:4; :: thesis: verum
end;
suppose A7: ( A <> {} & B <> {} ) ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
per cases ( A is closed_interval or A is right_open_interval or A is left_open_interval or A is open_interval ) by A3, MEASURE5:1;
suppose A is closed_interval ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then A8: A = [.(inf A),(sup A).] by A7, MEASURE6:17;
inf A <= sup A by A7, A8, XXREAL_1:29;
then A9: ( A is left_end & A is right_end ) by A8, XXREAL_2:33;
per cases ( B is right_open_interval or B is left_open_interval or B is open_interval ) by A4, A10, MEASURE5:1;
suppose B is open_interval ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then A17: B = ].(inf B),(sup B).[ by A7, MEASURE6:16;
per cases ( ( inf A = sup B & A \/ B = ].(inf B),(sup A).] ) or ( inf B = sup A & A \/ B = [.(inf A),(sup B).[ ) ) by A1, A2, A7, A8, A17, Th17;
suppose A18: ( inf A = sup B & A \/ B = ].(inf B),(sup A).] ) ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then inf B <= sup A by A7, XXREAL_1:26;
then A19: ( sup (A \/ B) = sup A & inf (A \/ B) = inf B ) by A18, A7, MEASURE6:9, MEASURE6:13;
pre-Meas . (A \/ B) = diameter (A \/ B) by A2, Th59;
then A20: pre-Meas . (A \/ B) = (sup A) - (inf B) by A7, A19, MEASURE5:def 6;
( pre-Meas . A = diameter A & pre-Meas . B = diameter B ) by Th58;
then ( pre-Meas . A = (sup A) - (inf A) & pre-Meas . B = (sup B) - (inf B) ) by A7, MEASURE5:def 6;
hence pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) by A20, A9, A18, XXREAL_3:34; :: thesis: verum
end;
suppose A21: ( inf B = sup A & A \/ B = [.(inf A),(sup B).[ ) ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then inf A <= sup B by A7, XXREAL_1:27;
then A22: ( sup (A \/ B) = sup B & inf (A \/ B) = inf A ) by A21, A7, MEASURE6:11, MEASURE6:15;
pre-Meas . (A \/ B) = diameter (A \/ B) by A2, Th59;
then A23: pre-Meas . (A \/ B) = (sup B) - (inf A) by A7, A22, MEASURE5:def 6;
( pre-Meas . A = diameter A & pre-Meas . B = diameter B ) by Th58;
then ( pre-Meas . A = (sup A) - (inf A) & pre-Meas . B = (sup B) - (inf B) ) by A7, MEASURE5:def 6;
hence pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) by A23, A9, A21, XXREAL_3:34; :: thesis: verum
end;
end;
end;
end;
end;
suppose A is right_open_interval ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then A24: A = [.(inf A),(sup A).[ by A7, MEASURE6:18;
A25: A is left_end by A7, A24, XXREAL_1:27, XXREAL_2:34;
per cases ( B is closed_interval or B is right_open_interval or B is open_interval ) by A4, A26, MEASURE5:1;
suppose B is closed_interval ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then A27: B = [.(inf B),(sup B).] by A7, MEASURE6:17;
then A28: ( inf B = sup A & A \/ B = [.(inf A),(sup B).] ) by A1, A2, A7, A24, Th15;
inf B <= sup B by A7, A27, XXREAL_1:29;
then A29: ( B is left_end & B is right_end ) by A27, XXREAL_2:33;
A30: ( sup (A \/ B) = sup B & inf (A \/ B) = inf A ) by A28, A7, XXREAL_1:29, MEASURE6:10, MEASURE6:14;
pre-Meas . (A \/ B) = diameter (A \/ B) by A2, Th59;
then A31: pre-Meas . (A \/ B) = (sup B) - (inf A) by A7, A30, MEASURE5:def 6;
( pre-Meas . A = diameter A & pre-Meas . B = diameter B ) by Th58;
then ( pre-Meas . A = (sup A) - (inf A) & pre-Meas . B = (sup B) - (inf B) ) by A7, MEASURE5:def 6;
hence pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) by A31, A29, A28, XXREAL_3:34; :: thesis: verum
end;
suppose B is right_open_interval ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then A32: B = [.(inf B),(sup B).[ by A7, MEASURE6:18;
per cases ( ( inf A = sup B & A \/ B = [.(inf B),(sup A).[ ) or ( inf B = sup A & A \/ B = [.(inf A),(sup B).[ ) ) by A1, A2, A7, A24, A32, Th18;
suppose A33: ( inf A = sup B & A \/ B = [.(inf B),(sup A).[ ) ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then inf B <= sup A by A7, XXREAL_1:27;
then A34: ( sup (A \/ B) = sup A & inf (A \/ B) = inf B ) by A33, A7, MEASURE6:11, MEASURE6:15;
pre-Meas . (A \/ B) = diameter (A \/ B) by A2, Th59;
then A35: pre-Meas . (A \/ B) = (sup A) - (inf B) by A7, A34, MEASURE5:def 6;
( pre-Meas . A = diameter A & pre-Meas . B = diameter B ) by Th58;
then ( pre-Meas . A = (sup A) - (inf A) & pre-Meas . B = (sup B) - (inf B) ) by A7, MEASURE5:def 6;
hence pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) by A35, A25, A33, XXREAL_3:34; :: thesis: verum
end;
end;
end;
end;
end;
suppose A is left_open_interval ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then A43: A = ].(inf A),(sup A).] by A7, MEASURE6:19;
A44: A is right_end by A7, A43, XXREAL_1:26, XXREAL_2:35;
per cases ( B is closed_interval or B is left_open_interval or B is open_interval ) by A4, A45, MEASURE5:1;
suppose B is closed_interval ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then A46: B = [.(inf B),(sup B).] by A7, MEASURE6:17;
inf B <= sup B by A7, A46, XXREAL_1:29;
then A47: ( B is left_end & B is right_end ) by A46, XXREAL_2:33;
A48: ( inf A = sup B & A \/ B = [.(inf B),(sup A).] ) by A1, A2, A7, A43, A46, Th16;
then A49: ( sup (A \/ B) = sup A & inf (A \/ B) = inf B ) by A7, XXREAL_1:29, MEASURE6:10, MEASURE6:14;
pre-Meas . (A \/ B) = diameter (A \/ B) by A2, Th59;
then A50: pre-Meas . (A \/ B) = (sup A) - (inf B) by A7, A49, MEASURE5:def 6;
( pre-Meas . A = diameter A & pre-Meas . B = diameter B ) by Th58;
then ( pre-Meas . A = (sup A) - (inf A) & pre-Meas . B = (sup B) - (inf B) ) by A7, MEASURE5:def 6;
hence pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) by A50, A47, A48, XXREAL_3:34; :: thesis: verum
end;
suppose B is left_open_interval ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then A51: B = ].(inf B),(sup B).] by A7, MEASURE6:19;
A52: B is right_end by A7, A51, XXREAL_1:26, XXREAL_2:35;
per cases ( ( inf A = sup B & A \/ B = ].(inf B),(sup A).] ) or ( inf B = sup A & A \/ B = ].(inf A),(sup B).] ) ) by A1, A2, A7, A43, A51, Th21;
suppose A53: ( inf A = sup B & A \/ B = ].(inf B),(sup A).] ) ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then inf B <= sup A by A7, XXREAL_1:26;
then A54: ( sup (A \/ B) = sup A & inf (A \/ B) = inf B ) by A53, A7, MEASURE6:9, MEASURE6:13;
pre-Meas . (A \/ B) = diameter (A \/ B) by A2, Th59;
then A55: pre-Meas . (A \/ B) = (sup A) - (inf B) by A7, A54, MEASURE5:def 6;
( pre-Meas . A = diameter A & pre-Meas . B = diameter B ) by Th58;
then ( pre-Meas . A = (sup A) - (inf A) & pre-Meas . B = (sup B) - (inf B) ) by A7, MEASURE5:def 6;
hence pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) by A55, A52, A53, XXREAL_3:34; :: thesis: verum
end;
suppose A56: ( inf B = sup A & A \/ B = ].(inf A),(sup B).] ) ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then inf A <= sup B by A7, XXREAL_1:26;
then A57: ( sup (A \/ B) = sup B & inf (A \/ B) = inf A ) by A56, A7, MEASURE6:9, MEASURE6:13;
pre-Meas . (A \/ B) = diameter (A \/ B) by A2, Th59;
then A58: pre-Meas . (A \/ B) = (sup B) - (inf A) by A7, A57, MEASURE5:def 6;
( pre-Meas . A = diameter A & pre-Meas . B = diameter B ) by Th58;
then ( pre-Meas . A = (sup A) - (inf A) & pre-Meas . B = (sup B) - (inf B) ) by A7, MEASURE5:def 6;
hence pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) by A58, A44, A56, XXREAL_3:34; :: thesis: verum
end;
end;
end;
end;
end;
suppose A is open_interval ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then A63: A = ].(inf A),(sup A).[ by A7, MEASURE6:16;
per cases ( B is closed_interval or B is left_open_interval or B is right_open_interval ) by A4, A64, MEASURE5:1;
suppose B is closed_interval ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then A65: B = [.(inf B),(sup B).] by A7, MEASURE6:17;
inf B <= sup B by A7, A65, XXREAL_1:29;
then A66: ( B is left_end & B is right_end ) by A65, XXREAL_2:33;
per cases ( ( inf A = sup B & A \/ B = [.(inf B),(sup A).[ ) or ( inf B = sup A & A \/ B = ].(inf A),(sup B).] ) ) by A1, A2, A7, A63, A65, Th17;
suppose A67: ( inf A = sup B & A \/ B = [.(inf B),(sup A).[ ) ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then inf B <= sup A by A7, XXREAL_1:27;
then A68: ( sup (A \/ B) = sup A & inf (A \/ B) = inf B ) by A67, A7, MEASURE6:11, MEASURE6:15;
pre-Meas . (A \/ B) = diameter (A \/ B) by A2, Th59;
then A69: pre-Meas . (A \/ B) = (sup A) - (inf B) by A7, A68, MEASURE5:def 6;
( pre-Meas . A = diameter A & pre-Meas . B = diameter B ) by Th58;
then ( pre-Meas . A = (sup A) - (inf A) & pre-Meas . B = (sup B) - (inf B) ) by A7, MEASURE5:def 6;
hence pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) by A69, A67, A66, XXREAL_3:34; :: thesis: verum
end;
suppose A70: ( inf B = sup A & A \/ B = ].(inf A),(sup B).] ) ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then inf A <= sup B by A7, XXREAL_1:26;
then A71: ( sup (A \/ B) = sup B & inf (A \/ B) = inf A ) by A70, A7, MEASURE6:9, MEASURE6:13;
pre-Meas . (A \/ B) = diameter (A \/ B) by A2, Th59;
then A72: pre-Meas . (A \/ B) = (sup B) - (inf A) by A7, A71, MEASURE5:def 6;
( pre-Meas . A = diameter A & pre-Meas . B = diameter B ) by Th58;
then ( pre-Meas . A = (sup A) - (inf A) & pre-Meas . B = (sup B) - (inf B) ) by A7, MEASURE5:def 6;
hence pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) by A72, A70, A66, XXREAL_3:34; :: thesis: verum
end;
end;
end;
suppose B is left_open_interval ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then A73: B = ].(inf B),(sup B).] by A7, MEASURE6:19;
A74: ( sup B = inf A & A \/ B = ].(inf B),(sup A).[ ) by A1, A2, A7, A63, A73, Th22;
then inf B <= sup A by A7, XXREAL_1:28;
then A75: ( sup (A \/ B) = sup A & inf (A \/ B) = inf B ) by A74, A7, MEASURE6:8, MEASURE6:12;
A76: B is right_end by A7, A73, XXREAL_1:26, XXREAL_2:35;
pre-Meas . (A \/ B) = diameter (A \/ B) by A2, Th59;
then A77: pre-Meas . (A \/ B) = (sup A) - (inf B) by A7, A75, MEASURE5:def 6;
( pre-Meas . A = diameter A & pre-Meas . B = diameter B ) by Th58;
then ( pre-Meas . A = (sup A) - (inf A) & pre-Meas . B = (sup B) - (inf B) ) by A7, MEASURE5:def 6;
hence pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) by A77, A74, A76, XXREAL_3:34; :: thesis: verum
end;
suppose B is right_open_interval ; :: thesis: pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B)
then A78: B = [.(inf B),(sup B).[ by A7, MEASURE6:18;
then A79: ( sup A = inf B & A \/ B = ].(inf A),(sup B).[ ) by A1, A2, A7, A63, Th20;
then inf A <= sup B by A7, XXREAL_1:28;
then A80: ( sup (A \/ B) = sup B & inf (A \/ B) = inf A ) by A79, A7, MEASURE6:8, MEASURE6:12;
A81: B is left_end by A7, A78, XXREAL_1:27, XXREAL_2:34;
pre-Meas . (A \/ B) = diameter (A \/ B) by A2, Th59;
then A82: pre-Meas . (A \/ B) = (sup B) - (inf A) by A7, A80, MEASURE5:def 6;
( pre-Meas . A = diameter A & pre-Meas . B = diameter B ) by Th58;
then ( pre-Meas . A = (sup A) - (inf A) & pre-Meas . B = (sup B) - (inf B) ) by A7, MEASURE5:def 6;
hence pre-Meas . (A \/ B) = (pre-Meas . A) + (pre-Meas . B) by A82, A79, A81, XXREAL_3:34; :: thesis: verum
end;
end;
end;
end;
end;
end;