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 ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ∧ ( 𝑃 ∈ ℤ ∧ 𝑄 ∈ ℕ ∧ ( 𝑃 gcd 𝑄 ) = 1 ) ∧ ( 𝑀 / 𝑁 ) = ( 𝑃 / 𝑄 ) ) → ( 𝑀 = 𝑃 ∧ 𝑁 = 𝑄 ) )

Proof

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