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