let k, n be Nat; :: thesis: ( ( n < k & k <= 2 * n implies ( ( not 2 * n < k or not k <= 3 * n ) & not k <= n & not k > 3 * n ) ) & ( ( k <= n or k > 3 * n ) implies ( ( not 2 * n < k or not k <= 3 * n ) & ( not n < k or not k <= 2 * n ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( not n < k or not k <= 2 * n ) & not k <= n & not k > 3 * n ) ) )

A1: 2 * n <= 3 * n by NAT_1:4;

hence ( n < k & k <= 2 * n implies ( ( not 2 * n < k or not k <= 3 * n ) & not k <= n & not k > 3 * n ) ) by XXREAL_0:2; :: thesis: ( ( ( k <= n or k > 3 * n ) implies ( ( not 2 * n < k or not k <= 3 * n ) & ( not n < k or not k <= 2 * n ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( not n < k or not k <= 2 * n ) & not k <= n & not k > 3 * n ) ) )

A2: 2 * n = n + n ;

A6: 2 * n < k and

A7: k <= 3 * n ; :: thesis: ( ( not n < k or not k <= 2 * n ) & not k <= n & not k > 3 * n )

thus ( not n < k or not k <= 2 * n ) by A6; :: thesis: ( not k <= n & not k > 3 * n )

thus ( not k <= n & not k > 3 * n ) by A2, A6, A7, NAT_1:12; :: thesis: verum

A1: 2 * n <= 3 * n by NAT_1:4;

hence ( n < k & k <= 2 * n implies ( ( not 2 * n < k or not k <= 3 * n ) & not k <= n & not k > 3 * n ) ) by XXREAL_0:2; :: thesis: ( ( ( k <= n or k > 3 * n ) implies ( ( not 2 * n < k or not k <= 3 * n ) & ( not n < k or not k <= 2 * n ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( not n < k or not k <= 2 * n ) & not k <= n & not k > 3 * n ) ) )

A2: 2 * n = n + n ;

hereby :: thesis: ( 2 * n < k & k <= 3 * n implies ( ( not n < k or not k <= 2 * n ) & not k <= n & not k > 3 * n ) )

assume that assume A3:
( k <= n or k > 3 * n )
; :: thesis: ( ( not 2 * n < k or not k <= 3 * n ) & ( not n < k or not k <= 2 * n ) )

end;per cases
( k <= n or k > 3 * n )
by A3;

end;

A6: 2 * n < k and

A7: k <= 3 * n ; :: thesis: ( ( not n < k or not k <= 2 * n ) & not k <= n & not k > 3 * n )

thus ( not n < k or not k <= 2 * n ) by A6; :: thesis: ( not k <= n & not k > 3 * n )

thus ( not k <= n & not k > 3 * n ) by A2, A6, A7, NAT_1:12; :: thesis: verum