Theorem nn0ledivnn

Description: Division of a nonnegative integer by a positive integer is less than or equal to the integer. (Contributed by AV, 19-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		elnn0	|- ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )
2		nnge1	|- ( B e. NN -> 1 <_ B )
3	2	adantl	|- ( ( A e. NN /\ B e. NN ) -> 1 <_ B )
4		nnrp	|- ( B e. NN -> B e. RR+ )
5		nnledivrp	|- ( ( A e. NN /\ B e. RR+ ) -> ( 1 <_ B <-> ( A / B ) <_ A ) )
6	4 5	sylan2	|- ( ( A e. NN /\ B e. NN ) -> ( 1 <_ B <-> ( A / B ) <_ A ) )
7	3 6	mpbid	|- ( ( A e. NN /\ B e. NN ) -> ( A / B ) <_ A )
8	7	ex	|- ( A e. NN -> ( B e. NN -> ( A / B ) <_ A ) )
9		nncn	|- ( B e. NN -> B e. CC )
10		nnne0	|- ( B e. NN -> B =/= 0 )
11	9 10	jca	|- ( B e. NN -> ( B e. CC /\ B =/= 0 ) )
12	11	adantl	|- ( ( A = 0 /\ B e. NN ) -> ( B e. CC /\ B =/= 0 ) )
13		div0	|- ( ( B e. CC /\ B =/= 0 ) -> ( 0 / B ) = 0 )
14	12 13	syl	|- ( ( A = 0 /\ B e. NN ) -> ( 0 / B ) = 0 )
15		0le0	|- 0 <_ 0
16	14 15	eqbrtrdi	|- ( ( A = 0 /\ B e. NN ) -> ( 0 / B ) <_ 0 )
17		oveq1	|- ( A = 0 -> ( A / B ) = ( 0 / B ) )
18		id	|- ( A = 0 -> A = 0 )
19	17 18	breq12d	|- ( A = 0 -> ( ( A / B ) <_ A <-> ( 0 / B ) <_ 0 ) )
20	19	adantr	|- ( ( A = 0 /\ B e. NN ) -> ( ( A / B ) <_ A <-> ( 0 / B ) <_ 0 ) )
21	16 20	mpbird	|- ( ( A = 0 /\ B e. NN ) -> ( A / B ) <_ A )
22	21	ex	|- ( A = 0 -> ( B e. NN -> ( A / B ) <_ A ) )
23	8 22	jaoi	|- ( ( A e. NN \/ A = 0 ) -> ( B e. NN -> ( A / B ) <_ A ) )
24	1 23	sylbi	|- ( A e. NN0 -> ( B e. NN -> ( A / B ) <_ A ) )
25	24	imp	|- ( ( A e. NN0 /\ B e. NN ) -> ( A / B ) <_ A )