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

Metamath Proof Explorer

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 )