Metamath Proof Explorer


Theorem nndivlub

Description: A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008)

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

Proof

Step Hyp Ref Expression
1 nnre
 |-  ( B e. NN -> B e. RR )
2 nngt0
 |-  ( B e. NN -> 0 < B )
3 1 2 jca
 |-  ( B e. NN -> ( B e. RR /\ 0 < B ) )
4 nnre
 |-  ( A e. NN -> A e. RR )
5 nngt0
 |-  ( A e. NN -> 0 < A )
6 4 5 jca
 |-  ( A e. NN -> ( A e. RR /\ 0 < A ) )
7 nnge1
 |-  ( ( A / B ) e. NN -> 1 <_ ( A / B ) )
8 lediv2
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( A e. RR /\ 0 < A ) /\ ( A e. RR /\ 0 < A ) ) -> ( B <_ A <-> ( A / A ) <_ ( A / B ) ) )
9 8 3anidm23
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( A e. RR /\ 0 < A ) ) -> ( B <_ A <-> ( A / A ) <_ ( A / B ) ) )
10 recn
 |-  ( A e. RR -> A e. CC )
11 10 adantr
 |-  ( ( A e. RR /\ 0 < A ) -> A e. CC )
12 gt0ne0
 |-  ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
13 divid
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( A / A ) = 1 )
14 13 breq1d
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( A / A ) <_ ( A / B ) <-> 1 <_ ( A / B ) ) )
15 11 12 14 syl2anc
 |-  ( ( A e. RR /\ 0 < A ) -> ( ( A / A ) <_ ( A / B ) <-> 1 <_ ( A / B ) ) )
16 15 adantl
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( A e. RR /\ 0 < A ) ) -> ( ( A / A ) <_ ( A / B ) <-> 1 <_ ( A / B ) ) )
17 9 16 bitrd
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( A e. RR /\ 0 < A ) ) -> ( B <_ A <-> 1 <_ ( A / B ) ) )
18 7 17 syl5ibr
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( A e. RR /\ 0 < A ) ) -> ( ( A / B ) e. NN -> B <_ A ) )
19 3 6 18 syl2anr
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A / B ) e. NN -> B <_ A ) )