Metamath Proof Explorer

Theorem qnumdenbi

Description: Two numbers are the canonical representation of a rational iff they are coprime and have the right quotient. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion qnumdenbi 
|- ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> ( ( ( B gcd C ) = 1 /\ A = ( B / C ) ) <-> ( ( numer ` A ) = B /\ ( denom ` A ) = C ) ) )

Proof

Step Hyp Ref Expression
1 qredeu 
 |-  ( A e. QQ -> E! a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) )
2 riotacl 
 |-  ( E! a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) -> ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) e. ( ZZ X. NN ) )
3 1st2nd2 
 |-  ( ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) e. ( ZZ X. NN ) -> ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) = <. ( 1st ` ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) ) , ( 2nd ` ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) ) >. )
4 1 2 3 3syl 
 |-  ( A e. QQ -> ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) = <. ( 1st ` ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) ) , ( 2nd ` ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) ) >. )
5 qnumval 
 |-  ( A e. QQ -> ( numer ` A ) = ( 1st ` ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) ) )
6 qdenval 
 |-  ( A e. QQ -> ( denom ` A ) = ( 2nd ` ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) ) )
7 5 6 opeq12d 
 |-  ( A e. QQ -> <. ( numer ` A ) , ( denom ` A ) >. = <. ( 1st ` ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) ) , ( 2nd ` ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) ) >. )
8 4 7 eqtr4d 
 |-  ( A e. QQ -> ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) = <. ( numer ` A ) , ( denom ` A ) >. )
9 8 eqeq1d 
 |-  ( A e. QQ -> ( ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) = <. B , C >. <-> <. ( numer ` A ) , ( denom ` A ) >. = <. B , C >. ) )
10 9 3ad2ant1 
 |-  ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> ( ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) = <. B , C >. <-> <. ( numer ` A ) , ( denom ` A ) >. = <. B , C >. ) )
11 fvex 
 |-  ( numer ` A ) e. _V
12 fvex 
 |-  ( denom ` A ) e. _V
13 11 12 opth 
 |-  ( <. ( numer ` A ) , ( denom ` A ) >. = <. B , C >. <-> ( ( numer ` A ) = B /\ ( denom ` A ) = C ) )
14 10 13 bitr2di 
 |-  ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> ( ( ( numer ` A ) = B /\ ( denom ` A ) = C ) <-> ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) = <. B , C >. ) )
15 opelxpi 
 |-  ( ( B e. ZZ /\ C e. NN ) -> <. B , C >. e. ( ZZ X. NN ) )
16 15 3adant1 
 |-  ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> <. B , C >. e. ( ZZ X. NN ) )
17 1 3ad2ant1 
 |-  ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> E! a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) )
18 fveq2 
 |-  ( a = <. B , C >. -> ( 1st ` a ) = ( 1st ` <. B , C >. ) )
19 fveq2 
 |-  ( a = <. B , C >. -> ( 2nd ` a ) = ( 2nd ` <. B , C >. ) )
20 18 19 oveq12d 
 |-  ( a = <. B , C >. -> ( ( 1st ` a ) gcd ( 2nd ` a ) ) = ( ( 1st ` <. B , C >. ) gcd ( 2nd ` <. B , C >. ) ) )
21 20 eqeq1d 
 |-  ( a = <. B , C >. -> ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 <-> ( ( 1st ` <. B , C >. ) gcd ( 2nd ` <. B , C >. ) ) = 1 ) )
22 18 19 oveq12d 
 |-  ( a = <. B , C >. -> ( ( 1st ` a ) / ( 2nd ` a ) ) = ( ( 1st ` <. B , C >. ) / ( 2nd ` <. B , C >. ) ) )
23 22 eqeq2d 
 |-  ( a = <. B , C >. -> ( A = ( ( 1st ` a ) / ( 2nd ` a ) ) <-> A = ( ( 1st ` <. B , C >. ) / ( 2nd ` <. B , C >. ) ) ) )
24 21 23 anbi12d 
 |-  ( a = <. B , C >. -> ( ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) <-> ( ( ( 1st ` <. B , C >. ) gcd ( 2nd ` <. B , C >. ) ) = 1 /\ A = ( ( 1st ` <. B , C >. ) / ( 2nd ` <. B , C >. ) ) ) ) )
25 24 riota2 
 |-  ( ( <. B , C >. e. ( ZZ X. NN ) /\ E! a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) -> ( ( ( ( 1st ` <. B , C >. ) gcd ( 2nd ` <. B , C >. ) ) = 1 /\ A = ( ( 1st ` <. B , C >. ) / ( 2nd ` <. B , C >. ) ) ) <-> ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) = <. B , C >. ) )
26 16 17 25 syl2anc 
 |-  ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> ( ( ( ( 1st ` <. B , C >. ) gcd ( 2nd ` <. B , C >. ) ) = 1 /\ A = ( ( 1st ` <. B , C >. ) / ( 2nd ` <. B , C >. ) ) ) <-> ( iota_ a e. ( ZZ X. NN ) ( ( ( 1st ` a ) gcd ( 2nd ` a ) ) = 1 /\ A = ( ( 1st ` a ) / ( 2nd ` a ) ) ) ) = <. B , C >. ) )
27 op1stg 
 |-  ( ( B e. ZZ /\ C e. NN ) -> ( 1st ` <. B , C >. ) = B )
28 op2ndg 
 |-  ( ( B e. ZZ /\ C e. NN ) -> ( 2nd ` <. B , C >. ) = C )
29 27 28 oveq12d 
 |-  ( ( B e. ZZ /\ C e. NN ) -> ( ( 1st ` <. B , C >. ) gcd ( 2nd ` <. B , C >. ) ) = ( B gcd C ) )
30 29 3adant1 
 |-  ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> ( ( 1st ` <. B , C >. ) gcd ( 2nd ` <. B , C >. ) ) = ( B gcd C ) )
31 30 eqeq1d 
 |-  ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> ( ( ( 1st ` <. B , C >. ) gcd ( 2nd ` <. B , C >. ) ) = 1 <-> ( B gcd C ) = 1 ) )
32 27 3adant1 
 |-  ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> ( 1st ` <. B , C >. ) = B )
33 28 3adant1 
 |-  ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> ( 2nd ` <. B , C >. ) = C )
34 32 33 oveq12d 
 |-  ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> ( ( 1st ` <. B , C >. ) / ( 2nd ` <. B , C >. ) ) = ( B / C ) )
35 34 eqeq2d 
 |-  ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> ( A = ( ( 1st ` <. B , C >. ) / ( 2nd ` <. B , C >. ) ) <-> A = ( B / C ) ) )
36 31 35 anbi12d 
 |-  ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> ( ( ( ( 1st ` <. B , C >. ) gcd ( 2nd ` <. B , C >. ) ) = 1 /\ A = ( ( 1st ` <. B , C >. ) / ( 2nd ` <. B , C >. ) ) ) <-> ( ( B gcd C ) = 1 /\ A = ( B / C ) ) ) )
37 14 26 36 3bitr2rd 
 |-  ( ( A e. QQ /\ B e. ZZ /\ C e. NN ) -> ( ( ( B gcd C ) = 1 /\ A = ( B / C ) ) <-> ( ( numer ` A ) = B /\ ( denom ` A ) = C ) ) )