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

Theorem phimullem 11828
Description: Lemma for phimul 11829. (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 5749 . . . . . . . . . . . . . 14 (𝑦 = 𝑤 → (𝑦 gcd (𝑀 · 𝑁)) = (𝑤 gcd (𝑀 · 𝑁)))
21eqeq1d 2126 . . . . . . . . . . . . 13 (𝑦 = 𝑤 → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ (𝑤 gcd (𝑀 · 𝑁)) = 1))
3 phimul.6 . . . . . . . . . . . . 13 𝑊 = {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
42, 3elrab2 2816 . . . . . . . . . . . 12 (𝑤𝑊 ↔ (𝑤𝑆 ∧ (𝑤 gcd (𝑀 · 𝑁)) = 1))
54simplbi 272 . . . . . . . . . . 11 (𝑤𝑊𝑤𝑆)
65adantl 275 . . . . . . . . . 10 ((𝜑𝑤𝑊) → 𝑤𝑆)
7 elfzoelz 9892 . . . . . . . . . . . . . . 15 (𝑤 ∈ (0..^(𝑀 · 𝑁)) → 𝑤 ∈ ℤ)
8 crth.1 . . . . . . . . . . . . . . 15 𝑆 = (0..^(𝑀 · 𝑁))
97, 8eleq2s 2212 . . . . . . . . . . . . . 14 (𝑤𝑆𝑤 ∈ ℤ)
106, 9syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑤 ∈ ℤ)
11 zq 9386 . . . . . . . . . . . . 13 (𝑤 ∈ ℤ → 𝑤 ∈ ℚ)
1210, 11syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑤 ∈ ℚ)
13 crth.4 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))
1413simp1d 978 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℕ)
1514adantr 274 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑀 ∈ ℕ)
16 nnq 9393 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
1715, 16syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑀 ∈ ℚ)
1815nngt0d 8732 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 0 < 𝑀)
1912, 17, 18modqcld 10069 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ ℚ)
2013simp2d 979 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ)
2120adantr 274 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑁 ∈ ℕ)
22 nnq 9393 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
2321, 22syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑁 ∈ ℚ)
2421nngt0d 8732 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 0 < 𝑁)
2512, 23, 24modqcld 10069 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ ℚ)
26 opexg 4120 . . . . . . . . . . 11 (((𝑤 mod 𝑀) ∈ ℚ ∧ (𝑤 mod 𝑁) ∈ ℚ) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V)
2719, 25, 26syl2anc 408 . . . . . . . . . 10 ((𝜑𝑤𝑊) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V)
28 oveq1 5749 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑥 mod 𝑀) = (𝑤 mod 𝑀))
29 oveq1 5749 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝑥 mod 𝑁) = (𝑤 mod 𝑁))
3028, 29opeq12d 3683 . . . . . . . . . . 11 (𝑥 = 𝑤 → ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩ = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
31 crth.3 . . . . . . . . . . 11 𝐹 = (𝑥𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)
3230, 31fvmptg 5465 . . . . . . . . . 10 ((𝑤𝑆 ∧ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ V) → (𝐹𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
336, 27, 32syl2anc 408 . . . . . . . . 9 ((𝜑𝑤𝑊) → (𝐹𝑤) = ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
345, 8eleqtrdi 2210 . . . . . . . . . . . . . 14 (𝑤𝑊𝑤 ∈ (0..^(𝑀 · 𝑁)))
3534adantl 275 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → 𝑤 ∈ (0..^(𝑀 · 𝑁)))
3635, 7syl 14 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → 𝑤 ∈ ℤ)
37 zmodfzo 10088 . . . . . . . . . . . 12 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
3836, 15, 37syl2anc 408 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ (0..^𝑀))
39 modgcd 11606 . . . . . . . . . . . . 13 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℕ) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
4036, 15, 39syl2anc 408 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = (𝑤 gcd 𝑀))
4115nnzd 9140 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → 𝑀 ∈ ℤ)
42 gcddvds 11579 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
4336, 41, 42syl2anc 408 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ 𝑀))
4443simpld 111 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ 𝑤)
45 nnne0 8716 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℕ → 𝑀 ≠ 0)
46 simpr 109 . . . . . . . . . . . . . . . . . . . 20 ((𝑤 = 0 ∧ 𝑀 = 0) → 𝑀 = 0)
4746necon3ai 2334 . . . . . . . . . . . . . . . . . . 19 (𝑀 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
4815, 45, 473syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ 𝑀 = 0))
49 gcdn0cl 11578 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑀 = 0)) → (𝑤 gcd 𝑀) ∈ ℕ)
5036, 41, 48, 49syl21anc 1200 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∈ ℕ)
5150nnzd 9140 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∈ ℤ)
5221nnzd 9140 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → 𝑁 ∈ ℤ)
5343simprd 113 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ 𝑀)
5451, 41, 52, 53dvdsmultr1d 11459 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁))
5515, 21nnmulcld 8737 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑀 · 𝑁) ∈ ℕ)
5655nnzd 9140 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑀 · 𝑁) ∈ ℤ)
57 nnne0 8716 . . . . . . . . . . . . . . . . 17 ((𝑀 · 𝑁) ∈ ℕ → (𝑀 · 𝑁) ≠ 0)
58 simpr 109 . . . . . . . . . . . . . . . . . 18 ((𝑤 = 0 ∧ (𝑀 · 𝑁) = 0) → (𝑀 · 𝑁) = 0)
5958necon3ai 2334 . . . . . . . . . . . . . . . . 17 ((𝑀 · 𝑁) ≠ 0 → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
6055, 57, 593syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0))
61 dvdslegcd 11580 . . . . . . . . . . . . . . . 16 ((((𝑤 gcd 𝑀) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))))
6251, 36, 56, 60, 61syl31anc 1204 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑀) ∥ 𝑤 ∧ (𝑤 gcd 𝑀) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁))))
6344, 54, 62mp2and 429 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ≤ (𝑤 gcd (𝑀 · 𝑁)))
644simprbi 273 . . . . . . . . . . . . . . 15 (𝑤𝑊 → (𝑤 gcd (𝑀 · 𝑁)) = 1)
6564adantl 275 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd (𝑀 · 𝑁)) = 1)
6663, 65breqtrd 3924 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) ≤ 1)
67 nnle1eq1 8712 . . . . . . . . . . . . . 14 ((𝑤 gcd 𝑀) ∈ ℕ → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
6850, 67syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑀) ≤ 1 ↔ (𝑤 gcd 𝑀) = 1))
6966, 68mpbid 146 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑀) = 1)
7040, 69eqtrd 2150 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑀) gcd 𝑀) = 1)
71 oveq1 5749 . . . . . . . . . . . . 13 (𝑦 = (𝑤 mod 𝑀) → (𝑦 gcd 𝑀) = ((𝑤 mod 𝑀) gcd 𝑀))
7271eqeq1d 2126 . . . . . . . . . . . 12 (𝑦 = (𝑤 mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
73 phimul.4 . . . . . . . . . . . 12 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}
7472, 73elrab2 2816 . . . . . . . . . . 11 ((𝑤 mod 𝑀) ∈ 𝑈 ↔ ((𝑤 mod 𝑀) ∈ (0..^𝑀) ∧ ((𝑤 mod 𝑀) gcd 𝑀) = 1))
7538, 70, 74sylanbrc 413 . . . . . . . . . 10 ((𝜑𝑤𝑊) → (𝑤 mod 𝑀) ∈ 𝑈)
76 zmodfzo 10088 . . . . . . . . . . . 12 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
7736, 21, 76syl2anc 408 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ (0..^𝑁))
78 modgcd 11606 . . . . . . . . . . . . 13 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
7936, 21, 78syl2anc 408 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = (𝑤 gcd 𝑁))
80 gcddvds 11579 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
8136, 52, 80syl2anc 408 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ 𝑁))
8281simpld 111 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ 𝑤)
8381simprd 113 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ 𝑁)
84 dvdsmul2 11443 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁))
8541, 52, 84syl2anc 408 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → 𝑁 ∥ (𝑀 · 𝑁))
86 nnne0 8716 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
87 simpr 109 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
8887necon3ai 2334 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ≠ 0 → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
8921, 86, 883syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤𝑊) → ¬ (𝑤 = 0 ∧ 𝑁 = 0))
90 gcdn0cl 11578 . . . . . . . . . . . . . . . . . . 19 (((𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ 𝑁 = 0)) → (𝑤 gcd 𝑁) ∈ ℕ)
9136, 52, 89, 90syl21anc 1200 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∈ ℕ)
9291nnzd 9140 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∈ ℤ)
93 dvdstr 11457 . . . . . . . . . . . . . . . . 17 (((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (((𝑤 gcd 𝑁) ∥ 𝑁𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)))
9492, 52, 56, 93syl3anc 1201 . . . . . . . . . . . . . . . 16 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑁𝑁 ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)))
9583, 85, 94mp2and 429 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁))
96 dvdslegcd 11580 . . . . . . . . . . . . . . . 16 ((((𝑤 gcd 𝑁) ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) ∧ ¬ (𝑤 = 0 ∧ (𝑀 · 𝑁) = 0)) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))))
9792, 36, 56, 60, 96syl31anc 1204 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑊) → (((𝑤 gcd 𝑁) ∥ 𝑤 ∧ (𝑤 gcd 𝑁) ∥ (𝑀 · 𝑁)) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁))))
9882, 95, 97mp2and 429 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ≤ (𝑤 gcd (𝑀 · 𝑁)))
9998, 65breqtrd 3924 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) ≤ 1)
100 nnle1eq1 8712 . . . . . . . . . . . . . 14 ((𝑤 gcd 𝑁) ∈ ℕ → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
10191, 100syl 14 . . . . . . . . . . . . 13 ((𝜑𝑤𝑊) → ((𝑤 gcd 𝑁) ≤ 1 ↔ (𝑤 gcd 𝑁) = 1))
10299, 101mpbid 146 . . . . . . . . . . . 12 ((𝜑𝑤𝑊) → (𝑤 gcd 𝑁) = 1)
10379, 102eqtrd 2150 . . . . . . . . . . 11 ((𝜑𝑤𝑊) → ((𝑤 mod 𝑁) gcd 𝑁) = 1)
104 oveq1 5749 . . . . . . . . . . . . 13 (𝑦 = (𝑤 mod 𝑁) → (𝑦 gcd 𝑁) = ((𝑤 mod 𝑁) gcd 𝑁))
105104eqeq1d 2126 . . . . . . . . . . . 12 (𝑦 = (𝑤 mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
106 phimul.5 . . . . . . . . . . . 12 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}
107105, 106elrab2 2816 . . . . . . . . . . 11 ((𝑤 mod 𝑁) ∈ 𝑉 ↔ ((𝑤 mod 𝑁) ∈ (0..^𝑁) ∧ ((𝑤 mod 𝑁) gcd 𝑁) = 1))
10877, 103, 107sylanbrc 413 . . . . . . . . . 10 ((𝜑𝑤𝑊) → (𝑤 mod 𝑁) ∈ 𝑉)
109 opelxpi 4541 . . . . . . . . . 10 (((𝑤 mod 𝑀) ∈ 𝑈 ∧ (𝑤 mod 𝑁) ∈ 𝑉) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
11075, 108, 109syl2anc 408 . . . . . . . . 9 ((𝜑𝑤𝑊) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
11133, 110eqeltrd 2194 . . . . . . . 8 ((𝜑𝑤𝑊) → (𝐹𝑤) ∈ (𝑈 × 𝑉))
112111ralrimiva 2482 . . . . . . 7 (𝜑 → ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉))
113 crth.2 . . . . . . . . . 10 𝑇 = ((0..^𝑀) × (0..^𝑁))
1148, 113, 31, 13crth 11827 . . . . . . . . 9 (𝜑𝐹:𝑆1-1-onto𝑇)
115 f1ofn 5336 . . . . . . . . 9 (𝐹:𝑆1-1-onto𝑇𝐹 Fn 𝑆)
116 fnfun 5190 . . . . . . . . 9 (𝐹 Fn 𝑆 → Fun 𝐹)
117114, 115, 1163syl 17 . . . . . . . 8 (𝜑 → Fun 𝐹)
118 ssrab2 3152 . . . . . . . . . 10 {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} ⊆ 𝑆
1193, 118eqsstri 3099 . . . . . . . . 9 𝑊𝑆
120 fndm 5192 . . . . . . . . . 10 (𝐹 Fn 𝑆 → dom 𝐹 = 𝑆)
121114, 115, 1203syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝑆)
122119, 121sseqtrrid 3118 . . . . . . . 8 (𝜑𝑊 ⊆ dom 𝐹)
123 funimass4 5440 . . . . . . . 8 ((Fun 𝐹𝑊 ⊆ dom 𝐹) → ((𝐹𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉)))
124117, 122, 123syl2anc 408 . . . . . . 7 (𝜑 → ((𝐹𝑊) ⊆ (𝑈 × 𝑉) ↔ ∀𝑤𝑊 (𝐹𝑤) ∈ (𝑈 × 𝑉)))
125112, 124mpbird 166 . . . . . 6 (𝜑 → (𝐹𝑊) ⊆ (𝑈 × 𝑉))
126 ssrab2 3152 . . . . . . . . . . . . . 14 {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ⊆ (0..^𝑀)
12773, 126eqsstri 3099 . . . . . . . . . . . . 13 𝑈 ⊆ (0..^𝑀)
128 ssrab2 3152 . . . . . . . . . . . . . 14 {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁)
129106, 128eqsstri 3099 . . . . . . . . . . . . 13 𝑉 ⊆ (0..^𝑁)
130 xpss12 4616 . . . . . . . . . . . . 13 ((𝑈 ⊆ (0..^𝑀) ∧ 𝑉 ⊆ (0..^𝑁)) → (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁)))
131127, 129, 130mp2an 422 . . . . . . . . . . . 12 (𝑈 × 𝑉) ⊆ ((0..^𝑀) × (0..^𝑁))
132131, 113sseqtrri 3102 . . . . . . . . . . 11 (𝑈 × 𝑉) ⊆ 𝑇
133132sseli 3063 . . . . . . . . . 10 (𝑧 ∈ (𝑈 × 𝑉) → 𝑧𝑇)
134 f1ocnvfv2 5647 . . . . . . . . . 10 ((𝐹:𝑆1-1-onto𝑇𝑧𝑇) → (𝐹‘(𝐹𝑧)) = 𝑧)
135114, 133, 134syl2an 287 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) = 𝑧)
136 f1ocnv 5348 . . . . . . . . . . . . 13 (𝐹:𝑆1-1-onto𝑇𝐹:𝑇1-1-onto𝑆)
137 f1of 5335 . . . . . . . . . . . . 13 (𝐹:𝑇1-1-onto𝑆𝐹:𝑇𝑆)
138114, 136, 1373syl 17 . . . . . . . . . . . 12 (𝜑𝐹:𝑇𝑆)
139 ffvelrn 5521 . . . . . . . . . . . 12 ((𝐹:𝑇𝑆𝑧𝑇) → (𝐹𝑧) ∈ 𝑆)
140138, 133, 139syl2an 287 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ 𝑆)
141140, 8eleqtrdi 2210 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ (0..^(𝑀 · 𝑁)))
142 elfzoelz 9892 . . . . . . . . . . . . . . 15 ((𝐹𝑧) ∈ (0..^(𝑀 · 𝑁)) → (𝐹𝑧) ∈ ℤ)
143141, 142syl 14 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ ℤ)
14414adantr 274 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℕ)
145 modgcd 11606 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ ℤ ∧ 𝑀 ∈ ℕ) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = ((𝐹𝑧) gcd 𝑀))
146143, 144, 145syl2anc 408 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = ((𝐹𝑧) gcd 𝑀))
147 zq 9386 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑧) ∈ ℤ → (𝐹𝑧) ∈ ℚ)
148143, 147syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ ℚ)
149144, 16syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℚ)
150144nngt0d 8732 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 0 < 𝑀)
151148, 149, 150modqcld 10069 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑀) ∈ ℚ)
15220adantr 274 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℕ)
153152, 22syl 14 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℚ)
154152nngt0d 8732 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 0 < 𝑁)
155148, 153, 154modqcld 10069 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑁) ∈ ℚ)
156 opexg 4120 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑧) mod 𝑀) ∈ ℚ ∧ ((𝐹𝑧) mod 𝑁) ∈ ℚ) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V)
157151, 155, 156syl2anc 408 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V)
158 oveq1 5749 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝐹𝑧) → (𝑤 mod 𝑀) = ((𝐹𝑧) mod 𝑀))
159 oveq1 5749 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝐹𝑧) → (𝑤 mod 𝑁) = ((𝐹𝑧) mod 𝑁))
160158, 159opeq12d 3683 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = (𝐹𝑧) → ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩ = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
16130cbvmptv 3994 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩) = (𝑤𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
16231, 161eqtri 2138 . . . . . . . . . . . . . . . . . . . . 21 𝐹 = (𝑤𝑆 ↦ ⟨(𝑤 mod 𝑀), (𝑤 mod 𝑁)⟩)
163160, 162fvmptg 5465 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑧) ∈ 𝑆 ∧ ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ V) → (𝐹‘(𝐹𝑧)) = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
164140, 157, 163syl2anc 408 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
165135, 164eqtr3d 2152 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 = ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩)
166 simpr 109 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝑈 × 𝑉))
167165, 166eqeltrrd 2195 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉))
168 opelxp 4539 . . . . . . . . . . . . . . . . 17 (⟨((𝐹𝑧) mod 𝑀), ((𝐹𝑧) mod 𝑁)⟩ ∈ (𝑈 × 𝑉) ↔ (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ∧ ((𝐹𝑧) mod 𝑁) ∈ 𝑉))
169167, 168sylib 121 . . . . . . . . . . . . . . . 16 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ∧ ((𝐹𝑧) mod 𝑁) ∈ 𝑉))
170169simpld 111 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑀) ∈ 𝑈)
171 oveq1 5749 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝐹𝑧) mod 𝑀) → (𝑦 gcd 𝑀) = (((𝐹𝑧) mod 𝑀) gcd 𝑀))
172171eqeq1d 2126 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝐹𝑧) mod 𝑀) → ((𝑦 gcd 𝑀) = 1 ↔ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
173172, 73elrab2 2816 . . . . . . . . . . . . . . 15 (((𝐹𝑧) mod 𝑀) ∈ 𝑈 ↔ (((𝐹𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
174170, 173sylib 121 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) ∈ (0..^𝑀) ∧ (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1))
175174simprd 113 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑀) gcd 𝑀) = 1)
176146, 175eqtr3d 2152 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd 𝑀) = 1)
177 modgcd 11606 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = ((𝐹𝑧) gcd 𝑁))
178143, 152, 177syl2anc 408 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = ((𝐹𝑧) gcd 𝑁))
179169simprd 113 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) mod 𝑁) ∈ 𝑉)
180 oveq1 5749 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝐹𝑧) mod 𝑁) → (𝑦 gcd 𝑁) = (((𝐹𝑧) mod 𝑁) gcd 𝑁))
181180eqeq1d 2126 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝐹𝑧) mod 𝑁) → ((𝑦 gcd 𝑁) = 1 ↔ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
182181, 106elrab2 2816 . . . . . . . . . . . . . . 15 (((𝐹𝑧) mod 𝑁) ∈ 𝑉 ↔ (((𝐹𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
183179, 182sylib 121 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) ∈ (0..^𝑁) ∧ (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1))
184183simprd 113 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (((𝐹𝑧) mod 𝑁) gcd 𝑁) = 1)
185178, 184eqtr3d 2152 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd 𝑁) = 1)
18614nnzd 9140 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℤ)
187186adantr 274 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑀 ∈ ℤ)
18820nnzd 9140 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
189188adantr 274 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑁 ∈ ℤ)
190 rpmul 11706 . . . . . . . . . . . . 13 (((𝐹𝑧) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((((𝐹𝑧) gcd 𝑀) = 1 ∧ ((𝐹𝑧) gcd 𝑁) = 1) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
191143, 187, 189, 190syl3anc 1201 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((((𝐹𝑧) gcd 𝑀) = 1 ∧ ((𝐹𝑧) gcd 𝑁) = 1) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
192176, 185, 191mp2and 429 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1)
193 oveq1 5749 . . . . . . . . . . . . 13 (𝑦 = (𝐹𝑧) → (𝑦 gcd (𝑀 · 𝑁)) = ((𝐹𝑧) gcd (𝑀 · 𝑁)))
194193eqeq1d 2126 . . . . . . . . . . . 12 (𝑦 = (𝐹𝑧) → ((𝑦 gcd (𝑀 · 𝑁)) = 1 ↔ ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
195194, 3elrab2 2816 . . . . . . . . . . 11 ((𝐹𝑧) ∈ 𝑊 ↔ ((𝐹𝑧) ∈ 𝑆 ∧ ((𝐹𝑧) gcd (𝑀 · 𝑁)) = 1))
196140, 192, 195sylanbrc 413 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹𝑧) ∈ 𝑊)
197 funfvima2 5618 . . . . . . . . . . . 12 ((Fun 𝐹𝑊 ⊆ dom 𝐹) → ((𝐹𝑧) ∈ 𝑊 → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊)))
198117, 122, 197syl2anc 408 . . . . . . . . . . 11 (𝜑 → ((𝐹𝑧) ∈ 𝑊 → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊)))
199198imp 123 . . . . . . . . . 10 ((𝜑 ∧ (𝐹𝑧) ∈ 𝑊) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊))
200196, 199syldan 280 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑊))
201135, 200eqeltrrd 2195 . . . . . . . 8 ((𝜑𝑧 ∈ (𝑈 × 𝑉)) → 𝑧 ∈ (𝐹𝑊))
202201ex 114 . . . . . . 7 (𝜑 → (𝑧 ∈ (𝑈 × 𝑉) → 𝑧 ∈ (𝐹𝑊)))
203202ssrdv 3073 . . . . . 6 (𝜑 → (𝑈 × 𝑉) ⊆ (𝐹𝑊))
204125, 203eqssd 3084 . . . . 5 (𝜑 → (𝐹𝑊) = (𝑈 × 𝑉))
205 f1of1 5334 . . . . . . 7 (𝐹:𝑆1-1-onto𝑇𝐹:𝑆1-1𝑇)
206114, 205syl 14 . . . . . 6 (𝜑𝐹:𝑆1-1𝑇)
207119a1i 9 . . . . . 6 (𝜑𝑊𝑆)
208 0z 9033 . . . . . . . . . 10 0 ∈ ℤ
209186, 188zmulcld 9147 . . . . . . . . . 10 (𝜑 → (𝑀 · 𝑁) ∈ ℤ)
210 fzofig 10173 . . . . . . . . . 10 ((0 ∈ ℤ ∧ (𝑀 · 𝑁) ∈ ℤ) → (0..^(𝑀 · 𝑁)) ∈ Fin)
211208, 209, 210sylancr 410 . . . . . . . . 9 (𝜑 → (0..^(𝑀 · 𝑁)) ∈ Fin)
2128, 211eqeltrid 2204 . . . . . . . 8 (𝜑𝑆 ∈ Fin)
213 elfzoelz 9892 . . . . . . . . . . . . . 14 (𝑦 ∈ (0..^(𝑀 · 𝑁)) → 𝑦 ∈ ℤ)
214213, 8eleq2s 2212 . . . . . . . . . . . . 13 (𝑦𝑆𝑦 ∈ ℤ)
215214adantl 275 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 𝑦 ∈ ℤ)
216209adantr 274 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (𝑀 · 𝑁) ∈ ℤ)
217215, 216gcdcld 11584 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → (𝑦 gcd (𝑀 · 𝑁)) ∈ ℕ0)
218217nn0zd 9139 . . . . . . . . . 10 ((𝜑𝑦𝑆) → (𝑦 gcd (𝑀 · 𝑁)) ∈ ℤ)
219 1zzd 9049 . . . . . . . . . 10 ((𝜑𝑦𝑆) → 1 ∈ ℤ)
220 zdceq 9094 . . . . . . . . . 10 (((𝑦 gcd (𝑀 · 𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
221218, 219, 220syl2anc 408 . . . . . . . . 9 ((𝜑𝑦𝑆) → DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
222221ralrimiva 2482 . . . . . . . 8 (𝜑 → ∀𝑦𝑆 DECID (𝑦 gcd (𝑀 · 𝑁)) = 1)
223212, 222ssfirab 6790 . . . . . . 7 (𝜑 → {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} ∈ Fin)
2243, 223eqeltrid 2204 . . . . . 6 (𝜑𝑊 ∈ Fin)
225 f1imaeng 6654 . . . . . 6 ((𝐹:𝑆1-1𝑇𝑊𝑆𝑊 ∈ Fin) → (𝐹𝑊) ≈ 𝑊)
226206, 207, 224, 225syl3anc 1201 . . . . 5 (𝜑 → (𝐹𝑊) ≈ 𝑊)
227204, 226eqbrtrrd 3922 . . . 4 (𝜑 → (𝑈 × 𝑉) ≈ 𝑊)
228 fzofig 10173 . . . . . . . . 9 ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (0..^𝑀) ∈ Fin)
229208, 186, 228sylancr 410 . . . . . . . 8 (𝜑 → (0..^𝑀) ∈ Fin)
230 elfzoelz 9892 . . . . . . . . . . . . 13 (𝑦 ∈ (0..^𝑀) → 𝑦 ∈ ℤ)
231230adantl 275 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑀)) → 𝑦 ∈ ℤ)
232186adantr 274 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑀)) → 𝑀 ∈ ℤ)
233231, 232gcdcld 11584 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0..^𝑀)) → (𝑦 gcd 𝑀) ∈ ℕ0)
234233nn0zd 9139 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑀)) → (𝑦 gcd 𝑀) ∈ ℤ)
235 1z 9048 . . . . . . . . . 10 1 ∈ ℤ
236 zdceq 9094 . . . . . . . . . 10 (((𝑦 gcd 𝑀) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd 𝑀) = 1)
237234, 235, 236sylancl 409 . . . . . . . . 9 ((𝜑𝑦 ∈ (0..^𝑀)) → DECID (𝑦 gcd 𝑀) = 1)
238237ralrimiva 2482 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (0..^𝑀)DECID (𝑦 gcd 𝑀) = 1)
239229, 238ssfirab 6790 . . . . . . 7 (𝜑 → {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} ∈ Fin)
24073, 239eqeltrid 2204 . . . . . 6 (𝜑𝑈 ∈ Fin)
241 fzofig 10173 . . . . . . . . 9 ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0..^𝑁) ∈ Fin)
242208, 188, 241sylancr 410 . . . . . . . 8 (𝜑 → (0..^𝑁) ∈ Fin)
243 elfzoelz 9892 . . . . . . . . . . . . 13 (𝑦 ∈ (0..^𝑁) → 𝑦 ∈ ℤ)
244243adantl 275 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑁)) → 𝑦 ∈ ℤ)
245188adantr 274 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (0..^𝑁)) → 𝑁 ∈ ℤ)
246244, 245gcdcld 11584 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (0..^𝑁)) → (𝑦 gcd 𝑁) ∈ ℕ0)
247246nn0zd 9139 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑁)) → (𝑦 gcd 𝑁) ∈ ℤ)
248 1zzd 9049 . . . . . . . . . 10 ((𝜑𝑦 ∈ (0..^𝑁)) → 1 ∈ ℤ)
249 zdceq 9094 . . . . . . . . . 10 (((𝑦 gcd 𝑁) ∈ ℤ ∧ 1 ∈ ℤ) → DECID (𝑦 gcd 𝑁) = 1)
250247, 248, 249syl2anc 408 . . . . . . . . 9 ((𝜑𝑦 ∈ (0..^𝑁)) → DECID (𝑦 gcd 𝑁) = 1)
251250ralrimiva 2482 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (0..^𝑁)DECID (𝑦 gcd 𝑁) = 1)
252242, 251ssfirab 6790 . . . . . . 7 (𝜑 → {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ∈ Fin)
253106, 252eqeltrid 2204 . . . . . 6 (𝜑𝑉 ∈ Fin)
254 xpfi 6786 . . . . . 6 ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (𝑈 × 𝑉) ∈ Fin)
255240, 253, 254syl2anc 408 . . . . 5 (𝜑 → (𝑈 × 𝑉) ∈ Fin)
256 hashen 10498 . . . . 5 (((𝑈 × 𝑉) ∈ Fin ∧ 𝑊 ∈ Fin) → ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊))
257255, 224, 256syl2anc 408 . . . 4 (𝜑 → ((♯‘(𝑈 × 𝑉)) = (♯‘𝑊) ↔ (𝑈 × 𝑉) ≈ 𝑊))
258227, 257mpbird 166 . . 3 (𝜑 → (♯‘(𝑈 × 𝑉)) = (♯‘𝑊))
259 hashxp 10540 . . . 4 ((𝑈 ∈ Fin ∧ 𝑉 ∈ Fin) → (♯‘(𝑈 × 𝑉)) = ((♯‘𝑈) · (♯‘𝑉)))
260240, 253, 259syl2anc 408 . . 3 (𝜑 → (♯‘(𝑈 × 𝑉)) = ((♯‘𝑈) · (♯‘𝑉)))
261258, 260eqtr3d 2152 . 2 (𝜑 → (♯‘𝑊) = ((♯‘𝑈) · (♯‘𝑉)))
26214, 20nnmulcld 8737 . . 3 (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
263 dfphi2 11823 . . . 4 ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}))
2648rabeqi 2653 . . . . . 6 {𝑦𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
2653, 264eqtri 2138 . . . . 5 𝑊 = {𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}
266265fveq2i 5392 . . . 4 (♯‘𝑊) = (♯‘{𝑦 ∈ (0..^(𝑀 · 𝑁)) ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1})
267263, 266syl6eqr 2168 . . 3 ((𝑀 · 𝑁) ∈ ℕ → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊))
268262, 267syl 14 . 2 (𝜑 → (ϕ‘(𝑀 · 𝑁)) = (♯‘𝑊))
269 dfphi2 11823 . . . . 5 (𝑀 ∈ ℕ → (ϕ‘𝑀) = (♯‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}))
27073fveq2i 5392 . . . . 5 (♯‘𝑈) = (♯‘{𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1})
271269, 270syl6eqr 2168 . . . 4 (𝑀 ∈ ℕ → (ϕ‘𝑀) = (♯‘𝑈))
27214, 271syl 14 . . 3 (𝜑 → (ϕ‘𝑀) = (♯‘𝑈))
273 dfphi2 11823 . . . . 5 (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}))
274106fveq2i 5392 . . . . 5 (♯‘𝑉) = (♯‘{𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1})
275273, 274syl6eqr 2168 . . . 4 (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘𝑉))
27620, 275syl 14 . . 3 (𝜑 → (ϕ‘𝑁) = (♯‘𝑉))
277272, 276oveq12d 5760 . 2 (𝜑 → ((ϕ‘𝑀) · (ϕ‘𝑁)) = ((♯‘𝑈) · (♯‘𝑉)))
278261, 268, 2773eqtr4d 2160 1 (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  DECID wdc 804  w3a 947   = wceq 1316  wcel 1465  wne 2285  wral 2393  {crab 2397  Vcvv 2660  wss 3041  cop 3500   class class class wbr 3899  cmpt 3959   × cxp 4507  ccnv 4508  dom cdm 4509  cima 4512  Fun wfun 5087   Fn wfn 5088  wf 5089  1-1wf1 5090  1-1-ontowf1o 5092  cfv 5093  (class class class)co 5742  cen 6600  Fincfn 6602  0cc0 7588  1c1 7589   · cmul 7593  cle 7769  cn 8688  cz 9022  cq 9379  ..^cfzo 9887   mod cmo 10063  chash 10489  cdvds 11420   gcd cgcd 11562  ϕcphi 11813
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-coll 4013  ax-sep 4016  ax-nul 4024  ax-pow 4068  ax-pr 4101  ax-un 4325  ax-setind 4422  ax-iinf 4472  ax-cnex 7679  ax-resscn 7680  ax-1cn 7681  ax-1re 7682  ax-icn 7683  ax-addcl 7684  ax-addrcl 7685  ax-mulcl 7686  ax-mulrcl 7687  ax-addcom 7688  ax-mulcom 7689  ax-addass 7690  ax-mulass 7691  ax-distr 7692  ax-i2m1 7693  ax-0lt1 7694  ax-1rid 7695  ax-0id 7696  ax-rnegex 7697  ax-precex 7698  ax-cnre 7699  ax-pre-ltirr 7700  ax-pre-ltwlin 7701  ax-pre-lttrn 7702  ax-pre-apti 7703  ax-pre-ltadd 7704  ax-pre-mulgt0 7705  ax-pre-mulext 7706  ax-arch 7707  ax-caucvg 7708
This theorem depends on definitions:  df-bi 116  df-stab 801  df-dc 805  df-3or 948  df-3an 949  df-tru 1319  df-fal 1322  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-nel 2381  df-ral 2398  df-rex 2399  df-reu 2400  df-rmo 2401  df-rab 2402  df-v 2662  df-sbc 2883  df-csb 2976  df-dif 3043  df-un 3045  df-in 3047  df-ss 3054  df-nul 3334  df-if 3445  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-int 3742  df-iun 3785  df-br 3900  df-opab 3960  df-mpt 3961  df-tr 3997  df-id 4185  df-po 4188  df-iso 4189  df-iord 4258  df-on 4260  df-ilim 4261  df-suc 4263  df-iom 4475  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-rn 4520  df-res 4521  df-ima 4522  df-iota 5058  df-fun 5095  df-fn 5096  df-f 5097  df-f1 5098  df-fo 5099  df-f1o 5100  df-fv 5101  df-riota 5698  df-ov 5745  df-oprab 5746  df-mpo 5747  df-1st 6006  df-2nd 6007  df-recs 6170  df-irdg 6235  df-frec 6256  df-1o 6281  df-oadd 6285  df-er 6397  df-en 6603  df-dom 6604  df-fin 6605  df-sup 6839  df-pnf 7770  df-mnf 7771  df-xr 7772  df-ltxr 7773  df-le 7774  df-sub 7903  df-neg 7904  df-reap 8305  df-ap 8312  df-div 8401  df-inn 8689  df-2 8747  df-3 8748  df-4 8749  df-n0 8946  df-z 9023  df-uz 9295  df-q 9380  df-rp 9410  df-fz 9759  df-fzo 9888  df-fl 10011  df-mod 10064  df-seqfrec 10187  df-exp 10261  df-ihash 10490  df-cj 10582  df-re 10583  df-im 10584  df-rsqrt 10738  df-abs 10739  df-dvds 11421  df-gcd 11563  df-phi 11814
This theorem is referenced by:  phimul  11829
  Copyright terms: Public domain W3C validator