This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )