This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0mnnnnn0

Description: The result of subtracting a positive integer from 0 is not a nonnegative integer. (Contributed by Alexander van der Vekens, 19-Mar-2018)

Ref Expression
Assertion 0mnnnnn0 
|- ( N e. NN -> ( 0 - N ) e/ NN0 )

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 nnel 
 |-  ( -. ( 0 - N ) e/ NN0 <-> ( 0 - N ) e. NN0 )
3 df-neg 
 |-  -u N = ( 0 - N )
4 3 eqcomi 
 |-  ( 0 - N ) = -u N
5 4 eleq1i 
 |-  ( ( 0 - N ) e. NN0 <-> -u N e. NN0 )
6 nn0ge0 
 |-  ( -u N e. NN0 -> 0 <_ -u N )
7 nnre 
 |-  ( N e. NN -> N e. RR )
8 7 le0neg1d 
 |-  ( N e. NN -> ( N <_ 0 <-> 0 <_ -u N ) )
9 nngt0 
 |-  ( N e. NN -> 0 < N )
10 0red 
 |-  ( N e. NN -> 0 e. RR )
11 10 7 ltnled 
 |-  ( N e. NN -> ( 0 < N <-> -. N <_ 0 ) )
12 pm2.21 
 |-  ( -. N <_ 0 -> ( N <_ 0 -> -. 0 e. RR ) )
13 11 12 biimtrdi 
 |-  ( N e. NN -> ( 0 < N -> ( N <_ 0 -> -. 0 e. RR ) ) )
14 9 13 mpd 
 |-  ( N e. NN -> ( N <_ 0 -> -. 0 e. RR ) )
15 8 14 sylbird 
 |-  ( N e. NN -> ( 0 <_ -u N -> -. 0 e. RR ) )
16 6 15 syl5 
 |-  ( N e. NN -> ( -u N e. NN0 -> -. 0 e. RR ) )
17 5 16 biimtrid 
 |-  ( N e. NN -> ( ( 0 - N ) e. NN0 -> -. 0 e. RR ) )
18 2 17 biimtrid 
 |-  ( N e. NN -> ( -. ( 0 - N ) e/ NN0 -> -. 0 e. RR ) )
19 1 18 mt4i 
 |-  ( N e. NN -> ( 0 - N ) e/ NN0 )