Metamath Proof Explorer

Theorem qredeu

Description: Every rational number has a unique reduced form. (Contributed by Jeff Hankins, 29-Sep-2013)

Ref Expression
Assertion qredeu 
|- ( A e. QQ -> E! x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( n e. NN -> n e. ZZ )
2 gcddvds 
 |-  ( ( z e. ZZ /\ n e. ZZ ) -> ( ( z gcd n ) || z /\ ( z gcd n ) || n ) )
3 2 simpld 
 |-  ( ( z e. ZZ /\ n e. ZZ ) -> ( z gcd n ) || z )
4 1 3 sylan2 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( z gcd n ) || z )
5 gcdcl 
 |-  ( ( z e. ZZ /\ n e. ZZ ) -> ( z gcd n ) e. NN0 )
6 1 5 sylan2 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( z gcd n ) e. NN0 )
7 6 nn0zd 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( z gcd n ) e. ZZ )
8 simpl 
 |-  ( ( z e. ZZ /\ n e. NN ) -> z e. ZZ )
9 1 adantl 
 |-  ( ( z e. ZZ /\ n e. NN ) -> n e. ZZ )
10 nnne0 
 |-  ( n e. NN -> n =/= 0 )
11 10 neneqd 
 |-  ( n e. NN -> -. n = 0 )
12 11 intnand 
 |-  ( n e. NN -> -. ( z = 0 /\ n = 0 ) )
13 12 adantl 
 |-  ( ( z e. ZZ /\ n e. NN ) -> -. ( z = 0 /\ n = 0 ) )
14 gcdn0cl 
 |-  ( ( ( z e. ZZ /\ n e. ZZ ) /\ -. ( z = 0 /\ n = 0 ) ) -> ( z gcd n ) e. NN )
15 8 9 13 14 syl21anc 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( z gcd n ) e. NN )
16 nnne0 
 |-  ( ( z gcd n ) e. NN -> ( z gcd n ) =/= 0 )
17 15 16 syl 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( z gcd n ) =/= 0 )
18 dvdsval2 
 |-  ( ( ( z gcd n ) e. ZZ /\ ( z gcd n ) =/= 0 /\ z e. ZZ ) -> ( ( z gcd n ) || z <-> ( z / ( z gcd n ) ) e. ZZ ) )
19 7 17 8 18 syl3anc 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( ( z gcd n ) || z <-> ( z / ( z gcd n ) ) e. ZZ ) )
20 4 19 mpbid 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( z / ( z gcd n ) ) e. ZZ )
21 20 3adant3 
 |-  ( ( z e. ZZ /\ n e. NN /\ A = ( z / n ) ) -> ( z / ( z gcd n ) ) e. ZZ )
22 2 simprd 
 |-  ( ( z e. ZZ /\ n e. ZZ ) -> ( z gcd n ) || n )
23 1 22 sylan2 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( z gcd n ) || n )
24 dvdsval2 
 |-  ( ( ( z gcd n ) e. ZZ /\ ( z gcd n ) =/= 0 /\ n e. ZZ ) -> ( ( z gcd n ) || n <-> ( n / ( z gcd n ) ) e. ZZ ) )
25 7 17 9 24 syl3anc 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( ( z gcd n ) || n <-> ( n / ( z gcd n ) ) e. ZZ ) )
26 23 25 mpbid 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( n / ( z gcd n ) ) e. ZZ )
27 nnre 
 |-  ( n e. NN -> n e. RR )
28 27 adantl 
 |-  ( ( z e. ZZ /\ n e. NN ) -> n e. RR )
29 6 nn0red 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( z gcd n ) e. RR )
30 nngt0 
 |-  ( n e. NN -> 0 < n )
31 30 adantl 
 |-  ( ( z e. ZZ /\ n e. NN ) -> 0 < n )
32 nngt0 
 |-  ( ( z gcd n ) e. NN -> 0 < ( z gcd n ) )
33 15 32 syl 
 |-  ( ( z e. ZZ /\ n e. NN ) -> 0 < ( z gcd n ) )
34 28 29 31 33 divgt0d 
 |-  ( ( z e. ZZ /\ n e. NN ) -> 0 < ( n / ( z gcd n ) ) )
35 26 34 jca 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( ( n / ( z gcd n ) ) e. ZZ /\ 0 < ( n / ( z gcd n ) ) ) )
36 35 3adant3 
 |-  ( ( z e. ZZ /\ n e. NN /\ A = ( z / n ) ) -> ( ( n / ( z gcd n ) ) e. ZZ /\ 0 < ( n / ( z gcd n ) ) ) )
37 elnnz 
 |-  ( ( n / ( z gcd n ) ) e. NN <-> ( ( n / ( z gcd n ) ) e. ZZ /\ 0 < ( n / ( z gcd n ) ) ) )
38 36 37 sylibr 
 |-  ( ( z e. ZZ /\ n e. NN /\ A = ( z / n ) ) -> ( n / ( z gcd n ) ) e. NN )
39 21 38 opelxpd 
 |-  ( ( z e. ZZ /\ n e. NN /\ A = ( z / n ) ) -> <. ( z / ( z gcd n ) ) , ( n / ( z gcd n ) ) >. e. ( ZZ X. NN ) )
40 20 26 gcdcld 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( ( z / ( z gcd n ) ) gcd ( n / ( z gcd n ) ) ) e. NN0 )
41 40 nn0cnd 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( ( z / ( z gcd n ) ) gcd ( n / ( z gcd n ) ) ) e. CC )
42 1cnd 
 |-  ( ( z e. ZZ /\ n e. NN ) -> 1 e. CC )
43 6 nn0cnd 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( z gcd n ) e. CC )
44 43 mulid1d 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( ( z gcd n ) x. 1 ) = ( z gcd n ) )
45 zcn 
 |-  ( z e. ZZ -> z e. CC )
46 45 adantr 
 |-  ( ( z e. ZZ /\ n e. NN ) -> z e. CC )
47 46 43 17 divcan2d 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( ( z gcd n ) x. ( z / ( z gcd n ) ) ) = z )
48 nncn 
 |-  ( n e. NN -> n e. CC )
49 48 adantl 
 |-  ( ( z e. ZZ /\ n e. NN ) -> n e. CC )
50 49 43 17 divcan2d 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( ( z gcd n ) x. ( n / ( z gcd n ) ) ) = n )
51 47 50 oveq12d 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( ( ( z gcd n ) x. ( z / ( z gcd n ) ) ) gcd ( ( z gcd n ) x. ( n / ( z gcd n ) ) ) ) = ( z gcd n ) )
52 mulgcd 
 |-  ( ( ( z gcd n ) e. NN0 /\ ( z / ( z gcd n ) ) e. ZZ /\ ( n / ( z gcd n ) ) e. ZZ ) -> ( ( ( z gcd n ) x. ( z / ( z gcd n ) ) ) gcd ( ( z gcd n ) x. ( n / ( z gcd n ) ) ) ) = ( ( z gcd n ) x. ( ( z / ( z gcd n ) ) gcd ( n / ( z gcd n ) ) ) ) )
53 6 20 26 52 syl3anc 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( ( ( z gcd n ) x. ( z / ( z gcd n ) ) ) gcd ( ( z gcd n ) x. ( n / ( z gcd n ) ) ) ) = ( ( z gcd n ) x. ( ( z / ( z gcd n ) ) gcd ( n / ( z gcd n ) ) ) ) )
54 44 51 53 3eqtr2rd 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( ( z gcd n ) x. ( ( z / ( z gcd n ) ) gcd ( n / ( z gcd n ) ) ) ) = ( ( z gcd n ) x. 1 ) )
55 41 42 43 17 54 mulcanad 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( ( z / ( z gcd n ) ) gcd ( n / ( z gcd n ) ) ) = 1 )
56 55 3adant3 
 |-  ( ( z e. ZZ /\ n e. NN /\ A = ( z / n ) ) -> ( ( z / ( z gcd n ) ) gcd ( n / ( z gcd n ) ) ) = 1 )
57 10 adantl 
 |-  ( ( z e. ZZ /\ n e. NN ) -> n =/= 0 )
58 46 49 43 57 17 divcan7d 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( ( z / ( z gcd n ) ) / ( n / ( z gcd n ) ) ) = ( z / n ) )
59 58 eqeq2d 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( A = ( ( z / ( z gcd n ) ) / ( n / ( z gcd n ) ) ) <-> A = ( z / n ) ) )
60 59 biimp3ar 
 |-  ( ( z e. ZZ /\ n e. NN /\ A = ( z / n ) ) -> A = ( ( z / ( z gcd n ) ) / ( n / ( z gcd n ) ) ) )
61 ovex 
 |-  ( z / ( z gcd n ) ) e. _V
62 ovex 
 |-  ( n / ( z gcd n ) ) e. _V
63 61 62 op1std 
 |-  ( x = <. ( z / ( z gcd n ) ) , ( n / ( z gcd n ) ) >. -> ( 1st ` x ) = ( z / ( z gcd n ) ) )
64 61 62 op2ndd 
 |-  ( x = <. ( z / ( z gcd n ) ) , ( n / ( z gcd n ) ) >. -> ( 2nd ` x ) = ( n / ( z gcd n ) ) )
65 63 64 oveq12d 
 |-  ( x = <. ( z / ( z gcd n ) ) , ( n / ( z gcd n ) ) >. -> ( ( 1st ` x ) gcd ( 2nd ` x ) ) = ( ( z / ( z gcd n ) ) gcd ( n / ( z gcd n ) ) ) )
66 65 eqeq1d 
 |-  ( x = <. ( z / ( z gcd n ) ) , ( n / ( z gcd n ) ) >. -> ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 <-> ( ( z / ( z gcd n ) ) gcd ( n / ( z gcd n ) ) ) = 1 ) )
67 63 64 oveq12d 
 |-  ( x = <. ( z / ( z gcd n ) ) , ( n / ( z gcd n ) ) >. -> ( ( 1st ` x ) / ( 2nd ` x ) ) = ( ( z / ( z gcd n ) ) / ( n / ( z gcd n ) ) ) )
68 67 eqeq2d 
 |-  ( x = <. ( z / ( z gcd n ) ) , ( n / ( z gcd n ) ) >. -> ( A = ( ( 1st ` x ) / ( 2nd ` x ) ) <-> A = ( ( z / ( z gcd n ) ) / ( n / ( z gcd n ) ) ) ) )
69 66 68 anbi12d 
 |-  ( x = <. ( z / ( z gcd n ) ) , ( n / ( z gcd n ) ) >. -> ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) <-> ( ( ( z / ( z gcd n ) ) gcd ( n / ( z gcd n ) ) ) = 1 /\ A = ( ( z / ( z gcd n ) ) / ( n / ( z gcd n ) ) ) ) ) )
70 69 rspcev 
 |-  ( ( <. ( z / ( z gcd n ) ) , ( n / ( z gcd n ) ) >. e. ( ZZ X. NN ) /\ ( ( ( z / ( z gcd n ) ) gcd ( n / ( z gcd n ) ) ) = 1 /\ A = ( ( z / ( z gcd n ) ) / ( n / ( z gcd n ) ) ) ) ) -> E. x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) )
71 39 56 60 70 syl12anc 
 |-  ( ( z e. ZZ /\ n e. NN /\ A = ( z / n ) ) -> E. x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) )
72 elxp6 
 |-  ( x e. ( ZZ X. NN ) <-> ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) )
73 elxp6 
 |-  ( y e. ( ZZ X. NN ) <-> ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) )
74 simprl 
 |-  ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) -> ( 1st ` x ) e. ZZ )
75 74 ad2antrr 
 |-  ( ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) /\ ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) ) -> ( 1st ` x ) e. ZZ )
76 simprr 
 |-  ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) -> ( 2nd ` x ) e. NN )
77 76 ad2antrr 
 |-  ( ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) /\ ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) ) -> ( 2nd ` x ) e. NN )
78 simprll 
 |-  ( ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) /\ ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) ) -> ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 )
79 simprl 
 |-  ( ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) -> ( 1st ` y ) e. ZZ )
80 79 ad2antlr 
 |-  ( ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) /\ ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) ) -> ( 1st ` y ) e. ZZ )
81 simprr 
 |-  ( ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) -> ( 2nd ` y ) e. NN )
82 81 ad2antlr 
 |-  ( ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) /\ ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) ) -> ( 2nd ` y ) e. NN )
83 simprrl 
 |-  ( ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) /\ ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) ) -> ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 )
84 simprlr 
 |-  ( ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) /\ ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) ) -> A = ( ( 1st ` x ) / ( 2nd ` x ) ) )
85 simprrr 
 |-  ( ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) /\ ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) ) -> A = ( ( 1st ` y ) / ( 2nd ` y ) ) )
86 84 85 eqtr3d 
 |-  ( ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) /\ ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) ) -> ( ( 1st ` x ) / ( 2nd ` x ) ) = ( ( 1st ` y ) / ( 2nd ` y ) ) )
87 qredeq 
 |-  ( ( ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN /\ ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 ) /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN /\ ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 ) /\ ( ( 1st ` x ) / ( 2nd ` x ) ) = ( ( 1st ` y ) / ( 2nd ` y ) ) ) -> ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) )
88 75 77 78 80 82 83 86 87 syl331anc 
 |-  ( ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) /\ ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) ) -> ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) )
89 fvex 
 |-  ( 1st ` x ) e. _V
90 fvex 
 |-  ( 2nd ` x ) e. _V
91 89 90 opth 
 |-  ( <. ( 1st ` x ) , ( 2nd ` x ) >. = <. ( 1st ` y ) , ( 2nd ` y ) >. <-> ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) )
92 88 91 sylibr 
 |-  ( ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) /\ ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) ) -> <. ( 1st ` x ) , ( 2nd ` x ) >. = <. ( 1st ` y ) , ( 2nd ` y ) >. )
93 simplll 
 |-  ( ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) /\ ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
94 simplrl 
 |-  ( ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) /\ ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
95 92 93 94 3eqtr4d 
 |-  ( ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) /\ ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) ) -> x = y )
96 95 ex 
 |-  ( ( ( x = <. ( 1st ` x ) , ( 2nd ` x ) >. /\ ( ( 1st ` x ) e. ZZ /\ ( 2nd ` x ) e. NN ) ) /\ ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. /\ ( ( 1st ` y ) e. ZZ /\ ( 2nd ` y ) e. NN ) ) ) -> ( ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) -> x = y ) )
97 72 73 96 syl2anb 
 |-  ( ( x e. ( ZZ X. NN ) /\ y e. ( ZZ X. NN ) ) -> ( ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) -> x = y ) )
98 97 rgen2 
 |-  A. x e. ( ZZ X. NN ) A. y e. ( ZZ X. NN ) ( ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) -> x = y )
99 71 98 jctir 
 |-  ( ( z e. ZZ /\ n e. NN /\ A = ( z / n ) ) -> ( E. x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ A. x e. ( ZZ X. NN ) A. y e. ( ZZ X. NN ) ( ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) -> x = y ) ) )
100 99 3expia 
 |-  ( ( z e. ZZ /\ n e. NN ) -> ( A = ( z / n ) -> ( E. x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ A. x e. ( ZZ X. NN ) A. y e. ( ZZ X. NN ) ( ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) -> x = y ) ) ) )
101 100 rexlimivv 
 |-  ( E. z e. ZZ E. n e. NN A = ( z / n ) -> ( E. x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ A. x e. ( ZZ X. NN ) A. y e. ( ZZ X. NN ) ( ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) -> x = y ) ) )
102 elq 
 |-  ( A e. QQ <-> E. z e. ZZ E. n e. NN A = ( z / n ) )
103 fveq2 
 |-  ( x = y -> ( 1st ` x ) = ( 1st ` y ) )
104 fveq2 
 |-  ( x = y -> ( 2nd ` x ) = ( 2nd ` y ) )
105 103 104 oveq12d 
 |-  ( x = y -> ( ( 1st ` x ) gcd ( 2nd ` x ) ) = ( ( 1st ` y ) gcd ( 2nd ` y ) ) )
106 105 eqeq1d 
 |-  ( x = y -> ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 <-> ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 ) )
107 103 104 oveq12d 
 |-  ( x = y -> ( ( 1st ` x ) / ( 2nd ` x ) ) = ( ( 1st ` y ) / ( 2nd ` y ) ) )
108 107 eqeq2d 
 |-  ( x = y -> ( A = ( ( 1st ` x ) / ( 2nd ` x ) ) <-> A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) )
109 106 108 anbi12d 
 |-  ( x = y -> ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) <-> ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) )
110 109 reu4 
 |-  ( E! x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) <-> ( E. x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ A. x e. ( ZZ X. NN ) A. y e. ( ZZ X. NN ) ( ( ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) /\ ( ( ( 1st ` y ) gcd ( 2nd ` y ) ) = 1 /\ A = ( ( 1st ` y ) / ( 2nd ` y ) ) ) ) -> x = y ) ) )
111 101 102 110 3imtr4i 
 |-  ( A e. QQ -> E! x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ A = ( ( 1st ` x ) / ( 2nd ` x ) ) ) )