Metamath Proof Explorer

Theorem phimullem

Description: Lemma for phimul . (Contributed by Mario Carneiro, 24-Feb-2014)

Ref Expression
Hypotheses crth.1 ⊢ 𝑆 = ( 0 ..^ ( 𝑀 · 𝑁 ) )
crth.2 ⊢ 𝑇 = ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) )
crth.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ ⟨ ( 𝑥 mod 𝑀 ) , ( 𝑥 mod 𝑁 ) ⟩ )
crth.4 ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) )
phimul.4 ⊢ 𝑈 = { 𝑦 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑦 gcd 𝑀 ) = 1 }
phimul.5 ⊢ 𝑉 = { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 }
phimul.6 ⊢ 𝑊 = { 𝑦 ∈ 𝑆 ∣ ( 𝑦 gcd ( 𝑀 · 𝑁 ) ) = 1 }
Assertion phimullem ( 𝜑 → ( ϕ ‘ ( 𝑀 · 𝑁 ) ) = ( ( ϕ ‘ 𝑀 ) · ( ϕ ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 crth.1 ⊢ 𝑆 = ( 0 ..^ ( 𝑀 · 𝑁 ) )
2 crth.2 ⊢ 𝑇 = ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) )
3 crth.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ ⟨ ( 𝑥 mod 𝑀 ) , ( 𝑥 mod 𝑁 ) ⟩ )
4 crth.4 ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑀 gcd 𝑁 ) = 1 ) )
5 phimul.4 ⊢ 𝑈 = { 𝑦 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑦 gcd 𝑀 ) = 1 }
6 phimul.5 ⊢ 𝑉 = { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 }
7 phimul.6 ⊢ 𝑊 = { 𝑦 ∈ 𝑆 ∣ ( 𝑦 gcd ( 𝑀 · 𝑁 ) ) = 1 }
8 fzofi ⊢ ( 0 ..^ 𝑀 ) ∈ Fin
9 ssrab2 ⊢ { 𝑦 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑦 gcd 𝑀 ) = 1 } ⊆ ( 0 ..^ 𝑀 )
10 ssfi ⊢ ( ( ( 0 ..^ 𝑀 ) ∈ Fin ∧ { 𝑦 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑦 gcd 𝑀 ) = 1 } ⊆ ( 0 ..^ 𝑀 ) ) → { 𝑦 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑦 gcd 𝑀 ) = 1 } ∈ Fin )
11 8 9 10 mp2an ⊢ { 𝑦 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑦 gcd 𝑀 ) = 1 } ∈ Fin
12 5 11 eqeltri ⊢ 𝑈 ∈ Fin
13 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
14 ssrab2 ⊢ { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 } ⊆ ( 0 ..^ 𝑁 )
15 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 } ⊆ ( 0 ..^ 𝑁 ) ) → { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 } ∈ Fin )
16 13 14 15 mp2an ⊢ { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 } ∈ Fin
17 6 16 eqeltri ⊢ 𝑉 ∈ Fin
18 hashxp ⊢ ( ( 𝑈 ∈ Fin ∧ 𝑉 ∈ Fin ) → ( ♯ ‘ ( 𝑈 × 𝑉 ) ) = ( ( ♯ ‘ 𝑈 ) · ( ♯ ‘ 𝑉 ) ) )
19 12 17 18 mp2an ⊢ ( ♯ ‘ ( 𝑈 × 𝑉 ) ) = ( ( ♯ ‘ 𝑈 ) · ( ♯ ‘ 𝑉 ) )
20 oveq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 gcd ( 𝑀 · 𝑁 ) ) = ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) )
21 20 eqeq1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 gcd ( 𝑀 · 𝑁 ) ) = 1 ↔ ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = 1 ) )
22 21 7 elrab2 ⊢ ( 𝑤 ∈ 𝑊 ↔ ( 𝑤 ∈ 𝑆 ∧ ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = 1 ) )
23 22 simplbi ⊢ ( 𝑤 ∈ 𝑊 → 𝑤 ∈ 𝑆 )
24 oveq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 mod 𝑀 ) = ( 𝑤 mod 𝑀 ) )
25 oveq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 mod 𝑁 ) = ( 𝑤 mod 𝑁 ) )
26 24 25 opeq12d ⊢ ( 𝑥 = 𝑤 → ⟨ ( 𝑥 mod 𝑀 ) , ( 𝑥 mod 𝑁 ) ⟩ = ⟨ ( 𝑤 mod 𝑀 ) , ( 𝑤 mod 𝑁 ) ⟩ )
27 opex ⊢ ⟨ ( 𝑤 mod 𝑀 ) , ( 𝑤 mod 𝑁 ) ⟩ ∈ V
28 26 3 27 fvmpt ⊢ ( 𝑤 ∈ 𝑆 → ( 𝐹 ‘ 𝑤 ) = ⟨ ( 𝑤 mod 𝑀 ) , ( 𝑤 mod 𝑁 ) ⟩ )
29 23 28 syl ⊢ ( 𝑤 ∈ 𝑊 → ( 𝐹 ‘ 𝑤 ) = ⟨ ( 𝑤 mod 𝑀 ) , ( 𝑤 mod 𝑁 ) ⟩ )
30 29 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑤 ) = ⟨ ( 𝑤 mod 𝑀 ) , ( 𝑤 mod 𝑁 ) ⟩ )
31 23 1 eleqtrdi ⊢ ( 𝑤 ∈ 𝑊 → 𝑤 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) )
32 31 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → 𝑤 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) )
33 elfzoelz ⊢ ( 𝑤 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) → 𝑤 ∈ ℤ )
34 32 33 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → 𝑤 ∈ ℤ )
35 4 simp1d ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → 𝑀 ∈ ℕ )
37 zmodfzo ⊢ ( ( 𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝑤 mod 𝑀 ) ∈ ( 0 ..^ 𝑀 ) )
38 34 36 37 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 mod 𝑀 ) ∈ ( 0 ..^ 𝑀 ) )
39 modgcd ⊢ ( ( 𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( ( 𝑤 mod 𝑀 ) gcd 𝑀 ) = ( 𝑤 gcd 𝑀 ) )
40 34 36 39 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( ( 𝑤 mod 𝑀 ) gcd 𝑀 ) = ( 𝑤 gcd 𝑀 ) )
41 36 nnzd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → 𝑀 ∈ ℤ )
42 gcddvds ⊢ ( ( 𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑤 gcd 𝑀 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑀 ) ∥ 𝑀 ) )
43 34 41 42 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( ( 𝑤 gcd 𝑀 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑀 ) ∥ 𝑀 ) )
44 43 simpld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑀 ) ∥ 𝑤 )
45 nnne0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ≠ 0 )
46 simpr ⊢ ( ( 𝑤 = 0 ∧ 𝑀 = 0 ) → 𝑀 = 0 )
47 46 necon3ai ⊢ ( 𝑀 ≠ 0 → ¬ ( 𝑤 = 0 ∧ 𝑀 = 0 ) )
48 36 45 47 3syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ¬ ( 𝑤 = 0 ∧ 𝑀 = 0 ) )
49 gcdn0cl ⊢ ( ( ( 𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ¬ ( 𝑤 = 0 ∧ 𝑀 = 0 ) ) → ( 𝑤 gcd 𝑀 ) ∈ ℕ )
50 34 41 48 49 syl21anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑀 ) ∈ ℕ )
51 50 nnzd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑀 ) ∈ ℤ )
52 4 simp2d ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → 𝑁 ∈ ℕ )
54 53 nnzd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → 𝑁 ∈ ℤ )
55 43 simprd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑀 ) ∥ 𝑀 )
56 51 41 54 55 dvdsmultr1d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑀 ) ∥ ( 𝑀 · 𝑁 ) )
57 36 53 nnmulcld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑀 · 𝑁 ) ∈ ℕ )
58 57 nnzd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
59 nnne0 ⊢ ( ( 𝑀 · 𝑁 ) ∈ ℕ → ( 𝑀 · 𝑁 ) ≠ 0 )
60 simpr ⊢ ( ( 𝑤 = 0 ∧ ( 𝑀 · 𝑁 ) = 0 ) → ( 𝑀 · 𝑁 ) = 0 )
61 60 necon3ai ⊢ ( ( 𝑀 · 𝑁 ) ≠ 0 → ¬ ( 𝑤 = 0 ∧ ( 𝑀 · 𝑁 ) = 0 ) )
62 57 59 61 3syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ¬ ( 𝑤 = 0 ∧ ( 𝑀 · 𝑁 ) = 0 ) )
63 dvdslegcd ⊢ ( ( ( ( 𝑤 gcd 𝑀 ) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) ∧ ¬ ( 𝑤 = 0 ∧ ( 𝑀 · 𝑁 ) = 0 ) ) → ( ( ( 𝑤 gcd 𝑀 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑀 ) ∥ ( 𝑀 · 𝑁 ) ) → ( 𝑤 gcd 𝑀 ) ≤ ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) ) )
64 51 34 58 62 63 syl31anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( ( ( 𝑤 gcd 𝑀 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑀 ) ∥ ( 𝑀 · 𝑁 ) ) → ( 𝑤 gcd 𝑀 ) ≤ ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) ) )
65 44 56 64 mp2and ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑀 ) ≤ ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) )
66 22 simprbi ⊢ ( 𝑤 ∈ 𝑊 → ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = 1 )
67 66 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = 1 )
68 65 67 breqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑀 ) ≤ 1 )
69 nnle1eq1 ⊢ ( ( 𝑤 gcd 𝑀 ) ∈ ℕ → ( ( 𝑤 gcd 𝑀 ) ≤ 1 ↔ ( 𝑤 gcd 𝑀 ) = 1 ) )
70 50 69 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( ( 𝑤 gcd 𝑀 ) ≤ 1 ↔ ( 𝑤 gcd 𝑀 ) = 1 ) )
71 68 70 mpbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑀 ) = 1 )
72 40 71 eqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( ( 𝑤 mod 𝑀 ) gcd 𝑀 ) = 1 )
73 oveq1 ⊢ ( 𝑦 = ( 𝑤 mod 𝑀 ) → ( 𝑦 gcd 𝑀 ) = ( ( 𝑤 mod 𝑀 ) gcd 𝑀 ) )
74 73 eqeq1d ⊢ ( 𝑦 = ( 𝑤 mod 𝑀 ) → ( ( 𝑦 gcd 𝑀 ) = 1 ↔ ( ( 𝑤 mod 𝑀 ) gcd 𝑀 ) = 1 ) )
75 74 5 elrab2 ⊢ ( ( 𝑤 mod 𝑀 ) ∈ 𝑈 ↔ ( ( 𝑤 mod 𝑀 ) ∈ ( 0 ..^ 𝑀 ) ∧ ( ( 𝑤 mod 𝑀 ) gcd 𝑀 ) = 1 ) )
76 38 72 75 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 mod 𝑀 ) ∈ 𝑈 )
77 zmodfzo ⊢ ( ( 𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑤 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
78 34 53 77 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
79 modgcd ⊢ ( ( 𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑤 mod 𝑁 ) gcd 𝑁 ) = ( 𝑤 gcd 𝑁 ) )
80 34 53 79 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( ( 𝑤 mod 𝑁 ) gcd 𝑁 ) = ( 𝑤 gcd 𝑁 ) )
81 gcddvds ⊢ ( ( 𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑤 gcd 𝑁 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑁 ) ∥ 𝑁 ) )
82 34 54 81 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( ( 𝑤 gcd 𝑁 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑁 ) ∥ 𝑁 ) )
83 82 simpld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑁 ) ∥ 𝑤 )
84 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
85 simpr ⊢ ( ( 𝑤 = 0 ∧ 𝑁 = 0 ) → 𝑁 = 0 )
86 85 necon3ai ⊢ ( 𝑁 ≠ 0 → ¬ ( 𝑤 = 0 ∧ 𝑁 = 0 ) )
87 53 84 86 3syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ¬ ( 𝑤 = 0 ∧ 𝑁 = 0 ) )
88 gcdn0cl ⊢ ( ( ( 𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑤 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑤 gcd 𝑁 ) ∈ ℕ )
89 34 54 87 88 syl21anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑁 ) ∈ ℕ )
90 89 nnzd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑁 ) ∈ ℤ )
91 82 simprd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑁 ) ∥ 𝑁 )
92 dvdsmul2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∥ ( 𝑀 · 𝑁 ) )
93 41 54 92 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → 𝑁 ∥ ( 𝑀 · 𝑁 ) )
94 90 54 58 91 93 dvdstrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑁 ) ∥ ( 𝑀 · 𝑁 ) )
95 dvdslegcd ⊢ ( ( ( ( 𝑤 gcd 𝑁 ) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) ∧ ¬ ( 𝑤 = 0 ∧ ( 𝑀 · 𝑁 ) = 0 ) ) → ( ( ( 𝑤 gcd 𝑁 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) → ( 𝑤 gcd 𝑁 ) ≤ ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) ) )
96 90 34 58 62 95 syl31anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( ( ( 𝑤 gcd 𝑁 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) → ( 𝑤 gcd 𝑁 ) ≤ ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) ) )
97 83 94 96 mp2and ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑁 ) ≤ ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) )
98 97 67 breqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑁 ) ≤ 1 )
99 nnle1eq1 ⊢ ( ( 𝑤 gcd 𝑁 ) ∈ ℕ → ( ( 𝑤 gcd 𝑁 ) ≤ 1 ↔ ( 𝑤 gcd 𝑁 ) = 1 ) )
100 89 99 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( ( 𝑤 gcd 𝑁 ) ≤ 1 ↔ ( 𝑤 gcd 𝑁 ) = 1 ) )
101 98 100 mpbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 gcd 𝑁 ) = 1 )
102 80 101 eqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( ( 𝑤 mod 𝑁 ) gcd 𝑁 ) = 1 )
103 oveq1 ⊢ ( 𝑦 = ( 𝑤 mod 𝑁 ) → ( 𝑦 gcd 𝑁 ) = ( ( 𝑤 mod 𝑁 ) gcd 𝑁 ) )
104 103 eqeq1d ⊢ ( 𝑦 = ( 𝑤 mod 𝑁 ) → ( ( 𝑦 gcd 𝑁 ) = 1 ↔ ( ( 𝑤 mod 𝑁 ) gcd 𝑁 ) = 1 ) )
105 104 6 elrab2 ⊢ ( ( 𝑤 mod 𝑁 ) ∈ 𝑉 ↔ ( ( 𝑤 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( 𝑤 mod 𝑁 ) gcd 𝑁 ) = 1 ) )
106 78 102 105 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝑤 mod 𝑁 ) ∈ 𝑉 )
107 76 106 opelxpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ⟨ ( 𝑤 mod 𝑀 ) , ( 𝑤 mod 𝑁 ) ⟩ ∈ ( 𝑈 × 𝑉 ) )
108 30 107 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝑈 × 𝑉 ) )
109 108 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑊 ( 𝐹 ‘ 𝑤 ) ∈ ( 𝑈 × 𝑉 ) )
110 1 2 3 4 crth ⊢ ( 𝜑 → 𝐹 : 𝑆 –1-1-onto→ 𝑇 )
111 f1ofn ⊢ ( 𝐹 : 𝑆 –1-1-onto→ 𝑇 → 𝐹 Fn 𝑆 )
112 fnfun ⊢ ( 𝐹 Fn 𝑆 → Fun 𝐹 )
113 110 111 112 3syl ⊢ ( 𝜑 → Fun 𝐹 )
114 7 ssrab3 ⊢ 𝑊 ⊆ 𝑆
115 fndm ⊢ ( 𝐹 Fn 𝑆 → dom 𝐹 = 𝑆 )
116 110 111 115 3syl ⊢ ( 𝜑 → dom 𝐹 = 𝑆 )
117 114 116 sseqtrrid ⊢ ( 𝜑 → 𝑊 ⊆ dom 𝐹 )
118 funimass4 ⊢ ( ( Fun 𝐹 ∧ 𝑊 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝑊 ) ⊆ ( 𝑈 × 𝑉 ) ↔ ∀ 𝑤 ∈ 𝑊 ( 𝐹 ‘ 𝑤 ) ∈ ( 𝑈 × 𝑉 ) ) )
119 113 117 118 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 “ 𝑊 ) ⊆ ( 𝑈 × 𝑉 ) ↔ ∀ 𝑤 ∈ 𝑊 ( 𝐹 ‘ 𝑤 ) ∈ ( 𝑈 × 𝑉 ) ) )
120 109 119 mpbird ⊢ ( 𝜑 → ( 𝐹 “ 𝑊 ) ⊆ ( 𝑈 × 𝑉 ) )
121 5 ssrab3 ⊢ 𝑈 ⊆ ( 0 ..^ 𝑀 )
122 6 ssrab3 ⊢ 𝑉 ⊆ ( 0 ..^ 𝑁 )
123 xpss12 ⊢ ( ( 𝑈 ⊆ ( 0 ..^ 𝑀 ) ∧ 𝑉 ⊆ ( 0 ..^ 𝑁 ) ) → ( 𝑈 × 𝑉 ) ⊆ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) ) )
124 121 122 123 mp2an ⊢ ( 𝑈 × 𝑉 ) ⊆ ( ( 0 ..^ 𝑀 ) × ( 0 ..^ 𝑁 ) )
125 124 2 sseqtrri ⊢ ( 𝑈 × 𝑉 ) ⊆ 𝑇
126 125 sseli ⊢ ( 𝑧 ∈ ( 𝑈 × 𝑉 ) → 𝑧 ∈ 𝑇 )
127 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑆 –1-1-onto→ 𝑇 ∧ 𝑧 ∈ 𝑇 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 )
128 110 126 127 syl2an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 )
129 f1ocnv ⊢ ( 𝐹 : 𝑆 –1-1-onto→ 𝑇 → ◡ 𝐹 : 𝑇 –1-1-onto→ 𝑆 )
130 f1of ⊢ ( ◡ 𝐹 : 𝑇 –1-1-onto→ 𝑆 → ◡ 𝐹 : 𝑇 ⟶ 𝑆 )
131 110 129 130 3syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝑇 ⟶ 𝑆 )
132 ffvelrn ⊢ ( ( ◡ 𝐹 : 𝑇 ⟶ 𝑆 ∧ 𝑧 ∈ 𝑇 ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑆 )
133 131 126 132 syl2an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑆 )
134 133 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) )
135 elfzoelz ⊢ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ℤ )
136 134 135 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ℤ )
137 35 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → 𝑀 ∈ ℕ )
138 modgcd ⊢ ( ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) gcd 𝑀 ) = ( ( ◡ 𝐹 ‘ 𝑧 ) gcd 𝑀 ) )
139 136 137 138 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) gcd 𝑀 ) = ( ( ◡ 𝐹 ‘ 𝑧 ) gcd 𝑀 ) )
140 oveq1 ⊢ ( 𝑤 = ( ◡ 𝐹 ‘ 𝑧 ) → ( 𝑤 mod 𝑀 ) = ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) )
141 oveq1 ⊢ ( 𝑤 = ( ◡ 𝐹 ‘ 𝑧 ) → ( 𝑤 mod 𝑁 ) = ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) )
142 140 141 opeq12d ⊢ ( 𝑤 = ( ◡ 𝐹 ‘ 𝑧 ) → ⟨ ( 𝑤 mod 𝑀 ) , ( 𝑤 mod 𝑁 ) ⟩ = ⟨ ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) , ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) ⟩ )
143 26 cbvmptv ⊢ ( 𝑥 ∈ 𝑆 ↦ ⟨ ( 𝑥 mod 𝑀 ) , ( 𝑥 mod 𝑁 ) ⟩ ) = ( 𝑤 ∈ 𝑆 ↦ ⟨ ( 𝑤 mod 𝑀 ) , ( 𝑤 mod 𝑁 ) ⟩ )
144 3 143 eqtri ⊢ 𝐹 = ( 𝑤 ∈ 𝑆 ↦ ⟨ ( 𝑤 mod 𝑀 ) , ( 𝑤 mod 𝑁 ) ⟩ )
145 opex ⊢ ⟨ ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) , ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) ⟩ ∈ V
146 142 144 145 fvmpt ⊢ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑆 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = ⟨ ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) , ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) ⟩ )
147 133 146 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = ⟨ ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) , ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) ⟩ )
148 128 147 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → 𝑧 = ⟨ ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) , ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) ⟩ )
149 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → 𝑧 ∈ ( 𝑈 × 𝑉 ) )
150 148 149 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ⟨ ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) , ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) ⟩ ∈ ( 𝑈 × 𝑉 ) )
151 opelxp ⊢ ( ⟨ ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) , ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) ⟩ ∈ ( 𝑈 × 𝑉 ) ↔ ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) ∈ 𝑈 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) ∈ 𝑉 ) )
152 150 151 sylib ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) ∈ 𝑈 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) ∈ 𝑉 ) )
153 152 simpld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) ∈ 𝑈 )
154 oveq1 ⊢ ( 𝑦 = ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) → ( 𝑦 gcd 𝑀 ) = ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) gcd 𝑀 ) )
155 154 eqeq1d ⊢ ( 𝑦 = ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) → ( ( 𝑦 gcd 𝑀 ) = 1 ↔ ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) gcd 𝑀 ) = 1 ) )
156 155 5 elrab2 ⊢ ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) ∈ 𝑈 ↔ ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) ∈ ( 0 ..^ 𝑀 ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) gcd 𝑀 ) = 1 ) )
157 153 156 sylib ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) ∈ ( 0 ..^ 𝑀 ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) gcd 𝑀 ) = 1 ) )
158 157 simprd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑀 ) gcd 𝑀 ) = 1 )
159 139 158 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ( ◡ 𝐹 ‘ 𝑧 ) gcd 𝑀 ) = 1 )
160 52 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → 𝑁 ∈ ℕ )
161 modgcd ⊢ ( ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) gcd 𝑁 ) = ( ( ◡ 𝐹 ‘ 𝑧 ) gcd 𝑁 ) )
162 136 160 161 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) gcd 𝑁 ) = ( ( ◡ 𝐹 ‘ 𝑧 ) gcd 𝑁 ) )
163 152 simprd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) ∈ 𝑉 )
164 oveq1 ⊢ ( 𝑦 = ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) → ( 𝑦 gcd 𝑁 ) = ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) gcd 𝑁 ) )
165 164 eqeq1d ⊢ ( 𝑦 = ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) → ( ( 𝑦 gcd 𝑁 ) = 1 ↔ ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) gcd 𝑁 ) = 1 ) )
166 165 6 elrab2 ⊢ ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) ∈ 𝑉 ↔ ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) gcd 𝑁 ) = 1 ) )
167 163 166 sylib ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) gcd 𝑁 ) = 1 ) )
168 167 simprd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ( ( ◡ 𝐹 ‘ 𝑧 ) mod 𝑁 ) gcd 𝑁 ) = 1 )
169 162 168 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ( ◡ 𝐹 ‘ 𝑧 ) gcd 𝑁 ) = 1 )
170 35 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
171 170 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → 𝑀 ∈ ℤ )
172 52 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
173 172 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → 𝑁 ∈ ℤ )
174 rpmul ⊢ ( ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( ◡ 𝐹 ‘ 𝑧 ) gcd 𝑀 ) = 1 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) gcd 𝑁 ) = 1 ) → ( ( ◡ 𝐹 ‘ 𝑧 ) gcd ( 𝑀 · 𝑁 ) ) = 1 ) )
175 136 171 173 174 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ( ( ( ◡ 𝐹 ‘ 𝑧 ) gcd 𝑀 ) = 1 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) gcd 𝑁 ) = 1 ) → ( ( ◡ 𝐹 ‘ 𝑧 ) gcd ( 𝑀 · 𝑁 ) ) = 1 ) )
176 159 169 175 mp2and ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ( ◡ 𝐹 ‘ 𝑧 ) gcd ( 𝑀 · 𝑁 ) ) = 1 )
177 oveq1 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑧 ) → ( 𝑦 gcd ( 𝑀 · 𝑁 ) ) = ( ( ◡ 𝐹 ‘ 𝑧 ) gcd ( 𝑀 · 𝑁 ) ) )
178 177 eqeq1d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑧 ) → ( ( 𝑦 gcd ( 𝑀 · 𝑁 ) ) = 1 ↔ ( ( ◡ 𝐹 ‘ 𝑧 ) gcd ( 𝑀 · 𝑁 ) ) = 1 ) )
179 178 7 elrab2 ⊢ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑊 ↔ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑆 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) gcd ( 𝑀 · 𝑁 ) ) = 1 ) )
180 133 176 179 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑊 )
181 funfvima2 ⊢ ( ( Fun 𝐹 ∧ 𝑊 ⊆ dom 𝐹 ) → ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑊 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐹 “ 𝑊 ) ) )
182 113 117 181 syl2anc ⊢ ( 𝜑 → ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑊 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐹 “ 𝑊 ) ) )
183 182 imp ⊢ ( ( 𝜑 ∧ ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑊 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐹 “ 𝑊 ) )
184 180 183 syldan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐹 “ 𝑊 ) )
185 128 184 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑈 × 𝑉 ) ) → 𝑧 ∈ ( 𝐹 “ 𝑊 ) )
186 120 185 eqelssd ⊢ ( 𝜑 → ( 𝐹 “ 𝑊 ) = ( 𝑈 × 𝑉 ) )
187 f1of1 ⊢ ( 𝐹 : 𝑆 –1-1-onto→ 𝑇 → 𝐹 : 𝑆 –1-1→ 𝑇 )
188 110 187 syl ⊢ ( 𝜑 → 𝐹 : 𝑆 –1-1→ 𝑇 )
189 fzofi ⊢ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ∈ Fin
190 1 189 eqeltri ⊢ 𝑆 ∈ Fin
191 ssfi ⊢ ( ( 𝑆 ∈ Fin ∧ 𝑊 ⊆ 𝑆 ) → 𝑊 ∈ Fin )
192 190 114 191 mp2an ⊢ 𝑊 ∈ Fin
193 192 elexi ⊢ 𝑊 ∈ V
194 193 f1imaen ⊢ ( ( 𝐹 : 𝑆 –1-1→ 𝑇 ∧ 𝑊 ⊆ 𝑆 ) → ( 𝐹 “ 𝑊 ) ≈ 𝑊 )
195 188 114 194 sylancl ⊢ ( 𝜑 → ( 𝐹 “ 𝑊 ) ≈ 𝑊 )
196 186 195 eqbrtrrd ⊢ ( 𝜑 → ( 𝑈 × 𝑉 ) ≈ 𝑊 )
197 xpfi ⊢ ( ( 𝑈 ∈ Fin ∧ 𝑉 ∈ Fin ) → ( 𝑈 × 𝑉 ) ∈ Fin )
198 12 17 197 mp2an ⊢ ( 𝑈 × 𝑉 ) ∈ Fin
199 hashen ⊢ ( ( ( 𝑈 × 𝑉 ) ∈ Fin ∧ 𝑊 ∈ Fin ) → ( ( ♯ ‘ ( 𝑈 × 𝑉 ) ) = ( ♯ ‘ 𝑊 ) ↔ ( 𝑈 × 𝑉 ) ≈ 𝑊 ) )
200 198 192 199 mp2an ⊢ ( ( ♯ ‘ ( 𝑈 × 𝑉 ) ) = ( ♯ ‘ 𝑊 ) ↔ ( 𝑈 × 𝑉 ) ≈ 𝑊 )
201 196 200 sylibr ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑈 × 𝑉 ) ) = ( ♯ ‘ 𝑊 ) )
202 19 201 syl5reqr ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = ( ( ♯ ‘ 𝑈 ) · ( ♯ ‘ 𝑉 ) ) )
203 35 52 nnmulcld ⊢ ( 𝜑 → ( 𝑀 · 𝑁 ) ∈ ℕ )
204 dfphi2 ⊢ ( ( 𝑀 · 𝑁 ) ∈ ℕ → ( ϕ ‘ ( 𝑀 · 𝑁 ) ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 · 𝑁 ) ) = 1 } ) )
205 1 rabeqi ⊢ { 𝑦 ∈ 𝑆 ∣ ( 𝑦 gcd ( 𝑀 · 𝑁 ) ) = 1 } = { 𝑦 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 · 𝑁 ) ) = 1 }
206 7 205 eqtri ⊢ 𝑊 = { 𝑦 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 · 𝑁 ) ) = 1 }
207 206 fveq2i ⊢ ( ♯ ‘ 𝑊 ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ ( 𝑀 · 𝑁 ) ) ∣ ( 𝑦 gcd ( 𝑀 · 𝑁 ) ) = 1 } )
208 204 207 eqtr4di ⊢ ( ( 𝑀 · 𝑁 ) ∈ ℕ → ( ϕ ‘ ( 𝑀 · 𝑁 ) ) = ( ♯ ‘ 𝑊 ) )
209 203 208 syl ⊢ ( 𝜑 → ( ϕ ‘ ( 𝑀 · 𝑁 ) ) = ( ♯ ‘ 𝑊 ) )
210 dfphi2 ⊢ ( 𝑀 ∈ ℕ → ( ϕ ‘ 𝑀 ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑦 gcd 𝑀 ) = 1 } ) )
211 5 fveq2i ⊢ ( ♯ ‘ 𝑈 ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑦 gcd 𝑀 ) = 1 } )
212 210 211 eqtr4di ⊢ ( 𝑀 ∈ ℕ → ( ϕ ‘ 𝑀 ) = ( ♯ ‘ 𝑈 ) )
213 35 212 syl ⊢ ( 𝜑 → ( ϕ ‘ 𝑀 ) = ( ♯ ‘ 𝑈 ) )
214 dfphi2 ⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 } ) )
215 6 fveq2i ⊢ ( ♯ ‘ 𝑉 ) = ( ♯ ‘ { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 } )
216 214 215 eqtr4di ⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ 𝑉 ) )
217 52 216 syl ⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ 𝑉 ) )
218 213 217 oveq12d ⊢ ( 𝜑 → ( ( ϕ ‘ 𝑀 ) · ( ϕ ‘ 𝑁 ) ) = ( ( ♯ ‘ 𝑈 ) · ( ♯ ‘ 𝑉 ) ) )
219 202 209 218 3eqtr4d ⊢ ( 𝜑 → ( ϕ ‘ ( 𝑀 · 𝑁 ) ) = ( ( ϕ ‘ 𝑀 ) · ( ϕ ‘ 𝑁 ) ) )