Theorem 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	⊢ 𝐴 = { 𝑦 ∈ ( 0 ..^ ( 𝑀 / 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 / 𝑁 ) ) = 1 }
	hashgcdlem.b	⊢ 𝐵 = { 𝑧 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑧 gcd 𝑀 ) = 𝑁 }
	hashgcdlem.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 · 𝑁 ) )
Assertion	hashgcdlem	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )

Proof

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