Step |
Hyp |
Ref |
Expression |
1 |
|
elnnne0 |
|- ( L e. NN <-> ( L e. NN0 /\ L =/= 0 ) ) |
2 |
|
nn0re |
|- ( K e. NN0 -> K e. RR ) |
3 |
2
|
adantr |
|- ( ( K e. NN0 /\ ( L e. NN0 /\ L =/= 0 ) ) -> K e. RR ) |
4 |
|
nn0re |
|- ( L e. NN0 -> L e. RR ) |
5 |
4
|
ad2antrl |
|- ( ( K e. NN0 /\ ( L e. NN0 /\ L =/= 0 ) ) -> L e. RR ) |
6 |
|
simprr |
|- ( ( K e. NN0 /\ ( L e. NN0 /\ L =/= 0 ) ) -> L =/= 0 ) |
7 |
3 5 6
|
3jca |
|- ( ( K e. NN0 /\ ( L e. NN0 /\ L =/= 0 ) ) -> ( K e. RR /\ L e. RR /\ L =/= 0 ) ) |
8 |
1 7
|
sylan2b |
|- ( ( K e. NN0 /\ L e. NN ) -> ( K e. RR /\ L e. RR /\ L =/= 0 ) ) |
9 |
|
redivcl |
|- ( ( K e. RR /\ L e. RR /\ L =/= 0 ) -> ( K / L ) e. RR ) |
10 |
8 9
|
syl |
|- ( ( K e. NN0 /\ L e. NN ) -> ( K / L ) e. RR ) |