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