ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  phimullem GIF version

Theorem phimullem 10995
Description: Lemma for phimul 10996. (Contributed by Mario Carneiro, 24-Feb-2014.)
Hypotheses
Ref Expression
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
Ref Expression
phimullem (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))
Distinct variable groups:   𝑦,𝐹   𝑥,𝑀   𝑥,𝑁   𝑥,𝑆,𝑦   𝑥,𝑇   𝜑,𝑥,𝑦   𝑦,𝑀   𝑦,𝑁
Allowed substitution hints:   𝑇(𝑦)   𝑈(𝑥,𝑦)   𝐹(𝑥)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem phimullem
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 5601 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (𝑦 gcd (𝑀 · 𝑁)) = (𝑤 gcd (𝑀 · 𝑁)))
21eqeq1d 2093 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ (𝑤 gcd (𝑀 · 𝑁)) = 1))
3 phimul.6 . . . . . . . . . . . . 13 𝑊 = {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
42, 3elrab2 2764 . . . . . . . . . . . 12 (𝑤𝑊 ↔ (𝑤𝑆 ∧ (𝑤 gcd (𝑀 · 𝑁)) = 1))
54simplbi 268 . . . . . . . . . . 11 (𝑤𝑊𝑤𝑆)
65adantl 271 . . . . . . . . . 10 ((𝜑𝑤𝑊) → 𝑤𝑆)
7 elfzoelz 9462 . . . . . . . . . . . . . . 15 (𝑤 ∈ (0..^(𝑀 · 𝑁)) → 𝑤 ∈ ℤ)
8 crth.1 . . . . . . . . . . . . . . 15 𝑆 = (0..^(𝑀 · 𝑁))
97, 8eleq2s 2179 . . . . . . . . . . . . . 14 (𝑤𝑆𝑤 ∈ ℤ)
106, 9syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑤 ∈ ℤ)
11 zq 9020 . . . . . . . . . . . . 13 (𝑤 ∈ ℤ → 𝑤 ∈ ℚ)
1210, 11syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑤 ∈ ℚ)
13 crth.4 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))
1413simp1d 953 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℕ)
1514adantr 270 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑀 ∈ ℕ)
16 nnq 9027 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
1715, 16syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑀 ∈ ℚ)
1815nngt0d 8377 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 0 < 𝑀)
1912, 17, 18modqcld 9638 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ ℚ)
2013simp2d 954 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ)
2120adantr 270 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑁 ∈ ℕ)
22 nnq 9027 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
2321, 22syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑁 ∈ ℚ)
2421nngt0d 8377 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 0 < 𝑁)
2512, 23, 24modqcld 9638 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ ℚ)
26 opexg 4022 . . . . . . . . . . 11 (((𝑤 mod 𝑀) ∈ ℚ ∧ (𝑤 mod 𝑁) ∈ ℚ) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V)
2719, 25, 26syl2anc 403 . . . . . . . . . 10 ((𝜑𝑤𝑊) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V)
28 oveq1 5601 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑥 mod 𝑀) = (𝑤 mod 𝑀))
29 oveq1 5601 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑥 mod 𝑁) = (𝑤 mod 𝑁))
3028, 29opeq12d 3607 . . . . . . . . . . 11 (𝑥 = 𝑤 → ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩ = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
31 crth.3 . . . . . . . . . . 11 𝐹 = (𝑥𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)
3230, 31fvmptg 5328 . . . . . . . . . 10 ((𝑤𝑆 ∧ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V) → (𝐹𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
336, 27, 32syl2anc 403 . . . . . . . . 9 ((𝜑𝑤𝑊) → (𝐹𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
345, 8syl6eleq 2177 . . . . . . . . . . . . . 14 (𝑤𝑊𝑤 ∈ (0..^(𝑀 · 𝑁)))
3534adantl 271 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑤 ∈ (0..^(𝑀 · 𝑁)))
3635, 7syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑤 ∈ ℤ)
37 zmodfzo 9657 . . . . . . . . . . . 12 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
3836, 15, 37syl2anc 403 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
39 modgcd 10776 . . . . . . . . . . . . 13 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
4036, 15, 39syl2anc 403 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
4115nnzd 8777 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → 𝑀 ∈ ℤ)
42 gcddvds 10749 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
4336, 41, 42syl2anc 403 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
4443simpld 110 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ 𝑤)
45 nnne0 8362 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℕ → 𝑀 ≠ 0)
46 simpr 108 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
4746necon3ai 2300 . . . . . . . . . . . . . . . . . . 19 (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
4815, 45, 473syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
49 gcdn0cl 10748 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
5036, 41, 48, 49syl21anc 1171 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∈ ℕ)
5150nnzd 8777 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∈ ℤ)
5221nnzd 8777 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → 𝑁 ∈ ℤ)
5343simprd 112 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ 𝑀)
5451, 41, 52, 53dvdsmultr1d 10629 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁))
5515, 21nnmulcld 8382 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑀 · 𝑁) ∈ ℕ)
5655nnzd 8777 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑀 · 𝑁) ∈ ℤ)
57 nnne0 8362 . . . . . . . . . . . . . . . . 17 ((𝑀 · 𝑁) ∈ ℕ → (𝑀 · 𝑁) ≠ 0)
58 simpr 108 . . . . . . . . . . . . . . . . . 18 ((𝑤 = 0 ∧ (𝑀 · 𝑁) = 0) → (𝑀 · 𝑁) = 0)
5958necon3ai 2300 . . . . . . . . . . . . . . . . 17 ((𝑀 · 𝑁) ≠ 0 → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
6055, 57, 593syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
61 dvdslegcd 10750 . . . . . . . . . . . . . . . 16 ((((𝑤 gcd 𝑀) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))))
6251, 36, 56, 60, 61syl31anc 1175 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))))
6344, 54, 62mp2and 424 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁)))
644simprbi 269 . . . . . . . . . . . . . . 15 (𝑤𝑊 → (𝑤 gcd (𝑀 · 𝑁)) = 1)
6564adantl 271 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd (𝑀 · 𝑁)) = 1)
6663, 65breqtrd 3838 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ≤ 1)
67 nnle1eq1 8358 . . . . . . . . . . . . . 14 ((𝑤 gcd 𝑀) ∈ ℕ → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
6850, 67syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
6966, 68mpbid 145 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) = 1)
7040, 69eqtrd 2117 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = 1)
71 oveq1 5601 . . . . . . . . . . . . 13 (𝑦 = (𝑤 mod 𝑀) → (𝑦 gcd 𝑀) = ((𝑤 mod 𝑀) gcd 𝑀))
7271eqeq1d 2093 . . . . . . . . . . . 12 (𝑦 = (𝑤 mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
73 phimul.4 . . . . . . . . . . . 12 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}
7472, 73elrab2 2764 . . . . . . . . . . 11 ((𝑤 mod 𝑀) ∈ 𝑈 ↔ ((𝑤 mod 𝑀) ∈ (0..^𝑀) ∧ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
7538, 70, 74sylanbrc 408 . . . . . . . . . 10 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ 𝑈)
76 zmodfzo 9657 . . . . . . . . . . . 12 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
7736, 21, 76syl2anc 403 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
78 modgcd 10776 . . . . . . . . . . . . 13 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
7936, 21, 78syl2anc 403 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
80 gcddvds 10749 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
8136, 52, 80syl2anc 403 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
8281simpld 110 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ 𝑤)
8381simprd 112 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ 𝑁)
84 dvdsmul2 10613 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁))
8541, 52, 84syl2anc 403 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → 𝑁 ∥ (𝑀 · 𝑁))
86 nnne0 8362 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
87 simpr 108 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
8887necon3ai 2300 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
8921, 86, 883syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
90 gcdn0cl 10748 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
9136, 52, 89, 90syl21anc 1171 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∈ ℕ)
9291nnzd 8777 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∈ ℤ)
93 dvdstr 10627 . . . . . . . . . . . . . . . . 17 (((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑤 gcd 𝑁) ∥ 𝑁𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)))
9492, 52, 56, 93syl3anc 1172 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑁𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)))
9583, 85, 94mp2and 424 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁))
96 dvdslegcd 10750 . . . . . . . . . . . . . . . 16 ((((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))))
9792, 36, 56, 60, 96syl31anc 1175 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))))
9882, 95, 97mp2and 424 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁)))
9998, 65breqtrd 3838 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ≤ 1)
100 nnle1eq1 8358 . . . . . . . . . . . . . 14 ((𝑤 gcd 𝑁) ∈ ℕ → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
10191, 100syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
10299, 101mpbid 145 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) = 1)
10379, 102eqtrd 2117 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = 1)
104 oveq1 5601 . . . . . . . . . . . . 13 (𝑦 = (𝑤 mod 𝑁) → (𝑦 gcd 𝑁) = ((𝑤 mod 𝑁) gcd 𝑁))
105104eqeq1d 2093 . . . . . . . . . . . 12 (𝑦 = (𝑤 mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
106 phimul.5 . . . . . . . . . . . 12 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
107105, 106elrab2 2764 . . . . . . . . . . 11 ((𝑤 mod 𝑁) ∈ 𝑉 ↔ ((𝑤 mod 𝑁) ∈ (0..^𝑁) ∧ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
10877, 103, 107sylanbrc 408 . . . . . . . . . 10 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ 𝑉)
109 opelxpi 4435 . . . . . . . . . 10 (((𝑤 mod 𝑀) ∈ 𝑈 ∧ (𝑤 mod 𝑁) ∈ 𝑉) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
11075, 108, 109syl2anc 403 . . . . . . . . 9 ((𝜑𝑤𝑊) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
11133, 110eqeltrd 2161 . . . . . . . 8 ((𝜑𝑤𝑊) → (𝐹𝑤) ∈ (𝑈 × 𝑉))
112111ralrimiva 2442 . . . . . . 7 (𝜑 → ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉))
113 crth.2 . . . . . . . . . 10 𝑇 = ((0..^𝑀) × (0..^𝑁))
1148, 113, 31, 13crth 10994 . . . . . . . . 9 (𝜑𝐹:𝑆1-1-onto𝑇)
115 f1ofn 5205 . . . . . . . . 9 (𝐹:𝑆1-1-onto𝑇𝐹 Fn 𝑆)
116 fnfun 5067 . . . . . . . . 9 (𝐹 Fn 𝑆 → Fun 𝐹)
117114, 115, 1163syl 17 . . . . . . . 8 (𝜑 → Fun 𝐹)
118 ssrab2 3092 . . . . . . . . . 10 {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} ⊆ 𝑆
1193, 118eqsstri 3042 . . . . . . . . 9 𝑊𝑆
120 fndm 5069 . . . . . . . . . 10 (𝐹 Fn 𝑆 → dom 𝐹 = 𝑆)
121114, 115, 1203syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝑆)
122119, 121syl5sseqr 3061 . . . . . . . 8 (𝜑𝑊 ⊆ dom 𝐹)
123 funimass4 5303 . . . . . . . 8 ((Fun 𝐹𝑊 ⊆ dom 𝐹) → ((𝐹𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉)))
124117, 122, 123syl2anc 403 . . . . . . 7 (𝜑 → ((𝐹𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉)))
125112, 124mpbird 165 . . . . . 6 (𝜑 → (𝐹𝑊) ⊆ (𝑈 × 𝑉))
126 ssrab2 3092 . . . . . . . . . . . . . 14 {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ⊆ (0..^𝑀)
12773, 126eqsstri 3042 . . . . . . . . . . . . 13 𝑈 ⊆ (0..^𝑀)
128 ssrab2 3092 . . . . . . . . . . . . . 14 {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)
129106, 128eqsstri 3042 . . . . . . . . . . . . 13 𝑉 ⊆ (0..^𝑁)
130 xpss12 4506 . . . . . . . . . . . . 13 ((𝑈 ⊆ (0..^𝑀) ∧ 𝑉 ⊆ (0..^𝑁)) → (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁)))
131127, 129, 130mp2an 417 . . . . . . . . . . . 12 (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁))
132131, 113sseqtr4i 3045 . . . . . . . . . . 11 (𝑈 × 𝑉) ⊆ 𝑇
133132sseli 3008 . . . . . . . . . 10 (𝑧 ∈ (𝑈 × 𝑉) → 𝑧𝑇)
134 f1ocnvfv2 5500 . . . . . . . . . 10 ((𝐹:𝑆1-1-onto𝑇𝑧𝑇) → (𝐹‘(𝐹𝑧)) = 𝑧)
135114, 133, 134syl2an 283 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) = 𝑧)
136 f1ocnv 5217 . . . . . . . . . . . . 13 (𝐹:𝑆1-1-onto𝑇𝐹:𝑇1-1-onto𝑆)
137 f1of 5204 . . . . . . . . . . . . 13 (𝐹:𝑇1-1-onto𝑆𝐹:𝑇𝑆)
138114, 136, 1373syl 17 . . . . . . . . . . . 12 (𝜑𝐹:𝑇𝑆)
139 ffvelrn 5380 . . . . . . . . . . . 12 ((𝐹:𝑇𝑆𝑧𝑇) → (𝐹𝑧) ∈ 𝑆)
140138, 133, 139syl2an 283 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ 𝑆)
141140, 8syl6eleq 2177 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ (0..^(𝑀 · 𝑁)))
142 elfzoelz 9462 . . . . . . . . . . . . . . 15 ((𝐹𝑧) ∈ (0..^(𝑀 · 𝑁)) → (𝐹𝑧) ∈ ℤ)
143141, 142syl 14 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ ℤ)
14414adantr 270 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℕ)
145 modgcd 10776 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ ℤ ∧ 𝑀 ∈ ℕ) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = ((𝐹𝑧) gcd 𝑀))
146143, 144, 145syl2anc 403 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = ((𝐹𝑧) gcd 𝑀))
147 zq 9020 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑧) ∈ ℤ → (𝐹𝑧) ∈ ℚ)
148143, 147syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ ℚ)
149144, 16syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℚ)
150144nngt0d 8377 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 0 < 𝑀)
151148, 149, 150modqcld 9638 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑀) ∈ ℚ)
15220adantr 270 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℕ)
153152, 22syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℚ)
154152nngt0d 8377 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 0 < 𝑁)
155148, 153, 154modqcld 9638 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑁) ∈ ℚ)
156 opexg 4022 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑧) mod 𝑀) ∈ ℚ ∧ ((𝐹𝑧) mod 𝑁) ∈ ℚ) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V)
157151, 155, 156syl2anc 403 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V)
158 oveq1 5601 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝐹𝑧) → (𝑤 mod 𝑀) = ((𝐹𝑧) mod 𝑀))
159 oveq1 5601 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝐹𝑧) → (𝑤 mod 𝑁) = ((𝐹𝑧) mod 𝑁))
160158, 159opeq12d 3607 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = (𝐹𝑧) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
16130cbvmptv 3902 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩) = (𝑤𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
16231, 161eqtri 2105 . . . . . . . . . . . . . . . . . . . . 21 𝐹 = (𝑤𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
163160, 162fvmptg 5328 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑧) ∈ 𝑆 ∧ ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V) → (𝐹‘(𝐹𝑧)) = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
164140, 157, 163syl2anc 403 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
165135, 164eqtr3d 2119 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
166 simpr 108 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝑈 × 𝑉))
167165, 166eqeltrrd 2162 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
168 opelxp 4433 . . . . . . . . . . . . . . . . 17 (⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉) ↔ (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ∧ ((𝐹𝑧) mod 𝑁) ∈ 𝑉))
169167, 168sylib 120 . . . . . . . . . . . . . . . 16 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ∧ ((𝐹𝑧) mod 𝑁) ∈ 𝑉))
170169simpld 110 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑀) ∈ 𝑈)
171 oveq1 5601 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝐹𝑧) mod 𝑀) → (𝑦 gcd 𝑀) = (((𝐹𝑧) mod 𝑀) gcd 𝑀))
172171eqeq1d 2093 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝐹𝑧) mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
173172, 73elrab2 2764 . . . . . . . . . . . . . . 15 (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ↔ (((𝐹𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
174170, 173sylib 120 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
175174simprd 112 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1)
176146, 175eqtr3d 2119 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd 𝑀) = 1)
177 modgcd 10776 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = ((𝐹𝑧) gcd 𝑁))
178143, 152, 177syl2anc 403 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = ((𝐹𝑧) gcd 𝑁))
179169simprd 112 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑁) ∈ 𝑉)
180 oveq1 5601 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝐹𝑧) mod 𝑁) → (𝑦 gcd 𝑁) = (((𝐹𝑧) mod 𝑁) gcd 𝑁))
181180eqeq1d 2093 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝐹𝑧) mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
182181, 106elrab2 2764 . . . . . . . . . . . . . . 15 (((𝐹𝑧) mod 𝑁) ∈ 𝑉 ↔ (((𝐹𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
183179, 182sylib 120 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
184183simprd 112 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1)
185178, 184eqtr3d 2119 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd 𝑁) = 1)
18614nnzd 8777 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℤ)
187186adantr 270 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℤ)
18820nnzd 8777 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
189188adantr 270 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℤ)
190 rpmul 10874 . . . . . . . . . . . . 13 (((𝐹𝑧) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((((𝐹𝑧) gcd 𝑀) = 1 ∧ ((𝐹𝑧) gcd 𝑁) = 1) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
191143, 187, 189, 190syl3anc 1172 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((((𝐹𝑧) gcd 𝑀) = 1 ∧ ((𝐹𝑧) gcd 𝑁) = 1) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
192176, 185, 191mp2and 424 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1)
193 oveq1 5601 . . . . . . . . . . . . 13 (𝑦 = (𝐹𝑧) → (𝑦 gcd (𝑀 · 𝑁)) = ((𝐹𝑧) gcd (𝑀 · 𝑁)))
194193eqeq1d 2093 . . . . . . . . . . . 12 (𝑦 = (𝐹𝑧) → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
195194, 3elrab2 2764 . . . . . . . . . . 11 ((𝐹𝑧) ∈ 𝑊 ↔ ((𝐹𝑧) ∈ 𝑆 ∧ ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
196140, 192, 195sylanbrc 408 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ 𝑊)
197 funfvima2 5470 . . . . . . . . . . . 12 ((Fun 𝐹𝑊 ⊆ dom 𝐹) → ((𝐹𝑧) ∈ 𝑊 → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊)))
198117, 122, 197syl2anc 403 . . . . . . . . . . 11 (𝜑 → ((𝐹𝑧) ∈ 𝑊 → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊)))
199198imp 122 . . . . . . . . . 10 ((𝜑 ∧ (𝐹𝑧) ∈ 𝑊) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊))
200196, 199syldan 276 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊))
201135, 200eqeltrrd 2162 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝐹𝑊))
202201ex 113 . . . . . . 7 (𝜑 → (𝑧 ∈ (𝑈 × 𝑉) → 𝑧 ∈ (𝐹𝑊)))
203202ssrdv 3018 . . . . . 6 (𝜑 → (𝑈 × 𝑉) ⊆ (𝐹𝑊))
204125, 203eqssd 3029 . . . . 5 (𝜑 → (𝐹𝑊) = (𝑈 × 𝑉))
205 f1of1 5203 . . . . . . 7 (𝐹:𝑆1-1-onto𝑇𝐹:𝑆1-1𝑇)
206114, 205syl 14 . . . . . 6 (𝜑𝐹:𝑆1-1𝑇)
207119a1i 9 . . . . . 6 (𝜑𝑊𝑆)
208 0z 8671 . . . . . . . . . 10 0 ∈ ℤ
209186, 188zmulcld 8784 . . . . . . . . . 10 (𝜑 → (𝑀 · 𝑁) ∈ ℤ)
210 fzofig 9742 . . . . . . . . . 10 ((0 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (0..^(𝑀 · 𝑁)) ∈ Fin)
211208, 209, 210sylancr 405 . . . . . . . . 9 (𝜑 → (0..^(𝑀 · 𝑁)) ∈ Fin)
2128, 211syl5eqel 2171 . . . . . . . 8 (𝜑𝑆 ∈ Fin)
213 elfzoelz 9462 . . . . . . . . . . . . . 14 (𝑦 ∈ (0..^(𝑀 · 𝑁)) → 𝑦 ∈ ℤ)
214213, 8eleq2s 2179 . . . . . . . . . . . . 13 (𝑦𝑆𝑦 ∈ ℤ)
215214adantl 271 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 𝑦 ∈ ℤ)
216209adantr 270 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (𝑀 · 𝑁) ∈ ℤ)
217215, 216gcdcld 10754 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → (𝑦 gcd (𝑀 · 𝑁)) ∈ ℕ0)
218217nn0zd 8776 . . . . . . . . . 10 ((𝜑𝑦𝑆) → (𝑦 gcd (𝑀 · 𝑁)) ∈ ℤ)
219 1zzd 8687 . . . . . . . . . 10 ((𝜑𝑦𝑆) → 1 ∈ ℤ)
220 zdceq 8732 . . . . . . . . . 10 (((𝑦 gcd (𝑀 · 𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
221218, 219, 220syl2anc 403 . . . . . . . . 9 ((𝜑𝑦𝑆) → DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
222221ralrimiva 2442 . . . . . . . 8 (𝜑 → ∀𝑦𝑆 DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
223212, 222ssfirab 6571 . . . . . . 7 (𝜑 → {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} ∈ Fin)
2243, 223syl5eqel 2171 . . . . . 6 (𝜑𝑊 ∈ Fin)
225 f1imaeng 6442 . . . . . 6 ((𝐹:𝑆1-1𝑇𝑊𝑆𝑊 ∈ Fin) → (𝐹𝑊) ≈ 𝑊)
226206, 207, 224, 225syl3anc 1172 . . . . 5 (𝜑 → (𝐹𝑊) ≈ 𝑊)
227204, 226eqbrtrrd 3836 . . . 4 (𝜑 → (𝑈 × 𝑉) ≈ 𝑊)
228 fzofig 9742 . . . . . . . . 9 ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0..^𝑀) ∈ Fin)
229208, 186, 228sylancr 405 . . . . . . . 8 (𝜑 → (0..^𝑀) ∈ Fin)
230 elfzoelz 9462 . . . . . . . . . . . . 13 (𝑦 ∈ (0..^𝑀) → 𝑦 ∈ ℤ)
231230adantl 271 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑀)) → 𝑦 ∈ ℤ)
232186adantr 270 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑀)) → 𝑀 ∈ ℤ)
233231, 232gcdcld 10754 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0..^𝑀)) → (𝑦 gcd 𝑀) ∈ ℕ0)
234233nn0zd 8776 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑀)) → (𝑦 gcd 𝑀) ∈ ℤ)
235 1z 8686 . . . . . . . . . 10 1 ∈ ℤ
236 zdceq 8732 . . . . . . . . . 10 (((𝑦 gcd 𝑀) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd 𝑀) = 1)
237234, 235, 236sylancl 404 . . . . . . . . 9 ((𝜑𝑦 ∈ (0..^𝑀)) → DECID (𝑦 gcd 𝑀) = 1)
238237ralrimiva 2442 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (0..^𝑀)DECID (𝑦 gcd 𝑀) = 1)
239229, 238ssfirab 6571 . . . . . . 7 (𝜑 → {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ∈ Fin)
24073, 239syl5eqel 2171 . . . . . 6 (𝜑𝑈 ∈ Fin)
241 fzofig 9742 . . . . . . . . 9 ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0..^𝑁) ∈ Fin)
242208, 188, 241sylancr 405 . . . . . . . 8 (𝜑 → (0..^𝑁) ∈ Fin)
243 elfzoelz 9462 . . . . . . . . . . . . 13 (𝑦 ∈ (0..^𝑁) → 𝑦 ∈ ℤ)
244243adantl 271 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑁)) → 𝑦 ∈ ℤ)
245188adantr 270 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑁)) → 𝑁 ∈ ℤ)
246244, 245gcdcld 10754 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0..^𝑁)) → (𝑦 gcd 𝑁) ∈ ℕ0)
247246nn0zd 8776 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑁)) → (𝑦 gcd 𝑁) ∈ ℤ)
248 1zzd 8687 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑁)) → 1 ∈ ℤ)
249 zdceq 8732 . . . . . . . . . 10 (((𝑦 gcd 𝑁) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd 𝑁) = 1)
250247, 248, 249syl2anc 403 . . . . . . . . 9 ((𝜑𝑦 ∈ (0..^𝑁)) → DECID (𝑦 gcd 𝑁) = 1)
251250ralrimiva 2442 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (0..^𝑁)DECID (𝑦 gcd 𝑁) = 1)
252242, 251ssfirab 6571 . . . . . . 7 (𝜑 → {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ∈ Fin)
253106, 252syl5eqel 2171 . . . . . 6 (𝜑𝑉 ∈ Fin)
254 xpfi 6568 . . . . . 6 ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (𝑈 × 𝑉) ∈ Fin)
255240, 253, 254syl2anc 403 . . . . 5 (𝜑 → (𝑈 × 𝑉) ∈ Fin)
256 hashen 10041 . . . . 5 (((𝑈 × 𝑉) ∈ Fin ∧ 𝑊 ∈ Fin) → ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊))
257255, 224, 256syl2anc 403 . . . 4 (𝜑 → ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊))
258227, 257mpbird 165 . . 3 (𝜑 → (♯‘(𝑈 × 𝑉)) = (♯‘𝑊))
259 hashxp 10083 . . . 4 ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (♯‘(𝑈 × 𝑉)) = ((♯‘𝑈) · (♯‘𝑉)))
260240, 253, 259syl2anc 403 . . 3 (𝜑 → (♯‘(𝑈 × 𝑉)) = ((♯‘𝑈) · (♯‘𝑉)))
261258, 260eqtr3d 2119 . 2 (𝜑 → (♯‘𝑊) = ((♯‘𝑈) · (♯‘𝑉)))
26214, 20nnmulcld 8382 . . 3 (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
263 dfphi2 10990 . . . 4 ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}))
2648rabeqi 2607 . . . . . 6 {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
2653, 264eqtri 2105 . . . . 5 𝑊 = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
266265fveq2i 5259 . . . 4 (♯‘𝑊) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1})
267263, 266syl6eqr 2135 . . 3 ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊))
268262, 267syl 14 . 2 (𝜑 → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊))
269 dfphi2 10990 . . . . 5 (𝑀 ∈ ℕ → (ϕ‘𝑀) = (♯‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}))
27073fveq2i 5259 . . . . 5 (♯‘𝑈) = (♯‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1})
271269, 270syl6eqr 2135 . . . 4 (𝑀 ∈ ℕ → (ϕ‘𝑀) = (♯‘𝑈))
27214, 271syl 14 . . 3 (𝜑 → (ϕ‘𝑀) = (♯‘𝑈))
273 dfphi2 10990 . . . . 5 (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}))
274106fveq2i 5259 . . . . 5 (♯‘𝑉) = (♯‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1})
275273, 274syl6eqr 2135 . . . 4 (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘𝑉))
27620, 275syl 14 . . 3 (𝜑 → (ϕ‘𝑁) = (♯‘𝑉))
277272, 276oveq12d 5612 . 2 (𝜑 → ((ϕ‘𝑀) · (ϕ‘𝑁)) = ((♯‘𝑈) · (♯‘𝑉)))
278261, 268, 2773eqtr4d 2127 1 (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  DECID wdc 778  w3a 922   = wceq 1287  wcel 1436  wne 2251  wral 2355  {crab 2359  Vcvv 2614  wss 2986  cop 3428   class class class wbr 3814  cmpt 3868   × cxp 4402  ccnv 4403  dom cdm 4404  cima 4407  Fun wfun 4966   Fn wfn 4967  wf 4968  1-1wf1 4969  1-1-ontowf1o 4971  cfv 4972  (class class class)co 5594  cen 6388  Fincfn 6390  0cc0 7271  1c1 7272   · cmul 7276  cle 7444  cn 8334  cz 8660  cq 9013  ..^cfzo 9457   mod cmo 9632  chash 10032  cdvds 10590   gcd cgcd 10732  ϕcphi 10980
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3922  ax-sep 3925  ax-nul 3933  ax-pow 3977  ax-pr 4003  ax-un 4227  ax-setind 4319  ax-iinf 4369  ax-cnex 7357  ax-resscn 7358  ax-1cn 7359  ax-1re 7360  ax-icn 7361  ax-addcl 7362  ax-addrcl 7363  ax-mulcl 7364  ax-mulrcl 7365  ax-addcom 7366  ax-mulcom 7367  ax-addass 7368  ax-mulass 7369  ax-distr 7370  ax-i2m1 7371  ax-0lt1 7372  ax-1rid 7373  ax-0id 7374  ax-rnegex 7375  ax-precex 7376  ax-cnre 7377  ax-pre-ltirr 7378  ax-pre-ltwlin 7379  ax-pre-lttrn 7380  ax-pre-apti 7381  ax-pre-ltadd 7382  ax-pre-mulgt0 7383  ax-pre-mulext 7384  ax-arch 7385  ax-caucvg 7386
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-nel 2347  df-ral 2360  df-rex 2361  df-reu 2362  df-rmo 2363  df-rab 2364  df-v 2616  df-sbc 2829  df-csb 2922  df-dif 2988  df-un 2990  df-in 2992  df-ss 2999  df-nul 3273  df-if 3377  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-int 3666  df-iun 3709  df-br 3815  df-opab 3869  df-mpt 3870  df-tr 3905  df-id 4087  df-po 4090  df-iso 4091  df-iord 4160  df-on 4162  df-ilim 4163  df-suc 4165  df-iom 4372  df-xp 4410  df-rel 4411  df-cnv 4412  df-co 4413  df-dm 4414  df-rn 4415  df-res 4416  df-ima 4417  df-iota 4937  df-fun 4974  df-fn 4975  df-f 4976  df-f1 4977  df-fo 4978  df-f1o 4979  df-fv 4980  df-riota 5550  df-ov 5597  df-oprab 5598  df-mpt2 5599  df-1st 5849  df-2nd 5850  df-recs 6005  df-irdg 6070  df-frec 6091  df-1o 6116  df-oadd 6120  df-er 6225  df-en 6391  df-dom 6392  df-fin 6393  df-sup 6600  df-pnf 7445  df-mnf 7446  df-xr 7447  df-ltxr 7448  df-le 7449  df-sub 7576  df-neg 7577  df-reap 7970  df-ap 7977  df-div 8056  df-inn 8335  df-2 8393  df-3 8394  df-4 8395  df-n0 8584  df-z 8661  df-uz 8929  df-q 9014  df-rp 9044  df-fz 9334  df-fzo 9458  df-fl 9580  df-mod 9633  df-iseq 9755  df-iexp 9806  df-ihash 10033  df-cj 10117  df-re 10118  df-im 10119  df-rsqrt 10272  df-abs 10273  df-dvds 10591  df-gcd 10733  df-phi 10981
This theorem is referenced by:  phimul  10996
  Copyright terms: Public domain W3C validator