Metamath Proof Explorer

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→ 𝐵 )