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 ) )