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

Metamath Proof Explorer

Theorem elpqb

Description: A class is a positive rational iff it is the quotient of two positive integers. (Contributed by AV, 30-Dec-2022)

Ref Expression
Assertion elpqb 
|- ( ( A e. QQ /\ 0 < A ) <-> E. x e. NN E. y e. NN A = ( x / y ) )

Proof

Step Hyp Ref Expression
1 elpq 
 |-  ( ( A e. QQ /\ 0 < A ) -> E. x e. NN E. y e. NN A = ( x / y ) )
2 nnz 
 |-  ( x e. NN -> x e. ZZ )
3 znq 
 |-  ( ( x e. ZZ /\ y e. NN ) -> ( x / y ) e. QQ )
4 2 3 sylan 
 |-  ( ( x e. NN /\ y e. NN ) -> ( x / y ) e. QQ )
5 nnre 
 |-  ( x e. NN -> x e. RR )
6 nngt0 
 |-  ( x e. NN -> 0 < x )
7 5 6 jca 
 |-  ( x e. NN -> ( x e. RR /\ 0 < x ) )
8 nnre 
 |-  ( y e. NN -> y e. RR )
9 nngt0 
 |-  ( y e. NN -> 0 < y )
10 8 9 jca 
 |-  ( y e. NN -> ( y e. RR /\ 0 < y ) )
11 divgt0 
 |-  ( ( ( x e. RR /\ 0 < x ) /\ ( y e. RR /\ 0 < y ) ) -> 0 < ( x / y ) )
12 7 10 11 syl2an 
 |-  ( ( x e. NN /\ y e. NN ) -> 0 < ( x / y ) )
13 4 12 jca 
 |-  ( ( x e. NN /\ y e. NN ) -> ( ( x / y ) e. QQ /\ 0 < ( x / y ) ) )
14 eleq1 
 |-  ( A = ( x / y ) -> ( A e. QQ <-> ( x / y ) e. QQ ) )
15 breq2 
 |-  ( A = ( x / y ) -> ( 0 < A <-> 0 < ( x / y ) ) )
16 14 15 anbi12d 
 |-  ( A = ( x / y ) -> ( ( A e. QQ /\ 0 < A ) <-> ( ( x / y ) e. QQ /\ 0 < ( x / y ) ) ) )
17 13 16 syl5ibrcom 
 |-  ( ( x e. NN /\ y e. NN ) -> ( A = ( x / y ) -> ( A e. QQ /\ 0 < A ) ) )
18 17 rexlimivv 
 |-  ( E. x e. NN E. y e. NN A = ( x / y ) -> ( A e. QQ /\ 0 < A ) )
19 1 18 impbii 
 |-  ( ( A e. QQ /\ 0 < A ) <-> E. x e. NN E. y e. NN A = ( x / y ) )