Step |
Hyp |
Ref |
Expression |
1 |
|
nn0ge0 |
|- ( K e. NN0 -> 0 <_ K ) |
2 |
1
|
adantr |
|- ( ( K e. NN0 /\ L e. NN ) -> 0 <_ K ) |
3 |
|
elnnz |
|- ( L e. NN <-> ( L e. ZZ /\ 0 < L ) ) |
4 |
|
nn0re |
|- ( K e. NN0 -> K e. RR ) |
5 |
4
|
adantr |
|- ( ( K e. NN0 /\ ( L e. ZZ /\ 0 < L ) ) -> K e. RR ) |
6 |
|
zre |
|- ( L e. ZZ -> L e. RR ) |
7 |
6
|
ad2antrl |
|- ( ( K e. NN0 /\ ( L e. ZZ /\ 0 < L ) ) -> L e. RR ) |
8 |
|
simprr |
|- ( ( K e. NN0 /\ ( L e. ZZ /\ 0 < L ) ) -> 0 < L ) |
9 |
5 7 8
|
3jca |
|- ( ( K e. NN0 /\ ( L e. ZZ /\ 0 < L ) ) -> ( K e. RR /\ L e. RR /\ 0 < L ) ) |
10 |
3 9
|
sylan2b |
|- ( ( K e. NN0 /\ L e. NN ) -> ( K e. RR /\ L e. RR /\ 0 < L ) ) |
11 |
|
ge0div |
|- ( ( K e. RR /\ L e. RR /\ 0 < L ) -> ( 0 <_ K <-> 0 <_ ( K / L ) ) ) |
12 |
10 11
|
syl |
|- ( ( K e. NN0 /\ L e. NN ) -> ( 0 <_ K <-> 0 <_ ( K / L ) ) ) |
13 |
2 12
|
mpbid |
|- ( ( K e. NN0 /\ L e. NN ) -> 0 <_ ( K / L ) ) |