Metamath Proof Explorer

Theorem nndivre

Description: The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008)

Ref Expression
Assertion nndivre A N A N


Step Hyp Ref Expression
1 nnre N N
2 nnne0 N N 0
3 1 2 jca N N N 0
4 redivcl A N N 0 A N
5 4 3expb A N N 0 A N
6 3 5 sylan2 A N A N