hashgcdlem

Description: A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015)

	Ref	Expression
Hypotheses	hashgcdlem.a	$⊢ A = \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\}$
	hashgcdlem.b	$⊢ B = \{z \in (0 ..^M) \| z \gcd M = N\}$
	hashgcdlem.f	$⊢ F = (x \in A ⟼ x \cdot N)$
Assertion	hashgcdlem	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to F : A \underset{1-1 onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		hashgcdlem.a	$⊢ A = \{y \in (0 ..^\frac{M}{N}) \| y \gcd (\frac{M}{N}) = 1\}$
2		hashgcdlem.b	$⊢ B = \{z \in (0 ..^M) \| z \gcd M = N\}$
3		hashgcdlem.f	$⊢ F = (x \in A ⟼ x \cdot N)$
4		oveq1	$⊢ y = x \to y \gcd (\frac{M}{N}) = x \gcd (\frac{M}{N})$
5	4	eqeq1d	$⊢ y = x \to (y \gcd (\frac{M}{N}) = 1 \leftrightarrow x \gcd (\frac{M}{N}) = 1)$
6	5 1	elrab2	$⊢ x \in A \leftrightarrow (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)$
7		elfzonn0	$⊢ x \in (0 ..^\frac{M}{N}) \to x \in ℕ_{0}$
8	7	ad2antrl	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to x \in ℕ_{0}$
9		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
10	9	3ad2ant2	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to N \in ℕ_{0}$
11	10	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to N \in ℕ_{0}$
12	8 11	nn0mulcld	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to x \cdot N \in ℕ_{0}$
13		simpl1	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to M \in ℕ$
14		elfzolt2	$⊢ x \in (0 ..^\frac{M}{N}) \to x < \frac{M}{N}$
15	14	ad2antrl	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to x < \frac{M}{N}$
16		elfzoelz	$⊢ x \in (0 ..^\frac{M}{N}) \to x \in ℤ$
17	16	ad2antrl	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to x \in ℤ$
18	17	zred	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to x \in ℝ$
19		nnre	$⊢ M \in ℕ \to M \in ℝ$
20	19	3ad2ant1	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to M \in ℝ$
21	20	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to M \in ℝ$
22		nnre	$⊢ N \in ℕ \to N \in ℝ$
23		nngt0	$⊢ N \in ℕ \to 0 < N$
24	22 23	jca	$⊢ N \in ℕ \to (N \in ℝ \land 0 < N)$
25	24	3ad2ant2	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to (N \in ℝ \land 0 < N)$
26	25	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to (N \in ℝ \land 0 < N)$
27		ltmuldiv	$⊢ (x \in ℝ \land M \in ℝ \land (N \in ℝ \land 0 < N)) \to (x \cdot N < M \leftrightarrow x < \frac{M}{N})$
28	18 21 26 27	syl3anc	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to (x \cdot N < M \leftrightarrow x < \frac{M}{N})$
29	15 28	mpbird	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to x \cdot N < M$
30		elfzo0	$⊢ x \cdot N \in (0 ..^M) \leftrightarrow (x \cdot N \in ℕ_{0} \land M \in ℕ \land x \cdot N < M)$
31	12 13 29 30	syl3anbrc	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to x \cdot N \in (0 ..^M)$
32		nncn	$⊢ M \in ℕ \to M \in ℂ$
33	32	3ad2ant1	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to M \in ℂ$
34		nncn	$⊢ N \in ℕ \to N \in ℂ$
35	34	3ad2ant2	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to N \in ℂ$
36		nnne0	$⊢ N \in ℕ \to N \neq 0$
37	36	3ad2ant2	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to N \neq 0$
38	33 35 37	divcan1d	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to (\frac{M}{N}) \cdot N = M$
39	38	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to (\frac{M}{N}) \cdot N = M$
40	39	eqcomd	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to M = (\frac{M}{N}) \cdot N$
41	40	oveq2d	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to x \cdot N \gcd M = x \cdot N \gcd (\frac{M}{N}) \cdot N$
42		nndivdvds	$⊢ (M \in ℕ \land N \in ℕ) \to (N ∥ M \leftrightarrow \frac{M}{N} \in ℕ)$
43	42	biimp3a	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to \frac{M}{N} \in ℕ$
44	43	nnzd	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to \frac{M}{N} \in ℤ$
45	44	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to \frac{M}{N} \in ℤ$
46		mulgcdr	$⊢ (x \in ℤ \land \frac{M}{N} \in ℤ \land N \in ℕ_{0}) \to x \cdot N \gcd (\frac{M}{N}) \cdot N = (x \gcd (\frac{M}{N})) \cdot N$
47	17 45 11 46	syl3anc	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to x \cdot N \gcd (\frac{M}{N}) \cdot N = (x \gcd (\frac{M}{N})) \cdot N$
48		simprr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to x \gcd (\frac{M}{N}) = 1$
49	48	oveq1d	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to (x \gcd (\frac{M}{N})) \cdot N = 1 \cdot N$
50	35	mulid2d	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to 1 \cdot N = N$
51	50	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to 1 \cdot N = N$
52	49 51	eqtrd	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to (x \gcd (\frac{M}{N})) \cdot N = N$
53	41 47 52	3eqtrd	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to x \cdot N \gcd M = N$
54		oveq1	$⊢ z = x \cdot N \to z \gcd M = x \cdot N \gcd M$
55	54	eqeq1d	$⊢ z = x \cdot N \to (z \gcd M = N \leftrightarrow x \cdot N \gcd M = N)$
56	55 2	elrab2	$⊢ x \cdot N \in B \leftrightarrow (x \cdot N \in (0 ..^M) \land x \cdot N \gcd M = N)$
57	31 53 56	sylanbrc	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land x \gcd (\frac{M}{N}) = 1)) \to x \cdot N \in B$
58	6 57	sylan2b	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land x \in A) \to x \cdot N \in B$
59		oveq1	$⊢ z = w \to z \gcd M = w \gcd M$
60	59	eqeq1d	$⊢ z = w \to (z \gcd M = N \leftrightarrow w \gcd M = N)$
61	60 2	elrab2	$⊢ w \in B \leftrightarrow (w \in (0 ..^M) \land w \gcd M = N)$
62		simprr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to w \gcd M = N$
63		elfzoelz	$⊢ w \in (0 ..^M) \to w \in ℤ$
64	63	ad2antrl	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to w \in ℤ$
65		simpl1	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to M \in ℕ$
66	65	nnzd	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to M \in ℤ$
67		gcddvds	$⊢ (w \in ℤ \land M \in ℤ) \to ((w \gcd M) ∥ w \land (w \gcd M) ∥ M)$
68	64 66 67	syl2anc	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to ((w \gcd M) ∥ w \land (w \gcd M) ∥ M)$
69	68	simpld	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to (w \gcd M) ∥ w$
70	62 69	eqbrtrrd	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to N ∥ w$
71		nnz	$⊢ N \in ℕ \to N \in ℤ$
72	71	3ad2ant2	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to N \in ℤ$
73	72	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to N \in ℤ$
74	37	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to N \neq 0$
75		dvdsval2	$⊢ (N \in ℤ \land N \neq 0 \land w \in ℤ) \to (N ∥ w \leftrightarrow \frac{w}{N} \in ℤ)$
76	73 74 64 75	syl3anc	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to (N ∥ w \leftrightarrow \frac{w}{N} \in ℤ)$
77	70 76	mpbid	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to \frac{w}{N} \in ℤ$
78		elfzofz	$⊢ w \in (0 ..^M) \to w \in (0 \dots M)$
79	78	ad2antrl	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to w \in (0 \dots M)$
80		elfznn0	$⊢ w \in (0 \dots M) \to w \in ℕ_{0}$
81		nn0re	$⊢ w \in ℕ_{0} \to w \in ℝ$
82		nn0ge0	$⊢ w \in ℕ_{0} \to 0 \leq w$
83	81 82	jca	$⊢ w \in ℕ_{0} \to (w \in ℝ \land 0 \leq w)$
84	79 80 83	3syl	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to (w \in ℝ \land 0 \leq w)$
85	25	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to (N \in ℝ \land 0 < N)$
86		divge0	$⊢ ((w \in ℝ \land 0 \leq w) \land (N \in ℝ \land 0 < N)) \to 0 \leq \frac{w}{N}$
87	84 85 86	syl2anc	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to 0 \leq \frac{w}{N}$
88		elnn0z	$⊢ \frac{w}{N} \in ℕ_{0} \leftrightarrow (\frac{w}{N} \in ℤ \land 0 \leq \frac{w}{N})$
89	77 87 88	sylanbrc	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to \frac{w}{N} \in ℕ_{0}$
90	43	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to \frac{M}{N} \in ℕ$
91		elfzolt2	$⊢ w \in (0 ..^M) \to w < M$
92	91	ad2antrl	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to w < M$
93	64	zred	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to w \in ℝ$
94	20	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to M \in ℝ$
95		ltdiv1	$⊢ (w \in ℝ \land M \in ℝ \land (N \in ℝ \land 0 < N)) \to (w < M \leftrightarrow \frac{w}{N} < \frac{M}{N})$
96	93 94 85 95	syl3anc	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to (w < M \leftrightarrow \frac{w}{N} < \frac{M}{N})$
97	92 96	mpbid	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to \frac{w}{N} < \frac{M}{N}$
98		elfzo0	$⊢ \frac{w}{N} \in (0 ..^\frac{M}{N}) \leftrightarrow (\frac{w}{N} \in ℕ_{0} \land \frac{M}{N} \in ℕ \land \frac{w}{N} < \frac{M}{N})$
99	89 90 97 98	syl3anbrc	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to \frac{w}{N} \in (0 ..^\frac{M}{N})$
100	62	oveq1d	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to \frac{w \gcd M}{N} = \frac{N}{N}$
101		simpl2	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to N \in ℕ$
102		simpl3	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to N ∥ M$
103		gcddiv	$⊢ ((w \in ℤ \land M \in ℤ \land N \in ℕ) \land (N ∥ w \land N ∥ M)) \to \frac{w \gcd M}{N} = (\frac{w}{N}) \gcd (\frac{M}{N})$
104	64 66 101 70 102 103	syl32anc	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to \frac{w \gcd M}{N} = (\frac{w}{N}) \gcd (\frac{M}{N})$
105	35 37	dividd	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to \frac{N}{N} = 1$
106	105	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to \frac{N}{N} = 1$
107	100 104 106	3eqtr3d	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to (\frac{w}{N}) \gcd (\frac{M}{N}) = 1$
108		oveq1	$⊢ y = \frac{w}{N} \to y \gcd (\frac{M}{N}) = (\frac{w}{N}) \gcd (\frac{M}{N})$
109	108	eqeq1d	$⊢ y = \frac{w}{N} \to (y \gcd (\frac{M}{N}) = 1 \leftrightarrow (\frac{w}{N}) \gcd (\frac{M}{N}) = 1)$
110	109 1	elrab2	$⊢ \frac{w}{N} \in A \leftrightarrow (\frac{w}{N} \in (0 ..^\frac{M}{N}) \land (\frac{w}{N}) \gcd (\frac{M}{N}) = 1)$
111	99 107 110	sylanbrc	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (w \in (0 ..^M) \land w \gcd M = N)) \to \frac{w}{N} \in A$
112	61 111	sylan2b	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land w \in B) \to \frac{w}{N} \in A$
113	6	simplbi	$⊢ x \in A \to x \in (0 ..^\frac{M}{N})$
114	61	simplbi	$⊢ w \in B \to w \in (0 ..^M)$
115	113 114	anim12i	$⊢ (x \in A \land w \in B) \to (x \in (0 ..^\frac{M}{N}) \land w \in (0 ..^M))$
116	63	ad2antll	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land w \in (0 ..^M))) \to w \in ℤ$
117	116	zcnd	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land w \in (0 ..^M))) \to w \in ℂ$
118	35	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land w \in (0 ..^M))) \to N \in ℂ$
119	37	adantr	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land w \in (0 ..^M))) \to N \neq 0$
120	117 118 119	divcan1d	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land w \in (0 ..^M))) \to (\frac{w}{N}) \cdot N = w$
121	120	eqcomd	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land w \in (0 ..^M))) \to w = (\frac{w}{N}) \cdot N$
122		oveq1	$⊢ x = \frac{w}{N} \to x \cdot N = (\frac{w}{N}) \cdot N$
123	122	eqeq2d	$⊢ x = \frac{w}{N} \to (w = x \cdot N \leftrightarrow w = (\frac{w}{N}) \cdot N)$
124	121 123	syl5ibrcom	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land w \in (0 ..^M))) \to (x = \frac{w}{N} \to w = x \cdot N)$
125	16	ad2antrl	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land w \in (0 ..^M))) \to x \in ℤ$
126	125	zcnd	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land w \in (0 ..^M))) \to x \in ℂ$
127	126 118 119	divcan4d	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land w \in (0 ..^M))) \to \frac{x \cdot N}{N} = x$
128	127	eqcomd	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land w \in (0 ..^M))) \to x = \frac{x \cdot N}{N}$
129		oveq1	$⊢ w = x \cdot N \to \frac{w}{N} = \frac{x \cdot N}{N}$
130	129	eqeq2d	$⊢ w = x \cdot N \to (x = \frac{w}{N} \leftrightarrow x = \frac{x \cdot N}{N})$
131	128 130	syl5ibrcom	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land w \in (0 ..^M))) \to (w = x \cdot N \to x = \frac{w}{N})$
132	124 131	impbid	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in (0 ..^\frac{M}{N}) \land w \in (0 ..^M))) \to (x = \frac{w}{N} \leftrightarrow w = x \cdot N)$
133	115 132	sylan2	$⊢ ((M \in ℕ \land N \in ℕ \land N ∥ M) \land (x \in A \land w \in B)) \to (x = \frac{w}{N} \leftrightarrow w = x \cdot N)$
134	3 58 112 133	f1o2d	$⊢ (M \in ℕ \land N \in ℕ \land N ∥ M) \to F : A \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem hashgcdlem

Proof