let i, j be Nat; :: thesis: ( i <= j & j <= i + 55 & not j = i & not j = i + 1 & not j = i + 2 & not j = i + 3 & not j = i + 4 & not j = i + 5 & not j = i + 6 & not j = i + 7 & not j = i + 8 & not j = i + 9 & not j = i + 10 & not j = i + 11 & not j = i + 12 & not j = i + 13 & not j = i + 14 & not j = i + 15 & not j = i + 16 & not j = i + 17 & not j = i + 18 & not j = i + 19 & not j = i + 20 & not j = i + 21 & not j = i + 22 & not j = i + 23 & not j = i + 24 & not j = i + 25 & not j = i + 26 & not j = i + 27 & not j = i + 28 & not j = i + 29 & not j = i + 30 & not j = i + 31 & not j = i + 32 & not j = i + 33 & not j = i + 34 & not j = i + 35 & not j = i + 36 & not j = i + 37 & not j = i + 38 & not j = i + 39 & not j = i + 40 & not j = i + 41 & not j = i + 42 & not j = i + 43 & not j = i + 44 & not j = i + 45 & not j = i + 46 & not j = i + 47 & not j = i + 48 & not j = i + 49 & not j = i + 50 & not j = i + 51 & not j = i + 52 & not j = i + 53 & not j = i + 54 implies j = i + 55 )
assume A0: ( i <= j & j <= i + 55 ) ; :: thesis: ( j = i or j = i + 1 or j = i + 2 or j = i + 3 or j = i + 4 or j = i + 5 or j = i + 6 or j = i + 7 or j = i + 8 or j = i + 9 or j = i + 10 or j = i + 11 or j = i + 12 or j = i + 13 or j = i + 14 or j = i + 15 or j = i + 16 or j = i + 17 or j = i + 18 or j = i + 19 or j = i + 20 or j = i + 21 or j = i + 22 or j = i + 23 or j = i + 24 or j = i + 25 or j = i + 26 or j = i + 27 or j = i + 28 or j = i + 29 or j = i + 30 or j = i + 31 or j = i + 32 or j = i + 33 or j = i + 34 or j = i + 35 or j = i + 36 or j = i + 37 or j = i + 38 or j = i + 39 or j = i + 40 or j = i + 41 or j = i + 42 or j = i + 43 or j = i + 44 or j = i + 45 or j = i + 46 or j = i + 47 or j = i + 48 or j = i + 49 or j = i + 50 or j = i + 51 or j = i + 52 or j = i + 53 or j = i + 54 or j = i + 55 )

now :: thesis: ( ( j <= i + 31 & ( j = i or j = i + 1 or j = i + 2 or j = i + 3 or j = i + 4 or j = i + 5 or j = i + 6 or j = i + 7 or j = i + 8 or j = i + 9 or j = i + 10 or j = i + 11 or j = i + 12 or j = i + 13 or j = i + 14 or j = i + 15 or j = i + 16 or j = i + 17 or j = i + 18 or j = i + 19 or j = i + 20 or j = i + 21 or j = i + 22 or j = i + 23 or j = i + 24 or j = i + 25 or j = i + 26 or j = i + 27 or j = i + 28 or j = i + 29 or j = i + 30 or j = i + 31 ) ) or ( j > i + 31 & ( j = i + 32 or j = i + 33 or j = i + 34 or j = i + 35 or j = i + 36 or j = i + 37 or j = i + 38 or j = i + 39 or j = i + 40 or j = i + 41 or j = i + 42 or j = i + 43 or j = i + 44 or j = i + 45 or j = i + 46 or j = i + 47 or j = i + 48 or j = i + 49 or j = i + 50 or j = i + 51 or j = i + 52 or j = i + 53 or j = i + 54 or j = i + 55 ) ) )

per cases ( j <= i + 31 or j > i + 31 ) ;

case j <= i + 31 ; :: thesis: ( j = i or j = i + 1 or j = i + 2 or j = i + 3 or j = i + 4 or j = i + 5 or j = i + 6 or j = i + 7 or j = i + 8 or j = i + 9 or j = i + 10 or j = i + 11 or j = i + 12 or j = i + 13 or j = i + 14 or j = i + 15 or j = i + 16 or j = i + 17 or j = i + 18 or j = i + 19 or j = i + 20 or j = i + 21 or j = i + 22 or j = i + 23 or j = i + 24 or j = i + 25 or j = i + 26 or j = i + 27 or j = i + 28 or j = i + 29 or j = i + 30 or j = i + 31 )

hence ( j = i or j = i + 1 or j = i + 2 or j = i + 3 or j = i + 4 or j = i + 5 or j = i + 6 or j = i + 7 or j = i + 8 or j = i + 9 or j = i + 10 or j = i + 11 or j = i + 12 or j = i + 13 or j = i + 14 or j = i + 15 or j = i + 16 or j = i + 17 or j = i + 18 or j = i + 19 or j = i + 20 or j = i + 21 or j = i + 22 or j = i + 23 or j = i + 24 or j = i + 25 or j = i + 26 or j = i + 27 or j = i + 28 or j = i + 29 or j = i + 30 or j = i + 31 ) by Lmseg32, A0; :: thesis: verum

end;

case A2: j > i + 31 ; :: thesis: ( j = i + 32 or j = i + 33 or j = i + 34 or j = i + 35 or j = i + 36 or j = i + 37 or j = i + 38 or j = i + 39 or j = i + 40 or j = i + 41 or j = i + 42 or j = i + 43 or j = i + 44 or j = i + 45 or j = i + 46 or j = i + 47 or j = i + 48 or j = i + 49 or j = i + 50 or j = i + 51 or j = i + 52 or j = i + 53 or j = i + 54 or j = i + 55 )

(i + 31) + 1 <= j by A2, NAT_1:13;
then ( j = i + 32 or j = (i + 32) + 1 or j = (i + 32) + 2 or j = (i + 32) + 3 or j = (i + 32) + 4 or j = (i + 32) + 5 or j = (i + 32) + 6 or j = (i + 32) + 7 or j = (i + 32) + 8 or j = (i + 32) + 9 or j = (i + 32) + 10 or j = (i + 32) + 11 or j = (i + 32) + 12 or j = (i + 32) + 13 or j = (i + 32) + 14 or j = (i + 32) + 15 or j = (i + 32) + 16 or j = (i + 32) + 17 or j = (i + 32) + 18 or j = (i + 32) + 19 or j = (i + 32) + 20 or j = (i + 32) + 21 or j = (i + 32) + 22 or j = (i + 32) + 23 ) by Lmseg24, A0;
hence ( j = i + 32 or j = i + 33 or j = i + 34 or j = i + 35 or j = i + 36 or j = i + 37 or j = i + 38 or j = i + 39 or j = i + 40 or j = i + 41 or j = i + 42 or j = i + 43 or j = i + 44 or j = i + 45 or j = i + 46 or j = i + 47 or j = i + 48 or j = i + 49 or j = i + 50 or j = i + 51 or j = i + 52 or j = i + 53 or j = i + 54 or j = i + 55 ) ; :: thesis: verum

end;

end;

end;

hence ( j = i or j = i + 1 or j = i + 2 or j = i + 3 or j = i + 4 or j = i + 5 or j = i + 6 or j = i + 7 or j = i + 8 or j = i + 9 or j = i + 10 or j = i + 11 or j = i + 12 or j = i + 13 or j = i + 14 or j = i + 15 or j = i + 16 or j = i + 17 or j = i + 18 or j = i + 19 or j = i + 20 or j = i + 21 or j = i + 22 or j = i + 23 or j = i + 24 or j = i + 25 or j = i + 26 or j = i + 27 or j = i + 28 or j = i + 29 or j = i + 30 or j = i + 31 or j = i + 32 or j = i + 33 or j = i + 34 or j = i + 35 or j = i + 36 or j = i + 37 or j = i + 38 or j = i + 39 or j = i + 40 or j = i + 41 or j = i + 42 or j = i + 43 or j = i + 44 or j = i + 45 or j = i + 46 or j = i + 47 or j = i + 48 or j = i + 49 or j = i + 50 or j = i + 51 or j = i + 52 or j = i + 53 or j = i + 54 or j = i + 55 ) ; :: thesis: verum