Metamath Proof Explorer

Theorem qredeq

Description: Two equal reduced fractions have the same numerator and denominator. (Contributed by Jeff Hankins, 29-Sep-2013)

Ref Expression
Assertion qredeq 
|- ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) /\ ( M / N ) = ( P / Q ) ) -> ( M = P /\ N = Q ) )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( M e. ZZ -> M e. CC )
2 1 adantr 
 |-  ( ( M e. ZZ /\ N e. NN ) -> M e. CC )
3 nncn 
 |-  ( N e. NN -> N e. CC )
4 3 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> N e. CC )
5 nnne0 
 |-  ( N e. NN -> N =/= 0 )
6 5 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> N =/= 0 )
7 2 4 6 divcld 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M / N ) e. CC )
8 7 3adant3 
 |-  ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) -> ( M / N ) e. CC )
9 8 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( M / N ) e. CC )
10 zcn 
 |-  ( P e. ZZ -> P e. CC )
11 10 adantr 
 |-  ( ( P e. ZZ /\ Q e. NN ) -> P e. CC )
12 nncn 
 |-  ( Q e. NN -> Q e. CC )
13 12 adantl 
 |-  ( ( P e. ZZ /\ Q e. NN ) -> Q e. CC )
14 nnne0 
 |-  ( Q e. NN -> Q =/= 0 )
15 14 adantl 
 |-  ( ( P e. ZZ /\ Q e. NN ) -> Q =/= 0 )
16 11 13 15 divcld 
 |-  ( ( P e. ZZ /\ Q e. NN ) -> ( P / Q ) e. CC )
17 16 3adant3 
 |-  ( ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) -> ( P / Q ) e. CC )
18 17 adantl 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( P / Q ) e. CC )
19 3 3ad2ant2 
 |-  ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) -> N e. CC )
20 19 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> N e. CC )
21 5 3ad2ant2 
 |-  ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) -> N =/= 0 )
22 21 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> N =/= 0 )
23 9 18 20 22 mulcand 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( ( N x. ( M / N ) ) = ( N x. ( P / Q ) ) <-> ( M / N ) = ( P / Q ) ) )
24 2 4 6 divcan2d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N x. ( M / N ) ) = M )
25 24 3adant3 
 |-  ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) -> ( N x. ( M / N ) ) = M )
26 25 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( N x. ( M / N ) ) = M )
27 26 eqeq1d 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( ( N x. ( M / N ) ) = ( N x. ( P / Q ) ) <-> M = ( N x. ( P / Q ) ) ) )
28 23 27 bitr3d 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( ( M / N ) = ( P / Q ) <-> M = ( N x. ( P / Q ) ) ) )
29 1 3ad2ant1 
 |-  ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) -> M e. CC )
30 29 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> M e. CC )
31 mulcl 
 |-  ( ( N e. CC /\ ( P / Q ) e. CC ) -> ( N x. ( P / Q ) ) e. CC )
32 19 17 31 syl2an 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( N x. ( P / Q ) ) e. CC )
33 12 3ad2ant2 
 |-  ( ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) -> Q e. CC )
34 33 adantl 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> Q e. CC )
35 14 3ad2ant2 
 |-  ( ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) -> Q =/= 0 )
36 35 adantl 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> Q =/= 0 )
37 30 32 34 36 mulcan2d 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( ( M x. Q ) = ( ( N x. ( P / Q ) ) x. Q ) <-> M = ( N x. ( P / Q ) ) ) )
38 20 18 34 mulassd 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( ( N x. ( P / Q ) ) x. Q ) = ( N x. ( ( P / Q ) x. Q ) ) )
39 11 13 15 divcan1d 
 |-  ( ( P e. ZZ /\ Q e. NN ) -> ( ( P / Q ) x. Q ) = P )
40 39 3adant3 
 |-  ( ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) -> ( ( P / Q ) x. Q ) = P )
41 40 adantl 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( ( P / Q ) x. Q ) = P )
42 41 oveq2d 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( N x. ( ( P / Q ) x. Q ) ) = ( N x. P ) )
43 38 42 eqtrd 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( ( N x. ( P / Q ) ) x. Q ) = ( N x. P ) )
44 43 eqeq2d 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( ( M x. Q ) = ( ( N x. ( P / Q ) ) x. Q ) <-> ( M x. Q ) = ( N x. P ) ) )
45 37 44 bitr3d 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( M = ( N x. ( P / Q ) ) <-> ( M x. Q ) = ( N x. P ) ) )
46 28 45 bitrd 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( ( M / N ) = ( P / Q ) <-> ( M x. Q ) = ( N x. P ) ) )
47 nnz 
 |-  ( N e. NN -> N e. ZZ )
48 47 3ad2ant2 
 |-  ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) -> N e. ZZ )
49 simp2 
 |-  ( ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) -> Q e. NN )
50 48 49 anim12i 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( N e. ZZ /\ Q e. NN ) )
51 50 adantr 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( N e. ZZ /\ Q e. NN ) )
52 48 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> N e. ZZ )
53 simpl1 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> M e. ZZ )
54 nnz 
 |-  ( Q e. NN -> Q e. ZZ )
55 54 3ad2ant2 
 |-  ( ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) -> Q e. ZZ )
56 55 adantl 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> Q e. ZZ )
57 52 53 56 3jca 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( N e. ZZ /\ M e. ZZ /\ Q e. ZZ ) )
58 57 adantr 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( N e. ZZ /\ M e. ZZ /\ Q e. ZZ ) )
59 simp1 
 |-  ( ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) -> P e. ZZ )
60 dvdsmul1 
 |-  ( ( N e. ZZ /\ P e. ZZ ) -> N || ( N x. P ) )
61 48 59 60 syl2an 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> N || ( N x. P ) )
62 61 adantr 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> N || ( N x. P ) )
63 simpr 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( M x. Q ) = ( N x. P ) )
64 62 63 breqtrrd 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> N || ( M x. Q ) )
65 gcdcom 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N gcd M ) = ( M gcd N ) )
66 47 65 sylan 
 |-  ( ( N e. NN /\ M e. ZZ ) -> ( N gcd M ) = ( M gcd N ) )
67 66 ancoms 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N gcd M ) = ( M gcd N ) )
68 67 3adant3 
 |-  ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) -> ( N gcd M ) = ( M gcd N ) )
69 simp3 
 |-  ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) -> ( M gcd N ) = 1 )
70 68 69 eqtrd 
 |-  ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) -> ( N gcd M ) = 1 )
71 70 ad2antrr 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( N gcd M ) = 1 )
72 64 71 jca 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( N || ( M x. Q ) /\ ( N gcd M ) = 1 ) )
73 coprmdvds 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ Q e. ZZ ) -> ( ( N || ( M x. Q ) /\ ( N gcd M ) = 1 ) -> N || Q ) )
74 58 72 73 sylc 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> N || Q )
75 dvdsle 
 |-  ( ( N e. ZZ /\ Q e. NN ) -> ( N || Q -> N <_ Q ) )
76 51 74 75 sylc 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> N <_ Q )
77 simp2 
 |-  ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) -> N e. NN )
78 55 77 anim12i 
 |-  ( ( ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) /\ ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) ) -> ( Q e. ZZ /\ N e. NN ) )
79 78 ancoms 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( Q e. ZZ /\ N e. NN ) )
80 79 adantr 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( Q e. ZZ /\ N e. NN ) )
81 simpr1 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> P e. ZZ )
82 56 81 52 3jca 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( Q e. ZZ /\ P e. ZZ /\ N e. ZZ ) )
83 82 adantr 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( Q e. ZZ /\ P e. ZZ /\ N e. ZZ ) )
84 simp1 
 |-  ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) -> M e. ZZ )
85 dvdsmul2 
 |-  ( ( M e. ZZ /\ Q e. ZZ ) -> Q || ( M x. Q ) )
86 84 55 85 syl2an 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> Q || ( M x. Q ) )
87 86 adantr 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> Q || ( M x. Q ) )
88 10 3ad2ant1 
 |-  ( ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) -> P e. CC )
89 mulcom 
 |-  ( ( N e. CC /\ P e. CC ) -> ( N x. P ) = ( P x. N ) )
90 19 88 89 syl2an 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( N x. P ) = ( P x. N ) )
91 90 adantr 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( N x. P ) = ( P x. N ) )
92 63 91 eqtrd 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( M x. Q ) = ( P x. N ) )
93 87 92 breqtrd 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> Q || ( P x. N ) )
94 gcdcom 
 |-  ( ( Q e. ZZ /\ P e. ZZ ) -> ( Q gcd P ) = ( P gcd Q ) )
95 54 94 sylan 
 |-  ( ( Q e. NN /\ P e. ZZ ) -> ( Q gcd P ) = ( P gcd Q ) )
96 95 ancoms 
 |-  ( ( P e. ZZ /\ Q e. NN ) -> ( Q gcd P ) = ( P gcd Q ) )
97 96 3adant3 
 |-  ( ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) -> ( Q gcd P ) = ( P gcd Q ) )
98 simp3 
 |-  ( ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) -> ( P gcd Q ) = 1 )
99 97 98 eqtrd 
 |-  ( ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) -> ( Q gcd P ) = 1 )
100 99 ad2antlr 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( Q gcd P ) = 1 )
101 93 100 jca 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( Q || ( P x. N ) /\ ( Q gcd P ) = 1 ) )
102 coprmdvds 
 |-  ( ( Q e. ZZ /\ P e. ZZ /\ N e. ZZ ) -> ( ( Q || ( P x. N ) /\ ( Q gcd P ) = 1 ) -> Q || N ) )
103 83 101 102 sylc 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> Q || N )
104 dvdsle 
 |-  ( ( Q e. ZZ /\ N e. NN ) -> ( Q || N -> Q <_ N ) )
105 80 103 104 sylc 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> Q <_ N )
106 nnre 
 |-  ( N e. NN -> N e. RR )
107 106 3ad2ant2 
 |-  ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) -> N e. RR )
108 107 ad2antrr 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> N e. RR )
109 nnre 
 |-  ( Q e. NN -> Q e. RR )
110 109 3ad2ant2 
 |-  ( ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) -> Q e. RR )
111 110 ad2antlr 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> Q e. RR )
112 108 111 letri3d 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( N = Q <-> ( N <_ Q /\ Q <_ N ) ) )
113 76 105 112 mpbir2and 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> N = Q )
114 oveq2 
 |-  ( N = Q -> ( M x. N ) = ( M x. Q ) )
115 114 eqeq1d 
 |-  ( N = Q -> ( ( M x. N ) = ( N x. P ) <-> ( M x. Q ) = ( N x. P ) ) )
116 115 anbi2d 
 |-  ( N = Q -> ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. N ) = ( N x. P ) ) <-> ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) ) )
117 mulcom 
 |-  ( ( M e. CC /\ N e. CC ) -> ( M x. N ) = ( N x. M ) )
118 1 3 117 syl2an 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M x. N ) = ( N x. M ) )
119 118 3adant3 
 |-  ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) -> ( M x. N ) = ( N x. M ) )
120 119 adantr 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( M x. N ) = ( N x. M ) )
121 120 eqeq1d 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( ( M x. N ) = ( N x. P ) <-> ( N x. M ) = ( N x. P ) ) )
122 88 adantl 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> P e. CC )
123 30 122 20 22 mulcand 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( ( N x. M ) = ( N x. P ) <-> M = P ) )
124 121 123 bitrd 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( ( M x. N ) = ( N x. P ) <-> M = P ) )
125 124 biimpa 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. N ) = ( N x. P ) ) -> M = P )
126 116 125 biimtrrdi 
 |-  ( N = Q -> ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> M = P ) )
127 126 com12 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( N = Q -> M = P ) )
128 127 ancrd 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( N = Q -> ( M = P /\ N = Q ) ) )
129 113 128 mpd 
 |-  ( ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) /\ ( M x. Q ) = ( N x. P ) ) -> ( M = P /\ N = Q ) )
130 129 ex 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( ( M x. Q ) = ( N x. P ) -> ( M = P /\ N = Q ) ) )
131 46 130 sylbid 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) ) -> ( ( M / N ) = ( P / Q ) -> ( M = P /\ N = Q ) ) )
132 131 3impia 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ ( M gcd N ) = 1 ) /\ ( P e. ZZ /\ Q e. NN /\ ( P gcd Q ) = 1 ) /\ ( M / N ) = ( P / Q ) ) -> ( M = P /\ N = Q ) )