# 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 ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℕ\wedge {M}\mathrm{gcd}{N}=1\right)\wedge \left({P}\in ℤ\wedge {Q}\in ℕ\wedge {P}\mathrm{gcd}{Q}=1\right)\wedge \frac{{M}}{{N}}=\frac{{P}}{{Q}}\right)\to \left({M}={P}\wedge {N}={Q}\right)$

### Proof

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