ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  qredeq Unicode version

Theorem qredeq 12096
Description: Two equal reduced fractions have the same numerator and denominator. (Contributed by Jeff Hankins, 29-Sep-2013.)
Assertion
Ref Expression
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 of Theorem qredeq
StepHypRef Expression
1 zcn 9258 . . . . . . . . . 10  |-  ( M  e.  ZZ  ->  M  e.  CC )
21adantr 276 . . . . . . . . 9  |-  ( ( M  e.  ZZ  /\  N  e.  NN )  ->  M  e.  CC )
3 nncn 8927 . . . . . . . . . 10  |-  ( N  e.  NN  ->  N  e.  CC )
43adantl 277 . . . . . . . . 9  |-  ( ( M  e.  ZZ  /\  N  e.  NN )  ->  N  e.  CC )
5 nnap0 8948 . . . . . . . . . 10  |-  ( N  e.  NN  ->  N #  0 )
65adantl 277 . . . . . . . . 9  |-  ( ( M  e.  ZZ  /\  N  e.  NN )  ->  N #  0 )
72, 4, 6divclapd 8747 . . . . . . . 8  |-  ( ( M  e.  ZZ  /\  N  e.  NN )  ->  ( M  /  N
)  e.  CC )
873adant3 1017 . . . . . . 7  |-  ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  ( M  /  N )  e.  CC )
98adantr 276 . . . . . 6  |-  ( ( ( 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 9258 . . . . . . . . . 10  |-  ( P  e.  ZZ  ->  P  e.  CC )
1110adantr 276 . . . . . . . . 9  |-  ( ( P  e.  ZZ  /\  Q  e.  NN )  ->  P  e.  CC )
12 nncn 8927 . . . . . . . . . 10  |-  ( Q  e.  NN  ->  Q  e.  CC )
1312adantl 277 . . . . . . . . 9  |-  ( ( P  e.  ZZ  /\  Q  e.  NN )  ->  Q  e.  CC )
14 nnap0 8948 . . . . . . . . . 10  |-  ( Q  e.  NN  ->  Q #  0 )
1514adantl 277 . . . . . . . . 9  |-  ( ( P  e.  ZZ  /\  Q  e.  NN )  ->  Q #  0 )
1611, 13, 15divclapd 8747 . . . . . . . 8  |-  ( ( P  e.  ZZ  /\  Q  e.  NN )  ->  ( P  /  Q
)  e.  CC )
17163adant3 1017 . . . . . . 7  |-  ( ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 )  ->  ( P  /  Q )  e.  CC )
1817adantl 277 . . . . . 6  |-  ( ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  /\  ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 ) )  ->  ( P  /  Q )  e.  CC )
1933ad2ant2 1019 . . . . . . 7  |-  ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  N  e.  CC )
2019adantr 276 . . . . . 6  |-  ( ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  /\  ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 ) )  ->  N  e.  CC )
2153ad2ant2 1019 . . . . . . 7  |-  ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  N #  0 )
2221adantr 276 . . . . . 6  |-  ( ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  /\  ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 ) )  ->  N #  0 )
239, 18, 20, 22mulcanapd 8618 . . . . 5  |-  ( ( ( 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 ) ) )
242, 4, 6divcanap2d 8749 . . . . . . . 8  |-  ( ( M  e.  ZZ  /\  N  e.  NN )  ->  ( N  x.  ( M  /  N ) )  =  M )
25243adant3 1017 . . . . . . 7  |-  ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  ( N  x.  ( M  /  N ) )  =  M )
2625adantr 276 . . . . . 6  |-  ( ( ( 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 )
2726eqeq1d 2186 . . . . 5  |-  ( ( ( 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 ) ) ) )
2823, 27bitr3d 190 . . . 4  |-  ( ( ( 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 ) ) ) )
2913ad2ant1 1018 . . . . . . 7  |-  ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  M  e.  CC )
3029adantr 276 . . . . . 6  |-  ( ( ( 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 7938 . . . . . . 7  |-  ( ( N  e.  CC  /\  ( P  /  Q
)  e.  CC )  ->  ( N  x.  ( P  /  Q
) )  e.  CC )
3219, 17, 31syl2an 289 . . . . . 6  |-  ( ( ( 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 )
33123ad2ant2 1019 . . . . . . 7  |-  ( ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 )  ->  Q  e.  CC )
3433adantl 277 . . . . . 6  |-  ( ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  /\  ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 ) )  ->  Q  e.  CC )
35143ad2ant2 1019 . . . . . . 7  |-  ( ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 )  ->  Q #  0 )
3635adantl 277 . . . . . 6  |-  ( ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  /\  ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 ) )  ->  Q #  0 )
3730, 32, 34, 36mulcanap2d 8619 . . . . 5  |-  ( ( ( 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 ) ) ) )
3820, 18, 34mulassd 7981 . . . . . . 7  |-  ( ( ( 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 ) ) )
3911, 13, 15divcanap1d 8748 . . . . . . . . . 10  |-  ( ( P  e.  ZZ  /\  Q  e.  NN )  ->  ( ( P  /  Q )  x.  Q
)  =  P )
40393adant3 1017 . . . . . . . . 9  |-  ( ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 )  ->  (
( P  /  Q
)  x.  Q )  =  P )
4140adantl 277 . . . . . . . 8  |-  ( ( ( 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 )
4241oveq2d 5891 . . . . . . 7  |-  ( ( ( 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 ) )
4338, 42eqtrd 2210 . . . . . 6  |-  ( ( ( 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 ) )
4443eqeq2d 2189 . . . . 5  |-  ( ( ( 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 ) ) )
4537, 44bitr3d 190 . . . 4  |-  ( ( ( 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 ) ) )
4628, 45bitrd 188 . . 3  |-  ( ( ( 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 9272 . . . . . . . . . 10  |-  ( N  e.  NN  ->  N  e.  ZZ )
48473ad2ant2 1019 . . . . . . . . 9  |-  ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  N  e.  ZZ )
49 simp2 998 . . . . . . . . 9  |-  ( ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 )  ->  Q  e.  NN )
5048, 49anim12i 338 . . . . . . . 8  |-  ( ( ( 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 ) )
5150adantr 276 . . . . . . 7  |-  ( ( ( ( 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 ) )
5248adantr 276 . . . . . . . . . 10  |-  ( ( ( 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 1000 . . . . . . . . . 10  |-  ( ( ( 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 9272 . . . . . . . . . . . 12  |-  ( Q  e.  NN  ->  Q  e.  ZZ )
55543ad2ant2 1019 . . . . . . . . . . 11  |-  ( ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 )  ->  Q  e.  ZZ )
5655adantl 277 . . . . . . . . . 10  |-  ( ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  /\  ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 ) )  ->  Q  e.  ZZ )
5752, 53, 563jca 1177 . . . . . . . . 9  |-  ( ( ( 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 ) )
5857adantr 276 . . . . . . . 8  |-  ( ( ( ( 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 997 . . . . . . . . . . . 12  |-  ( ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 )  ->  P  e.  ZZ )
60 dvdsmul1 11820 . . . . . . . . . . . 12  |-  ( ( N  e.  ZZ  /\  P  e.  ZZ )  ->  N  ||  ( N  x.  P ) )
6148, 59, 60syl2an 289 . . . . . . . . . . 11  |-  ( ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  /\  ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 ) )  ->  N  ||  ( N  x.  P )
)
6261adantr 276 . . . . . . . . . 10  |-  ( ( ( ( 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 110 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
6462, 63breqtrrd 4032 . . . . . . . . 9  |-  ( ( ( ( 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 11974 . . . . . . . . . . . . . 14  |-  ( ( N  e.  ZZ  /\  M  e.  ZZ )  ->  ( N  gcd  M
)  =  ( M  gcd  N ) )
6647, 65sylan 283 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN  /\  M  e.  ZZ )  ->  ( N  gcd  M
)  =  ( M  gcd  N ) )
6766ancoms 268 . . . . . . . . . . . 12  |-  ( ( M  e.  ZZ  /\  N  e.  NN )  ->  ( N  gcd  M
)  =  ( M  gcd  N ) )
68673adant3 1017 . . . . . . . . . . 11  |-  ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  ( N  gcd  M )  =  ( M  gcd  N
) )
69 simp3 999 . . . . . . . . . . 11  |-  ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  ( M  gcd  N )  =  1 )
7068, 69eqtrd 2210 . . . . . . . . . 10  |-  ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  ( N  gcd  M )  =  1 )
7170ad2antrr 488 . . . . . . . . 9  |-  ( ( ( ( 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 )
7264, 71jca 306 . . . . . . . 8  |-  ( ( ( ( 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 12092 . . . . . . . 8  |-  ( ( N  e.  ZZ  /\  M  e.  ZZ  /\  Q  e.  ZZ )  ->  (
( N  ||  ( M  x.  Q )  /\  ( N  gcd  M
)  =  1 )  ->  N  ||  Q
) )
7458, 72, 73sylc 62 . . . . . . 7  |-  ( ( ( ( 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 11850 . . . . . . 7  |-  ( ( N  e.  ZZ  /\  Q  e.  NN )  ->  ( N  ||  Q  ->  N  <_  Q )
)
7651, 74, 75sylc 62 . . . . . 6  |-  ( ( ( ( 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 998 . . . . . . . . . 10  |-  ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  N  e.  NN )
7855, 77anim12i 338 . . . . . . . . 9  |-  ( ( ( 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 ) )
7978ancoms 268 . . . . . . . 8  |-  ( ( ( 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 ) )
8079adantr 276 . . . . . . 7  |-  ( ( ( ( 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 1003 . . . . . . . . . 10  |-  ( ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  /\  ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 ) )  ->  P  e.  ZZ )
8256, 81, 523jca 1177 . . . . . . . . 9  |-  ( ( ( 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 ) )
8382adantr 276 . . . . . . . 8  |-  ( ( ( ( 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 997 . . . . . . . . . . . 12  |-  ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  M  e.  ZZ )
85 dvdsmul2 11821 . . . . . . . . . . . 12  |-  ( ( M  e.  ZZ  /\  Q  e.  ZZ )  ->  Q  ||  ( M  x.  Q ) )
8684, 55, 85syl2an 289 . . . . . . . . . . 11  |-  ( ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  /\  ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 ) )  ->  Q  ||  ( M  x.  Q )
)
8786adantr 276 . . . . . . . . . 10  |-  ( ( ( ( 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 )
)
88103ad2ant1 1018 . . . . . . . . . . . . 13  |-  ( ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 )  ->  P  e.  CC )
89 mulcom 7940 . . . . . . . . . . . . 13  |-  ( ( N  e.  CC  /\  P  e.  CC )  ->  ( N  x.  P
)  =  ( P  x.  N ) )
9019, 88, 89syl2an 289 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
9190adantr 276 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
9263, 91eqtrd 2210 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
9387, 92breqtrd 4030 . . . . . . . . 9  |-  ( ( ( ( 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 11974 . . . . . . . . . . . . . 14  |-  ( ( Q  e.  ZZ  /\  P  e.  ZZ )  ->  ( Q  gcd  P
)  =  ( P  gcd  Q ) )
9554, 94sylan 283 . . . . . . . . . . . . 13  |-  ( ( Q  e.  NN  /\  P  e.  ZZ )  ->  ( Q  gcd  P
)  =  ( P  gcd  Q ) )
9695ancoms 268 . . . . . . . . . . . 12  |-  ( ( P  e.  ZZ  /\  Q  e.  NN )  ->  ( Q  gcd  P
)  =  ( P  gcd  Q ) )
97963adant3 1017 . . . . . . . . . . 11  |-  ( ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 )  ->  ( Q  gcd  P )  =  ( P  gcd  Q
) )
98 simp3 999 . . . . . . . . . . 11  |-  ( ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 )  ->  ( P  gcd  Q )  =  1 )
9997, 98eqtrd 2210 . . . . . . . . . 10  |-  ( ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 )  ->  ( Q  gcd  P )  =  1 )
10099ad2antlr 489 . . . . . . . . 9  |-  ( ( ( ( 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 )
10193, 100jca 306 . . . . . . . 8  |-  ( ( ( ( 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 12092 . . . . . . . 8  |-  ( ( Q  e.  ZZ  /\  P  e.  ZZ  /\  N  e.  ZZ )  ->  (
( Q  ||  ( P  x.  N )  /\  ( Q  gcd  P
)  =  1 )  ->  Q  ||  N
) )
10383, 101, 102sylc 62 . . . . . . 7  |-  ( ( ( ( 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 11850 . . . . . . 7  |-  ( ( Q  e.  ZZ  /\  N  e.  NN )  ->  ( Q  ||  N  ->  Q  <_  N )
)
10580, 103, 104sylc 62 . . . . . 6  |-  ( ( ( ( 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 8926 . . . . . . . . 9  |-  ( N  e.  NN  ->  N  e.  RR )
1071063ad2ant2 1019 . . . . . . . 8  |-  ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  N  e.  RR )
108107ad2antrr 488 . . . . . . 7  |-  ( ( ( ( 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 8926 . . . . . . . . 9  |-  ( Q  e.  NN  ->  Q  e.  RR )
1101093ad2ant2 1019 . . . . . . . 8  |-  ( ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 )  ->  Q  e.  RR )
111110ad2antlr 489 . . . . . . 7  |-  ( ( ( ( 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 )
112108, 111letri3d 8073 . . . . . 6  |-  ( ( ( ( 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
) ) )
11376, 105, 112mpbir2and 944 . . . . 5  |-  ( ( ( ( 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 5883 . . . . . . . . . 10  |-  ( N  =  Q  ->  ( M  x.  N )  =  ( M  x.  Q ) )
115114eqeq1d 2186 . . . . . . . . 9  |-  ( N  =  Q  ->  (
( M  x.  N
)  =  ( N  x.  P )  <->  ( M  x.  Q )  =  ( N  x.  P ) ) )
116115anbi2d 464 . . . . . . . 8  |-  ( 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 7940 . . . . . . . . . . . . . 14  |-  ( ( M  e.  CC  /\  N  e.  CC )  ->  ( M  x.  N
)  =  ( N  x.  M ) )
1181, 3, 117syl2an 289 . . . . . . . . . . . . 13  |-  ( ( M  e.  ZZ  /\  N  e.  NN )  ->  ( M  x.  N
)  =  ( N  x.  M ) )
1191183adant3 1017 . . . . . . . . . . . 12  |-  ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  ( M  x.  N )  =  ( N  x.  M ) )
120119adantr 276 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
121120eqeq1d 2186 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
12288adantl 277 . . . . . . . . . . 11  |-  ( ( ( M  e.  ZZ  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  /\  ( P  e.  ZZ  /\  Q  e.  NN  /\  ( P  gcd  Q )  =  1 ) )  ->  P  e.  CC )
12330, 122, 20, 22mulcanapd 8618 . . . . . . . . . 10  |-  ( ( ( 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
) )
124121, 123bitrd 188 . . . . . . . . 9  |-  ( ( ( 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
) )
125124biimpa 296 . . . . . . . 8  |-  ( ( ( ( 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 )
126116, 125syl6bir 164 . . . . . . 7  |-  ( 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 ) )
127126com12 30 . . . . . 6  |-  ( ( ( ( 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 ) )
128127ancrd 326 . . . . 5  |-  ( ( ( ( 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 ) ) )
129113, 128mpd 13 . . . 4  |-  ( ( ( ( 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 ) )
130129ex 115 . . 3  |-  ( ( ( 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 ) ) )
13146, 130sylbid 150 . 2  |-  ( ( ( 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 ) ) )
1321313impia 1200 1  |-  ( ( ( 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 ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 978    = wceq 1353    e. wcel 2148   class class class wbr 4004  (class class class)co 5875   CCcc 7809   RRcr 7810   0cc0 7811   1c1 7812    x. cmul 7816    <_ cle 7993   # cap 8538    / cdiv 8629   NNcn 8919   ZZcz 9253    || cdvds 11794    gcd cgcd 11943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4119  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588  ax-cnex 7902  ax-resscn 7903  ax-1cn 7904  ax-1re 7905  ax-icn 7906  ax-addcl 7907  ax-addrcl 7908  ax-mulcl 7909  ax-mulrcl 7910  ax-addcom 7911  ax-mulcom 7912  ax-addass 7913  ax-mulass 7914  ax-distr 7915  ax-i2m1 7916  ax-0lt1 7917  ax-1rid 7918  ax-0id 7919  ax-rnegex 7920  ax-precex 7921  ax-cnre 7922  ax-pre-ltirr 7923  ax-pre-ltwlin 7924  ax-pre-lttrn 7925  ax-pre-apti 7926  ax-pre-ltadd 7927  ax-pre-mulgt0 7928  ax-pre-mulext 7929  ax-arch 7930  ax-caucvg 7931
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-if 3536  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-tr 4103  df-id 4294  df-po 4297  df-iso 4298  df-iord 4367  df-on 4369  df-ilim 4370  df-suc 4372  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-riota 5831  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1st 6141  df-2nd 6142  df-recs 6306  df-frec 6392  df-sup 6983  df-pnf 7994  df-mnf 7995  df-xr 7996  df-ltxr 7997  df-le 7998  df-sub 8130  df-neg 8131  df-reap 8532  df-ap 8539  df-div 8630  df-inn 8920  df-2 8978  df-3 8979  df-4 8980  df-n0 9177  df-z 9254  df-uz 9529  df-q 9620  df-rp 9654  df-fz 10009  df-fzo 10143  df-fl 10270  df-mod 10323  df-seqfrec 10446  df-exp 10520  df-cj 10851  df-re 10852  df-im 10853  df-rsqrt 11007  df-abs 11008  df-dvds 11795  df-gcd 11944
This theorem is referenced by:  qredeu  12097
  Copyright terms: Public domain W3C validator