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	imbitrrid	|- ( ( ( 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 ) )