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 ;
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 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 ) )
per cases ( k <= n or k > 3 * n ) by A3;
suppose A4: k <= n ; :: thesis: ( ( not 2 * n < k or not k <= 3 * n ) & ( not n < k or not k <= 2 * n ) )
hence ( not 2 * n < k or not k <= 3 * n ) by A2, NAT_1:12; :: thesis: ( not n < k or not k <= 2 * n )
thus ( not n < k or not k <= 2 * n ) by A4; :: thesis: verum
end;
suppose A5: k > 3 * n ; :: thesis: ( ( not 2 * n < k or not k <= 3 * n ) & ( not n < k or not k <= 2 * n ) )
hence ( not 2 * n < k or not k <= 3 * n ) ; :: thesis: ( not n < k or not k <= 2 * n )
thus ( not n < k or not k <= 2 * n ) by A1, A5, XXREAL_0:2; :: thesis: verum
end;
end;
end;
assume that
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