Metamath Proof Explorer


Theorem qre

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

Ref Expression
Assertion qre A A

Proof

Step Hyp Ref Expression
1 elq A x y A = x y
2 zre x x
3 nnre y y
4 nnne0 y y 0
5 3 4 jca y y y 0
6 redivcl x y y 0 x y
7 6 3expb x y y 0 x y
8 2 5 7 syl2an x y x y
9 eleq1 A = x y A x y
10 8 9 syl5ibrcom x y A = x y A
11 10 rexlimivv x y A = x y A
12 1 11 sylbi A A