Theorem qre

Description: A rational number is a real number. (Contributed by NM, 14-Nov-2002)

	Ref	Expression
Assertion	qre	|- ( A e. QQ -> A e. RR )

Proof

Step	Hyp	Ref	Expression
1		elq	|- ( A e. QQ <-> E. x e. ZZ E. y e. NN A = ( x / y ) )
2		zre	|- ( x e. ZZ -> x e. RR )
3		nnre	|- ( y e. NN -> y e. RR )
4		nnne0	|- ( y e. NN -> y =/= 0 )
5	3 4	jca	|- ( y e. NN -> ( y e. RR /\ y =/= 0 ) )
6		redivcl	|- ( ( x e. RR /\ y e. RR /\ y =/= 0 ) -> ( x / y ) e. RR )
7	6	3expb	|- ( ( x e. RR /\ ( y e. RR /\ y =/= 0 ) ) -> ( x / y ) e. RR )
8	2 5 7	syl2an	|- ( ( x e. ZZ /\ y e. NN ) -> ( x / y ) e. RR )
9		eleq1	|- ( A = ( x / y ) -> ( A e. RR <-> ( x / y ) e. RR ) )
10	8 9	syl5ibrcom	|- ( ( x e. ZZ /\ y e. NN ) -> ( A = ( x / y ) -> A e. RR ) )
11	10	rexlimivv	|- ( E. x e. ZZ E. y e. NN A = ( x / y ) -> A e. RR )
12	1 11	sylbi	|- ( A e. QQ -> A e. RR )