Metamath Proof Explorer

Theorem elq2

Description: Elementhood in the rational numbers, providing the canonical representation. (Contributed by Thierry Arnoux, 9-Nov-2025)

Ref Expression
Assertion elq2 
|- ( Q e. QQ -> E. p e. ZZ E. q e. NN ( Q = ( p / q ) /\ ( p gcd q ) = 1 ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( p = ( x / ( x gcd y ) ) -> ( p / q ) = ( ( x / ( x gcd y ) ) / q ) )
2 1 eqeq2d 
 |-  ( p = ( x / ( x gcd y ) ) -> ( Q = ( p / q ) <-> Q = ( ( x / ( x gcd y ) ) / q ) ) )
3 oveq1 
 |-  ( p = ( x / ( x gcd y ) ) -> ( p gcd q ) = ( ( x / ( x gcd y ) ) gcd q ) )
4 3 eqeq1d 
 |-  ( p = ( x / ( x gcd y ) ) -> ( ( p gcd q ) = 1 <-> ( ( x / ( x gcd y ) ) gcd q ) = 1 ) )
5 2 4 anbi12d 
 |-  ( p = ( x / ( x gcd y ) ) -> ( ( Q = ( p / q ) /\ ( p gcd q ) = 1 ) <-> ( Q = ( ( x / ( x gcd y ) ) / q ) /\ ( ( x / ( x gcd y ) ) gcd q ) = 1 ) ) )
6 oveq2 
 |-  ( q = ( y / ( x gcd y ) ) -> ( ( x / ( x gcd y ) ) / q ) = ( ( x / ( x gcd y ) ) / ( y / ( x gcd y ) ) ) )
7 6 eqeq2d 
 |-  ( q = ( y / ( x gcd y ) ) -> ( Q = ( ( x / ( x gcd y ) ) / q ) <-> Q = ( ( x / ( x gcd y ) ) / ( y / ( x gcd y ) ) ) ) )
8 oveq2 
 |-  ( q = ( y / ( x gcd y ) ) -> ( ( x / ( x gcd y ) ) gcd q ) = ( ( x / ( x gcd y ) ) gcd ( y / ( x gcd y ) ) ) )
9 8 eqeq1d 
 |-  ( q = ( y / ( x gcd y ) ) -> ( ( ( x / ( x gcd y ) ) gcd q ) = 1 <-> ( ( x / ( x gcd y ) ) gcd ( y / ( x gcd y ) ) ) = 1 ) )
10 7 9 anbi12d 
 |-  ( q = ( y / ( x gcd y ) ) -> ( ( Q = ( ( x / ( x gcd y ) ) / q ) /\ ( ( x / ( x gcd y ) ) gcd q ) = 1 ) <-> ( Q = ( ( x / ( x gcd y ) ) / ( y / ( x gcd y ) ) ) /\ ( ( x / ( x gcd y ) ) gcd ( y / ( x gcd y ) ) ) = 1 ) ) )
11 simpllr 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> x e. ZZ )
12 simplr 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> y e. NN )
13 12 nnzd 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> y e. ZZ )
14 12 nnne0d 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> y =/= 0 )
15 divgcdz 
 |-  ( ( x e. ZZ /\ y e. ZZ /\ y =/= 0 ) -> ( x / ( x gcd y ) ) e. ZZ )
16 11 13 14 15 syl3anc 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> ( x / ( x gcd y ) ) e. ZZ )
17 divgcdnnr 
 |-  ( ( y e. NN /\ x e. ZZ ) -> ( y / ( x gcd y ) ) e. NN )
18 12 11 17 syl2anc 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> ( y / ( x gcd y ) ) e. NN )
19 simpr 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> Q = ( x / y ) )
20 11 zcnd 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> x e. CC )
21 12 nncnd 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> y e. CC )
22 11 13 gcdcld 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> ( x gcd y ) e. NN0 )
23 22 nn0cnd 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> ( x gcd y ) e. CC )
24 14 neneqd 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> -. y = 0 )
25 24 intnand 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> -. ( x = 0 /\ y = 0 ) )
26 gcdeq0 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( x gcd y ) = 0 <-> ( x = 0 /\ y = 0 ) ) )
27 26 necon3abid 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( x gcd y ) =/= 0 <-> -. ( x = 0 /\ y = 0 ) ) )
28 27 biimpar 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ -. ( x = 0 /\ y = 0 ) ) -> ( x gcd y ) =/= 0 )
29 11 13 25 28 syl21anc 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> ( x gcd y ) =/= 0 )
30 20 21 23 14 29 divcan7d 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> ( ( x / ( x gcd y ) ) / ( y / ( x gcd y ) ) ) = ( x / y ) )
31 19 30 eqtr4d 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> Q = ( ( x / ( x gcd y ) ) / ( y / ( x gcd y ) ) ) )
32 divgcdcoprm0 
 |-  ( ( x e. ZZ /\ y e. ZZ /\ y =/= 0 ) -> ( ( x / ( x gcd y ) ) gcd ( y / ( x gcd y ) ) ) = 1 )
33 11 13 14 32 syl3anc 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> ( ( x / ( x gcd y ) ) gcd ( y / ( x gcd y ) ) ) = 1 )
34 31 33 jca 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> ( Q = ( ( x / ( x gcd y ) ) / ( y / ( x gcd y ) ) ) /\ ( ( x / ( x gcd y ) ) gcd ( y / ( x gcd y ) ) ) = 1 ) )
35 5 10 16 18 34 2rspcedvdw 
 |-  ( ( ( ( Q e. QQ /\ x e. ZZ ) /\ y e. NN ) /\ Q = ( x / y ) ) -> E. p e. ZZ E. q e. NN ( Q = ( p / q ) /\ ( p gcd q ) = 1 ) )
36 elq 
 |-  ( Q e. QQ <-> E. x e. ZZ E. y e. NN Q = ( x / y ) )
37 36 biimpi 
 |-  ( Q e. QQ -> E. x e. ZZ E. y e. NN Q = ( x / y ) )
38 35 37 r19.29vva 
 |-  ( Q e. QQ -> E. p e. ZZ E. q e. NN ( Q = ( p / q ) /\ ( p gcd q ) = 1 ) )