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 e. RR /\ N e. NN ) -> ( A / N ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		nnre	|- ( N e. NN -> N e. RR )
2		nnne0	|- ( N e. NN -> N =/= 0 )
3	1 2	jca	|- ( N e. NN -> ( N e. RR /\ N =/= 0 ) )
4		redivcl	|- ( ( A e. RR /\ N e. RR /\ N =/= 0 ) -> ( A / N ) e. RR )
5	4	3expb	|- ( ( A e. RR /\ ( N e. RR /\ N =/= 0 ) ) -> ( A / N ) e. RR )
6	3 5	sylan2	|- ( ( A e. RR /\ N e. NN ) -> ( A / N ) e. RR )