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

Metamath Proof Explorer

Theorem nnsub

Description: Subtraction of positive integers. (Contributed by NM, 20-Aug-2001) (Revised by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion nnsub 
|- ( ( A e. NN /\ B e. NN ) -> ( A < B <-> ( B - A ) e. NN ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( x = 1 -> ( z < x <-> z < 1 ) )
2 oveq1 
 |-  ( x = 1 -> ( x - z ) = ( 1 - z ) )
3 2 eleq1d 
 |-  ( x = 1 -> ( ( x - z ) e. NN <-> ( 1 - z ) e. NN ) )
4 1 3 imbi12d 
 |-  ( x = 1 -> ( ( z < x -> ( x - z ) e. NN ) <-> ( z < 1 -> ( 1 - z ) e. NN ) ) )
5 4 ralbidv 
 |-  ( x = 1 -> ( A. z e. NN ( z < x -> ( x - z ) e. NN ) <-> A. z e. NN ( z < 1 -> ( 1 - z ) e. NN ) ) )
6 breq2 
 |-  ( x = y -> ( z < x <-> z < y ) )
7 oveq1 
 |-  ( x = y -> ( x - z ) = ( y - z ) )
8 7 eleq1d 
 |-  ( x = y -> ( ( x - z ) e. NN <-> ( y - z ) e. NN ) )
9 6 8 imbi12d 
 |-  ( x = y -> ( ( z < x -> ( x - z ) e. NN ) <-> ( z < y -> ( y - z ) e. NN ) ) )
10 9 ralbidv 
 |-  ( x = y -> ( A. z e. NN ( z < x -> ( x - z ) e. NN ) <-> A. z e. NN ( z < y -> ( y - z ) e. NN ) ) )
11 breq2 
 |-  ( x = ( y + 1 ) -> ( z < x <-> z < ( y + 1 ) ) )
12 oveq1 
 |-  ( x = ( y + 1 ) -> ( x - z ) = ( ( y + 1 ) - z ) )
13 12 eleq1d 
 |-  ( x = ( y + 1 ) -> ( ( x - z ) e. NN <-> ( ( y + 1 ) - z ) e. NN ) )
14 11 13 imbi12d 
 |-  ( x = ( y + 1 ) -> ( ( z < x -> ( x - z ) e. NN ) <-> ( z < ( y + 1 ) -> ( ( y + 1 ) - z ) e. NN ) ) )
15 14 ralbidv 
 |-  ( x = ( y + 1 ) -> ( A. z e. NN ( z < x -> ( x - z ) e. NN ) <-> A. z e. NN ( z < ( y + 1 ) -> ( ( y + 1 ) - z ) e. NN ) ) )
16 breq2 
 |-  ( x = B -> ( z < x <-> z < B ) )
17 oveq1 
 |-  ( x = B -> ( x - z ) = ( B - z ) )
18 17 eleq1d 
 |-  ( x = B -> ( ( x - z ) e. NN <-> ( B - z ) e. NN ) )
19 16 18 imbi12d 
 |-  ( x = B -> ( ( z < x -> ( x - z ) e. NN ) <-> ( z < B -> ( B - z ) e. NN ) ) )
20 19 ralbidv 
 |-  ( x = B -> ( A. z e. NN ( z < x -> ( x - z ) e. NN ) <-> A. z e. NN ( z < B -> ( B - z ) e. NN ) ) )
21 nnnlt1 
 |-  ( z e. NN -> -. z < 1 )
22 21 pm2.21d 
 |-  ( z e. NN -> ( z < 1 -> ( 1 - z ) e. NN ) )
23 22 rgen 
 |-  A. z e. NN ( z < 1 -> ( 1 - z ) e. NN )
24 breq1 
 |-  ( z = x -> ( z < y <-> x < y ) )
25 oveq2 
 |-  ( z = x -> ( y - z ) = ( y - x ) )
26 25 eleq1d 
 |-  ( z = x -> ( ( y - z ) e. NN <-> ( y - x ) e. NN ) )
27 24 26 imbi12d 
 |-  ( z = x -> ( ( z < y -> ( y - z ) e. NN ) <-> ( x < y -> ( y - x ) e. NN ) ) )
28 27 cbvralvw 
 |-  ( A. z e. NN ( z < y -> ( y - z ) e. NN ) <-> A. x e. NN ( x < y -> ( y - x ) e. NN ) )
29 nncn 
 |-  ( y e. NN -> y e. CC )
30 29 adantr 
 |-  ( ( y e. NN /\ z e. NN ) -> y e. CC )
31 ax-1cn 
 |-  1 e. CC
32 pncan 
 |-  ( ( y e. CC /\ 1 e. CC ) -> ( ( y + 1 ) - 1 ) = y )
33 30 31 32 sylancl 
 |-  ( ( y e. NN /\ z e. NN ) -> ( ( y + 1 ) - 1 ) = y )
34 simpl 
 |-  ( ( y e. NN /\ z e. NN ) -> y e. NN )
35 33 34 eqeltrd 
 |-  ( ( y e. NN /\ z e. NN ) -> ( ( y + 1 ) - 1 ) e. NN )
36 oveq2 
 |-  ( z = 1 -> ( ( y + 1 ) - z ) = ( ( y + 1 ) - 1 ) )
37 36 eleq1d 
 |-  ( z = 1 -> ( ( ( y + 1 ) - z ) e. NN <-> ( ( y + 1 ) - 1 ) e. NN ) )
38 35 37 syl5ibrcom 
 |-  ( ( y e. NN /\ z e. NN ) -> ( z = 1 -> ( ( y + 1 ) - z ) e. NN ) )
39 38 2a1dd 
 |-  ( ( y e. NN /\ z e. NN ) -> ( z = 1 -> ( A. x e. NN ( x < y -> ( y - x ) e. NN ) -> ( z < ( y + 1 ) -> ( ( y + 1 ) - z ) e. NN ) ) ) )
40 breq1 
 |-  ( x = ( z - 1 ) -> ( x < y <-> ( z - 1 ) < y ) )
41 oveq2 
 |-  ( x = ( z - 1 ) -> ( y - x ) = ( y - ( z - 1 ) ) )
42 41 eleq1d 
 |-  ( x = ( z - 1 ) -> ( ( y - x ) e. NN <-> ( y - ( z - 1 ) ) e. NN ) )
43 40 42 imbi12d 
 |-  ( x = ( z - 1 ) -> ( ( x < y -> ( y - x ) e. NN ) <-> ( ( z - 1 ) < y -> ( y - ( z - 1 ) ) e. NN ) ) )
44 43 rspcv 
 |-  ( ( z - 1 ) e. NN -> ( A. x e. NN ( x < y -> ( y - x ) e. NN ) -> ( ( z - 1 ) < y -> ( y - ( z - 1 ) ) e. NN ) ) )
45 nnre 
 |-  ( z e. NN -> z e. RR )
46 nnre 
 |-  ( y e. NN -> y e. RR )
47 1re 
 |-  1 e. RR
48 ltsubadd 
 |-  ( ( z e. RR /\ 1 e. RR /\ y e. RR ) -> ( ( z - 1 ) < y <-> z < ( y + 1 ) ) )
49 47 48 mp3an2 
 |-  ( ( z e. RR /\ y e. RR ) -> ( ( z - 1 ) < y <-> z < ( y + 1 ) ) )
50 45 46 49 syl2anr 
 |-  ( ( y e. NN /\ z e. NN ) -> ( ( z - 1 ) < y <-> z < ( y + 1 ) ) )
51 nncn 
 |-  ( z e. NN -> z e. CC )
52 subsub3 
 |-  ( ( y e. CC /\ z e. CC /\ 1 e. CC ) -> ( y - ( z - 1 ) ) = ( ( y + 1 ) - z ) )
53 31 52 mp3an3 
 |-  ( ( y e. CC /\ z e. CC ) -> ( y - ( z - 1 ) ) = ( ( y + 1 ) - z ) )
54 29 51 53 syl2an 
 |-  ( ( y e. NN /\ z e. NN ) -> ( y - ( z - 1 ) ) = ( ( y + 1 ) - z ) )
55 54 eleq1d 
 |-  ( ( y e. NN /\ z e. NN ) -> ( ( y - ( z - 1 ) ) e. NN <-> ( ( y + 1 ) - z ) e. NN ) )
56 50 55 imbi12d 
 |-  ( ( y e. NN /\ z e. NN ) -> ( ( ( z - 1 ) < y -> ( y - ( z - 1 ) ) e. NN ) <-> ( z < ( y + 1 ) -> ( ( y + 1 ) - z ) e. NN ) ) )
57 56 biimpd 
 |-  ( ( y e. NN /\ z e. NN ) -> ( ( ( z - 1 ) < y -> ( y - ( z - 1 ) ) e. NN ) -> ( z < ( y + 1 ) -> ( ( y + 1 ) - z ) e. NN ) ) )
58 44 57 syl9r 
 |-  ( ( y e. NN /\ z e. NN ) -> ( ( z - 1 ) e. NN -> ( A. x e. NN ( x < y -> ( y - x ) e. NN ) -> ( z < ( y + 1 ) -> ( ( y + 1 ) - z ) e. NN ) ) ) )
59 nn1m1nn 
 |-  ( z e. NN -> ( z = 1 \/ ( z - 1 ) e. NN ) )
60 59 adantl 
 |-  ( ( y e. NN /\ z e. NN ) -> ( z = 1 \/ ( z - 1 ) e. NN ) )
61 39 58 60 mpjaod 
 |-  ( ( y e. NN /\ z e. NN ) -> ( A. x e. NN ( x < y -> ( y - x ) e. NN ) -> ( z < ( y + 1 ) -> ( ( y + 1 ) - z ) e. NN ) ) )
62 61 ralrimdva 
 |-  ( y e. NN -> ( A. x e. NN ( x < y -> ( y - x ) e. NN ) -> A. z e. NN ( z < ( y + 1 ) -> ( ( y + 1 ) - z ) e. NN ) ) )
63 28 62 biimtrid 
 |-  ( y e. NN -> ( A. z e. NN ( z < y -> ( y - z ) e. NN ) -> A. z e. NN ( z < ( y + 1 ) -> ( ( y + 1 ) - z ) e. NN ) ) )
64 5 10 15 20 23 63 nnind 
 |-  ( B e. NN -> A. z e. NN ( z < B -> ( B - z ) e. NN ) )
65 breq1 
 |-  ( z = A -> ( z < B <-> A < B ) )
66 oveq2 
 |-  ( z = A -> ( B - z ) = ( B - A ) )
67 66 eleq1d 
 |-  ( z = A -> ( ( B - z ) e. NN <-> ( B - A ) e. NN ) )
68 65 67 imbi12d 
 |-  ( z = A -> ( ( z < B -> ( B - z ) e. NN ) <-> ( A < B -> ( B - A ) e. NN ) ) )
69 68 rspcva 
 |-  ( ( A e. NN /\ A. z e. NN ( z < B -> ( B - z ) e. NN ) ) -> ( A < B -> ( B - A ) e. NN ) )
70 64 69 sylan2 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A < B -> ( B - A ) e. NN ) )
71 nngt0 
 |-  ( ( B - A ) e. NN -> 0 < ( B - A ) )
72 nnre 
 |-  ( A e. NN -> A e. RR )
73 nnre 
 |-  ( B e. NN -> B e. RR )
74 posdif 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> 0 < ( B - A ) ) )
75 72 73 74 syl2an 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A < B <-> 0 < ( B - A ) ) )
76 71 75 imbitrrid 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( B - A ) e. NN -> A < B ) )
77 70 76 impbid 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A < B <-> ( B - A ) e. NN ) )