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

Metamath Proof Explorer

Theorem nnledivrp

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

Ref Expression
Assertion nnledivrp 
|- ( ( A e. NN /\ B e. RR+ ) -> ( 1 <_ B <-> ( A / B ) <_ A ) )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 0lt1 
 |-  0 < 1
3 1 2 pm3.2i 
 |-  ( 1 e. RR /\ 0 < 1 )
4 rpregt0 
 |-  ( B e. RR+ -> ( B e. RR /\ 0 < B ) )
5 4 adantl 
 |-  ( ( A e. NN /\ B e. RR+ ) -> ( B e. RR /\ 0 < B ) )
6 nnre 
 |-  ( A e. NN -> A e. RR )
7 nngt0 
 |-  ( A e. NN -> 0 < A )
8 6 7 jca 
 |-  ( A e. NN -> ( A e. RR /\ 0 < A ) )
9 8 adantr 
 |-  ( ( A e. NN /\ B e. RR+ ) -> ( A e. RR /\ 0 < A ) )
10 lediv2 
 |-  ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( B e. RR /\ 0 < B ) /\ ( A e. RR /\ 0 < A ) ) -> ( 1 <_ B <-> ( A / B ) <_ ( A / 1 ) ) )
11 3 5 9 10 mp3an2i 
 |-  ( ( A e. NN /\ B e. RR+ ) -> ( 1 <_ B <-> ( A / B ) <_ ( A / 1 ) ) )
12 nncn 
 |-  ( A e. NN -> A e. CC )
13 12 div1d 
 |-  ( A e. NN -> ( A / 1 ) = A )
14 13 adantr 
 |-  ( ( A e. NN /\ B e. RR+ ) -> ( A / 1 ) = A )
15 14 breq2d 
 |-  ( ( A e. NN /\ B e. RR+ ) -> ( ( A / B ) <_ ( A / 1 ) <-> ( A / B ) <_ A ) )
16 11 15 bitrd 
 |-  ( ( A e. NN /\ B e. RR+ ) -> ( 1 <_ B <-> ( A / B ) <_ A ) )