Metamath Proof Explorer

Theorem elpq

Description: A positive rational is the quotient of two positive integers. (Contributed by AV, 29-Dec-2022)

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

Proof

Step Hyp Ref Expression
1 elq 
 |-  ( A e. QQ <-> E. z e. ZZ E. y e. NN A = ( z / y ) )
2 rexcom 
 |-  ( E. z e. ZZ E. y e. NN A = ( z / y ) <-> E. y e. NN E. z e. ZZ A = ( z / y ) )
3 1 2 bitri 
 |-  ( A e. QQ <-> E. y e. NN E. z e. ZZ A = ( z / y ) )
4 breq2 
 |-  ( A = ( z / y ) -> ( 0 < A <-> 0 < ( z / y ) ) )
5 zre 
 |-  ( z e. ZZ -> z e. RR )
6 5 adantl 
 |-  ( ( y e. NN /\ z e. ZZ ) -> z e. RR )
7 nnre 
 |-  ( y e. NN -> y e. RR )
8 7 adantr 
 |-  ( ( y e. NN /\ z e. ZZ ) -> y e. RR )
9 nngt0 
 |-  ( y e. NN -> 0 < y )
10 9 adantr 
 |-  ( ( y e. NN /\ z e. ZZ ) -> 0 < y )
11 gt0div 
 |-  ( ( z e. RR /\ y e. RR /\ 0 < y ) -> ( 0 < z <-> 0 < ( z / y ) ) )
12 6 8 10 11 syl3anc 
 |-  ( ( y e. NN /\ z e. ZZ ) -> ( 0 < z <-> 0 < ( z / y ) ) )
13 12 bicomd 
 |-  ( ( y e. NN /\ z e. ZZ ) -> ( 0 < ( z / y ) <-> 0 < z ) )
14 4 13 sylan9bb 
 |-  ( ( A = ( z / y ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( 0 < A <-> 0 < z ) )
15 elnnz 
 |-  ( z e. NN <-> ( z e. ZZ /\ 0 < z ) )
16 15 simplbi2 
 |-  ( z e. ZZ -> ( 0 < z -> z e. NN ) )
17 16 adantl 
 |-  ( ( y e. NN /\ z e. ZZ ) -> ( 0 < z -> z e. NN ) )
18 17 adantl 
 |-  ( ( A = ( z / y ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( 0 < z -> z e. NN ) )
19 18 imp 
 |-  ( ( ( A = ( z / y ) /\ ( y e. NN /\ z e. ZZ ) ) /\ 0 < z ) -> z e. NN )
20 oveq1 
 |-  ( x = z -> ( x / y ) = ( z / y ) )
21 20 eqeq2d 
 |-  ( x = z -> ( A = ( x / y ) <-> A = ( z / y ) ) )
22 21 adantl 
 |-  ( ( ( ( A = ( z / y ) /\ ( y e. NN /\ z e. ZZ ) ) /\ 0 < z ) /\ x = z ) -> ( A = ( x / y ) <-> A = ( z / y ) ) )
23 simpll 
 |-  ( ( ( A = ( z / y ) /\ ( y e. NN /\ z e. ZZ ) ) /\ 0 < z ) -> A = ( z / y ) )
24 19 22 23 rspcedvd 
 |-  ( ( ( A = ( z / y ) /\ ( y e. NN /\ z e. ZZ ) ) /\ 0 < z ) -> E. x e. NN A = ( x / y ) )
25 24 ex 
 |-  ( ( A = ( z / y ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( 0 < z -> E. x e. NN A = ( x / y ) ) )
26 14 25 sylbid 
 |-  ( ( A = ( z / y ) /\ ( y e. NN /\ z e. ZZ ) ) -> ( 0 < A -> E. x e. NN A = ( x / y ) ) )
27 26 ex 
 |-  ( A = ( z / y ) -> ( ( y e. NN /\ z e. ZZ ) -> ( 0 < A -> E. x e. NN A = ( x / y ) ) ) )
28 27 com13 
 |-  ( 0 < A -> ( ( y e. NN /\ z e. ZZ ) -> ( A = ( z / y ) -> E. x e. NN A = ( x / y ) ) ) )
29 28 impl 
 |-  ( ( ( 0 < A /\ y e. NN ) /\ z e. ZZ ) -> ( A = ( z / y ) -> E. x e. NN A = ( x / y ) ) )
30 29 rexlimdva 
 |-  ( ( 0 < A /\ y e. NN ) -> ( E. z e. ZZ A = ( z / y ) -> E. x e. NN A = ( x / y ) ) )
31 30 reximdva 
 |-  ( 0 < A -> ( E. y e. NN E. z e. ZZ A = ( z / y ) -> E. y e. NN E. x e. NN A = ( x / y ) ) )
32 3 31 syl5bi 
 |-  ( 0 < A -> ( A e. QQ -> E. y e. NN E. x e. NN A = ( x / y ) ) )
33 32 impcom 
 |-  ( ( A e. QQ /\ 0 < A ) -> E. y e. NN E. x e. NN A = ( x / y ) )
34 rexcom 
 |-  ( E. x e. NN E. y e. NN A = ( x / y ) <-> E. y e. NN E. x e. NN A = ( x / y ) )
35 33 34 sylibr 
 |-  ( ( A e. QQ /\ 0 < A ) -> E. x e. NN E. y e. NN A = ( x / y ) )