consider l being Nat such that
A1: ( i2 = l or i2 = - l ) by Th2;
consider k being Nat such that
A2: ( i1 = k or i1 = - k ) by Th2;
A3: now :: thesis: ( i1 = - k & i2 = l implies i1 + i2 is Integer )
A4: now :: thesis: ( l - k <= 0 implies l - k is Integer )
assume l - k <= 0 ; :: thesis: l - k is Integer
then l <= 0 + k by XREAL_1:20;
then consider z being Nat such that
A5: k = l + z by NAT_1:10;
- z = (- k) + l by A5;
hence l - k is Integer by Th1; :: thesis: verum
end;
assume that
A6: i1 = - k and
A7: i2 = l ; :: thesis: i1 + i2 is Integer
now :: thesis: ( 0 <= l - k implies l - k is Integer )
assume 0 <= l - k ; :: thesis: l - k is Integer
then 0 + k <= l by XREAL_1:19;
then ex z being Nat st l = k + z by NAT_1:10;
hence l - k is Integer ; :: thesis: verum
end;
hence i1 + i2 is Integer by A6, A7, A4; :: thesis: verum
end;
A8: now :: thesis: ( i1 = k & i2 = - l implies i1 + i2 is Integer )
A9: now :: thesis: ( k - l <= 0 implies k - l is Integer )
assume k - l <= 0 ; :: thesis: k - l is Integer
then k <= 0 + l by XREAL_1:20;
then consider z being Nat such that
A10: l = k + z by NAT_1:10;
- z = (- l) + k by A10;
hence k - l is Integer by Th1; :: thesis: verum
end;
assume that
A11: i1 = k and
A12: i2 = - l ; :: thesis: i1 + i2 is Integer
now :: thesis: ( 0 <= k - l implies k - l is Integer )
assume 0 <= k - l ; :: thesis: k - l is Integer
then 0 + l <= k by XREAL_1:19;
then ex z being Nat st k = l + z by NAT_1:10;
hence k - l is Integer ; :: thesis: verum
end;
hence i1 + i2 is Integer by A11, A12, A9; :: thesis: verum
end;
now :: thesis: ( i1 = - k & i2 = - l implies i1 + i2 is Integer )
assume that
A13: i1 = - k and
A14: i2 = - l ; :: thesis: i1 + i2 is Integer
i1 + i2 = - (k + l) by A13, A14;
hence i1 + i2 is Integer by Th1; :: thesis: verum
end;
hence i1 + i2 is integer by A2, A1, A8, A3; :: thesis: verum