Metamath Proof Explorer

Theorem nndivsub

Description: Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008)

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

Proof

Step Hyp Ref Expression
1 nnre 
 |-  ( A e. NN -> A e. RR )
2 nnre 
 |-  ( B e. NN -> B e. RR )
3 nnre 
 |-  ( C e. NN -> C e. RR )
4 nngt0 
 |-  ( C e. NN -> 0 < C )
5 3 4 jca 
 |-  ( C e. NN -> ( C e. RR /\ 0 < C ) )
6 ltdiv1 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( A / C ) < ( B / C ) ) )
7 1 2 5 6 syl3an 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( A < B <-> ( A / C ) < ( B / C ) ) )
8 nnsub 
 |-  ( ( ( A / C ) e. NN /\ ( B / C ) e. NN ) -> ( ( A / C ) < ( B / C ) <-> ( ( B / C ) - ( A / C ) ) e. NN ) )
9 7 8 sylan9bb 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A / C ) e. NN /\ ( B / C ) e. NN ) ) -> ( A < B <-> ( ( B / C ) - ( A / C ) ) e. NN ) )
10 9 biimpd 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A / C ) e. NN /\ ( B / C ) e. NN ) ) -> ( A < B -> ( ( B / C ) - ( A / C ) ) e. NN ) )
11 10 exp32 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A / C ) e. NN -> ( ( B / C ) e. NN -> ( A < B -> ( ( B / C ) - ( A / C ) ) e. NN ) ) ) )
12 11 com34 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A / C ) e. NN -> ( A < B -> ( ( B / C ) e. NN -> ( ( B / C ) - ( A / C ) ) e. NN ) ) ) )
13 12 imp32 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A / C ) e. NN /\ A < B ) ) -> ( ( B / C ) e. NN -> ( ( B / C ) - ( A / C ) ) e. NN ) )
14 nnaddcl 
 |-  ( ( ( ( B / C ) - ( A / C ) ) e. NN /\ ( A / C ) e. NN ) -> ( ( ( B / C ) - ( A / C ) ) + ( A / C ) ) e. NN )
15 14 expcom 
 |-  ( ( A / C ) e. NN -> ( ( ( B / C ) - ( A / C ) ) e. NN -> ( ( ( B / C ) - ( A / C ) ) + ( A / C ) ) e. NN ) )
16 nnsscn 
 |-  NN C_ CC
17 nnne0 
 |-  ( C e. NN -> C =/= 0 )
18 divcl 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( A / C ) e. CC )
19 16 17 18 nnssi2 
 |-  ( ( A e. NN /\ C e. NN ) -> ( A / C ) e. CC )
20 divcl 
 |-  ( ( B e. CC /\ C e. CC /\ C =/= 0 ) -> ( B / C ) e. CC )
21 16 17 20 nnssi2 
 |-  ( ( B e. NN /\ C e. NN ) -> ( B / C ) e. CC )
22 19 21 anim12i 
 |-  ( ( ( A e. NN /\ C e. NN ) /\ ( B e. NN /\ C e. NN ) ) -> ( ( A / C ) e. CC /\ ( B / C ) e. CC ) )
23 22 3impdir 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( A / C ) e. CC /\ ( B / C ) e. CC ) )
24 npcan 
 |-  ( ( ( B / C ) e. CC /\ ( A / C ) e. CC ) -> ( ( ( B / C ) - ( A / C ) ) + ( A / C ) ) = ( B / C ) )
25 24 ancoms 
 |-  ( ( ( A / C ) e. CC /\ ( B / C ) e. CC ) -> ( ( ( B / C ) - ( A / C ) ) + ( A / C ) ) = ( B / C ) )
26 23 25 syl 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( B / C ) - ( A / C ) ) + ( A / C ) ) = ( B / C ) )
27 26 eleq1d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( ( B / C ) - ( A / C ) ) + ( A / C ) ) e. NN <-> ( B / C ) e. NN ) )
28 27 biimpd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( ( B / C ) - ( A / C ) ) + ( A / C ) ) e. NN -> ( B / C ) e. NN ) )
29 15 28 sylan9r 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( A / C ) e. NN ) -> ( ( ( B / C ) - ( A / C ) ) e. NN -> ( B / C ) e. NN ) )
30 29 adantrr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A / C ) e. NN /\ A < B ) ) -> ( ( ( B / C ) - ( A / C ) ) e. NN -> ( B / C ) e. NN ) )
31 13 30 impbid 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A / C ) e. NN /\ A < B ) ) -> ( ( B / C ) e. NN <-> ( ( B / C ) - ( A / C ) ) e. NN ) )
32 nncn 
 |-  ( B e. NN -> B e. CC )
33 32 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> B e. CC )
34 nncn 
 |-  ( A e. NN -> A e. CC )
35 34 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> A e. CC )
36 nncn 
 |-  ( C e. NN -> C e. CC )
37 36 17 jca 
 |-  ( C e. NN -> ( C e. CC /\ C =/= 0 ) )
38 37 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( C e. CC /\ C =/= 0 ) )
39 divsubdir 
 |-  ( ( B e. CC /\ A e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( B - A ) / C ) = ( ( B / C ) - ( A / C ) ) )
40 33 35 38 39 syl3anc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( B - A ) / C ) = ( ( B / C ) - ( A / C ) ) )
41 40 eleq1d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ( ( ( B - A ) / C ) e. NN <-> ( ( B / C ) - ( A / C ) ) e. NN ) )
42 41 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A / C ) e. NN /\ A < B ) ) -> ( ( ( B - A ) / C ) e. NN <-> ( ( B / C ) - ( A / C ) ) e. NN ) )
43 31 42 bitr4d 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A / C ) e. NN /\ A < B ) ) -> ( ( B / C ) e. NN <-> ( ( B - A ) / C ) e. NN ) )