qredeq

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

		Ref	Expression
	Assertion	qredeq	$⊢ ((M \in ℤ \land N \in ℕ \land M \gcd N = 1) \land (P \in ℤ \land Q \in ℕ \land P \gcd Q = 1) \land \frac{M}{N} = \frac{P}{Q}) \to (M = P \land N = Q)$

Proof

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

Metamath Proof Explorer

Theorem qredeq

Proof